CBMC
cprover.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: C library check
4 
5 Author: 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)
17 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
18 // NOLINTNEXTLINE(readability/identifiers)
19 typedef signed long long __CPROVER_ssize_t;
20 
21 #define __CPROVER_constant_infinity_uint 1
22 
23 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
24 void __CPROVER_deallocate(void *);
25 extern const void *__CPROVER_deallocated;
26 extern const void *__CPROVER_memory_leak;
27 
29 extern __CPROVER_size_t __CPROVER_max_malloc_size;
30 extern __CPROVER_bool __CPROVER_malloc_may_fail;
31 
32 // malloc failure modes
35 
37  _Bool widowed;
38  char data[4];
39  short next_avail;
40  short next_unread;
41 };
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
59 __CPROVER_bool __CPROVER_overflow_unary_minus(unsigned long long);
60 
61 // enumerations
62 // expects one enum-typed argument
63 __CPROVER_bool __CPROVER_enum_is_in_range(unsigned long long);
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 *, ...);
70 __CPROVER_bool __CPROVER_rw_ok(const void *, ...);
71 
72 #include "../cprover_builtin_headers.h"
73 
74 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
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)
__CPROVER_bool __CPROVER_w_ok(const void *,...)
void __CPROVER_deallocate(void *)
Definition: stdlib.c:670
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
short next_unread
Definition: cprover.h:40
short next_avail
Definition: cprover.h:39
_Bool widowed
Definition: cprover.h:37
char data[4]
Definition: cprover.h:38