cprover
cprover.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module:
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
9 #ifndef CPROVER_CPP_LIBRARY_CPROVER_H
10 #define CPROVER_CPP_LIBRARY_CPROVER_H
11 
12 // NOLINTNEXTLINE(readability/identifiers)
13 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
14 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
15 extern const void *__CPROVER_deallocated;
16 extern const void *__CPROVER_new_object;
18 extern const void *__CPROVER_memory_leak;
19 
20 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
21 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
22 void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
23 void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
24 
25 void __CPROVER_input(const char *description, ...);
26 void __CPROVER_output(const char *description, ...);
27 
28 // concurrency-related
31 void __CPROVER_fence(const char *kind, ...);
32 
33 // pointers
34 unsigned __CPROVER_POINTER_OBJECT(const void *p);
35 signed __CPROVER_POINTER_OFFSET(const void *p);
36 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
37 
38 // arrays
39 // __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
40 void __CPROVER_array_copy(const void *dest, const void *src);
41 void __CPROVER_array_set(const void *dest, ...);
42 void __CPROVER_array_replace(const void *dest, const void *src);
43 
44 void __CPROVER_set_must(const void *, const char *);
45 void __CPROVER_set_may(const void *, const char *);
46 void __CPROVER_clear_must(const void *, const char *);
47 void __CPROVER_clear_may(const void *, const char *);
48 void __CPROVER_cleanup(const void *, void (*)(void *));
49 __CPROVER_bool __CPROVER_get_must(const void *, const char *);
50 __CPROVER_bool __CPROVER_get_may(const void *, const char *);
51 
52 #endif // CPROVER_CPP_LIBRARY_CPROVER_H
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
typedef __typeof__(sizeof(int)) __CPROVER_size_t
const void * __CPROVER_deallocated
const void * __CPROVER_new_object
const void * __CPROVER_memory_leak
__CPROVER_bool __CPROVER_malloc_is_new_array
void __CPROVER_atomic_end()
void __CPROVER_clear_must(const void *, const char *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
void __CPROVER_array_replace(const void *dest, const void *src)
void __CPROVER_atomic_begin()
void __CPROVER_array_set(const void *dest,...)
signed __CPROVER_POINTER_OFFSET(const void *p)
void __CPROVER_fence(const char *kind,...)
void __CPROVER_output(const char *description,...)
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
unsigned __CPROVER_POINTER_OBJECT(const void *p)
void __CPROVER_set_may(const void *, const char *)
void __CPROVER_precondition(__CPROVER_bool assertion, const char *description)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p)
void __CPROVER_cleanup(const void *, void(*)(void *))
void __CPROVER_clear_may(const void *, const char *)
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
void __CPROVER_set_must(const void *, const char *)
void __CPROVER_array_copy(const void *dest, const void *src)
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__))
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description)
void __CPROVER_input(const char *description,...)
int __gcc_m64 __attribute__((__vector_size__(8), __may_alias__))