cprover
Loading...
Searching...
No Matches
cprover.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: C library check
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
9#ifndef CPROVER_ANSI_C_LIBRARY_CPROVER_H
10#define CPROVER_ANSI_C_LIBRARY_CPROVER_H
11
15
16// NOLINTNEXTLINE(readability/identifiers)
17typedef __typeof__(sizeof(int)) __CPROVER_size_t;
18// NOLINTNEXTLINE(readability/identifiers)
19typedef signed long long __CPROVER_ssize_t;
20
21#define __CPROVER_constant_infinity_uint 1
22
25extern const void *__CPROVER_deallocated;
26extern const void *__CPROVER_memory_leak;
27
31
32// malloc failure modes
35
42
43// __CPROVER_equal expects two arguments of the same type -- any type is
44// permitted, unsigned long long is just used for the benefit of running syntax
45// checks using system compilers
46__CPROVER_bool __CPROVER_equal(unsigned long long, unsigned long long);
47
48// The following built-ins are type checked by our C front-end and do not
49// require declarations. They work with any types as described below. unsigned
50// long long is just used to enable checks using system compilers.
51
52// detect overflow
53// the following expect two numeric arguments
54__CPROVER_bool __CPROVER_overflow_minus(unsigned long long, unsigned long long);
55__CPROVER_bool __CPROVER_overflow_mult(unsigned long long, unsigned long long);
56__CPROVER_bool __CPROVER_overflow_plus(unsigned long long, unsigned long long);
57__CPROVER_bool __CPROVER_overflow_shl(unsigned long long, unsigned long long);
58// expects one numeric argument
60
61// enumerations
62// expects one enum-typed argument
64
65// The following have an optional second parameter (the width), and are
66// polymorphic in the first parameter: if the second argument is omitted, then
67// the width of the subtype of the pointer-typed first argument is used.
68__CPROVER_bool __CPROVER_r_ok(const void *, ...);
69__CPROVER_bool __CPROVER_w_ok(const void *, ...);
71
72#include "../cprover_builtin_headers.h"
73
74#endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H
int __CPROVER_malloc_failure_mode
int __CPROVER_malloc_failure_mode_return_null
typedef __typeof__(sizeof(int)) __CPROVER_size_t
__CPROVER_bool __CPROVER_overflow_mult(unsigned long long, unsigned long long)
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_bool __CPROVER_w_ok(const void *,...)
void __CPROVER_deallocate(void *)
const void * __CPROVER_deallocated
__CPROVER_bool __CPROVER_enum_is_in_range(unsigned long long)
__CPROVER_size_t __CPROVER_max_malloc_size
__CPROVER_bool __CPROVER_overflow_shl(unsigned long long, unsigned long long)
__CPROVER_bool __CPROVER_equal(unsigned long long, unsigned long long)
const void * __CPROVER_memory_leak
__CPROVER_bool __CPROVER_malloc_may_fail
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_bool __CPROVER_rw_ok(const void *,...)
__CPROVER_bool __CPROVER_overflow_minus(unsigned long long, unsigned long long)
__CPROVER_bool __CPROVER_overflow_plus(unsigned long long, unsigned long long)
__CPROVER_bool __CPROVER_r_ok(const void *,...)
__CPROVER_bool __CPROVER_overflow_unary_minus(unsigned long long)
signed long long __CPROVER_ssize_t
Definition cprover.h:19
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
short next_unread
Definition cprover.h:40
short next_avail
Definition cprover.h:39
_Bool widowed
Definition cprover.h:37
Definition kdev_t.h:24