cprover
Loading...
Searching...
No Matches
cprover.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module:
4
5Author: 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)
13typedef __typeof__(sizeof(int)) __CPROVER_size_t;
14void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
15extern const void *__CPROVER_deallocated;
16extern const void *__CPROVER_new_object;
18extern const void *__CPROVER_memory_leak;
19
20void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
21void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
22void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
23void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
24
25void __CPROVER_input(const char *description, ...);
26void __CPROVER_output(const char *description, ...);
27
28// concurrency-related
31void __CPROVER_fence(const char *kind, ...);
32
33// pointers
34unsigned __CPROVER_POINTER_OBJECT(const void *p);
35signed __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);
40void __CPROVER_array_copy(const void *dest, const void *src);
41void __CPROVER_array_set(const void *dest, ...);
42void __CPROVER_array_replace(const void *dest, const void *src);
43
44void __CPROVER_set_must(const void *, const char *);
45void __CPROVER_set_may(const void *, const char *);
46void __CPROVER_clear_must(const void *, const char *);
47void __CPROVER_clear_may(const void *, const char *);
48void __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
typedef __typeof__(sizeof(int)) __CPROVER_size_t
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
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__))