cprover
Loading...
Searching...
No Matches
cprover_builtin_headers.h
Go to the documentation of this file.
1// clang-format off
2void __CPROVER_assume(__CPROVER_bool assumption);
3void __VERIFIER_assume(__CPROVER_bool assumption);
4void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
5void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);
6void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
8void __CPROVER_havoc_slice(void *, __CPROVER_size_t);
9__CPROVER_bool __CPROVER_same_object(const void *, const void *);
10__CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
11_Bool __CPROVER_is_zero_string(const void *);
12__CPROVER_size_t __CPROVER_zero_string_length(const void *);
13__CPROVER_size_t __CPROVER_buffer_size(const void *);
14
15// experimental features for CHC encodings -- do not use
16__CPROVER_bool __CPROVER_is_list(const void *); // a singly-linked null-terminated dynamically-allocated list
17__CPROVER_bool __CPROVER_is_dll(const void *);
18__CPROVER_bool __CPROVER_is_cyclic_dll(const void *);
19__CPROVER_bool __CPROVER_is_sentinel_dll(const void *, ...);
20__CPROVER_bool __CPROVER_is_cstring(const char *);
21__CPROVER_size_t __CPROVER_cstrlen(const char *);
22__CPROVER_bool __CPROVER_separate(const void *, const void *, ...);
23
24// bitvector analysis
25__CPROVER_bool __CPROVER_get_flag(const void *, const char *);
26void __CPROVER_set_must(const void *, const char *);
27void __CPROVER_clear_must(const void *, const char *);
28void __CPROVER_set_may(const void *, const char *);
29void __CPROVER_clear_may(const void *, const char *);
30void __CPROVER_cleanup(const void *, const void *);
31__CPROVER_bool __CPROVER_get_must(const void *, const char *);
32__CPROVER_bool __CPROVER_get_may(const void *, const char *);
33
34void __CPROVER_printf(const char *format, ...);
35void __CPROVER_input(const char *id, ...);
36void __CPROVER_output(const char *id, ...);
37void __CPROVER_cover(__CPROVER_bool condition);
38
39// concurrency-related
42void __CPROVER_fence(const char *kind, ...);
43
44// contract-related functions
45__CPROVER_bool __CPROVER_is_freeable(const void *mem);
46__CPROVER_bool __CPROVER_was_freed(const void *mem);
47__CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size);
48__CPROVER_bool __CPROVER_obeys_contract(void (*)(void), void (*)(void));
49// same as pointer_in_range with experimental support in contracts
50__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub);
51void __CPROVER_old(const void *);
52void __CPROVER_loop_entry(const void *);
53
54// pointers
55__CPROVER_bool __CPROVER_LIVE_OBJECT(const void *);
56__CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *);
57__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
58__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *);
59__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
60__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
61__CPROVER_bool __CPROVER_pointer_in_range(const void *, const void *, const void *);
62void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
63
64// float stuff
65int __CPROVER_fpclassify(int, int, int, int, int, ...);
66__CPROVER_bool __CPROVER_isnanf(float f);
67__CPROVER_bool __CPROVER_isnand(double f);
68__CPROVER_bool __CPROVER_isnanld(long double f);
69__CPROVER_bool __CPROVER_isfinitef(float f);
70__CPROVER_bool __CPROVER_isfinited(double f);
71__CPROVER_bool __CPROVER_isfiniteld(long double f);
72__CPROVER_bool __CPROVER_isinff(float f);
73__CPROVER_bool __CPROVER_isinfd(double f);
74__CPROVER_bool __CPROVER_isinfld(long double f);
75__CPROVER_bool __CPROVER_isnormalf(float f);
76__CPROVER_bool __CPROVER_isnormald(double f);
77__CPROVER_bool __CPROVER_isnormalld(long double f);
78__CPROVER_bool __CPROVER_signf(float f);
79__CPROVER_bool __CPROVER_signd(double f);
80__CPROVER_bool __CPROVER_signld(long double f);
81double __CPROVER_inf(void);
82float __CPROVER_inff(void);
83long double __CPROVER_infl(void);
84int __CPROVER_isgreaterf(float f, float g);
85int __CPROVER_isgreaterd(double f, double g);
86int __CPROVER_isgreaterequalf(float f, float g);
87int __CPROVER_isgreaterequald(double f, double g);
88int __CPROVER_islessf(float f, float g);
89int __CPROVER_islessd(double f, double g);
90int __CPROVER_islessequalf(float f, float g);
91int __CPROVER_islessequald(double f, double g);
92int __CPROVER_islessgreaterf(float f, float g);
93int __CPROVER_islessgreaterd(double f, double g);
94int __CPROVER_isunorderedf(float f, float g);
95int __CPROVER_isunorderedd(double f, double g);
96
97// absolute value
98int __CPROVER_abs(int x);
99long int __CPROVER_labs(long int x);
100long long int __CPROVER_llabs(long long int x);
101double __CPROVER_fabs(double x);
102long double __CPROVER_fabsl(long double x);
103float __CPROVER_fabsf(float x);
104
105// modulo and remainder
106double __CPROVER_fmod(double, double);
107float __CPROVER_fmodf(float, float);
108long double __CPROVER_fmodl(long double, long double);
109double __CPROVER_remainder(double, double);
110float __CPROVER_remainderf(float, float);
111long double __CPROVER_remainderl(long double, long double);
112
113// arrays
114__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
115// overwrite all of *dest (possibly using nondet values), even
116// if *src is smaller
117void __CPROVER_array_copy(const void *dest, const void *src);
118// replace at most size-of-*src bytes in *dest
119void __CPROVER_array_replace(const void *dest, const void *src);
120void __CPROVER_array_set(const void *dest, ...);
121
122// k-induction
123void __CPROVER_k_induction_hint(unsigned min, unsigned max, unsigned step, unsigned loop_free);
124
125// format string-related
126int __CPROVER_scanf(const char *, ...);
127
128// contracts
129void __CPROVER_assignable(void *ptr, __CPROVER_size_t size,
130 __CPROVER_bool is_ptr_to_ptr);
132void __CPROVER_object_from(void *ptr);
133void __CPROVER_object_upto(void *ptr, __CPROVER_size_t size);
134void __CPROVER_freeable(void *ptr);
135// clang-format on
__CPROVER_size_t __CPROVER_buffer_size(const void *)
double __CPROVER_fabs(double x)
__CPROVER_bool __CPROVER_isnormalld(long double f)
void __CPROVER_printf(const char *format,...)
void __CPROVER_old(const void *)
float __CPROVER_fmodf(float, float)
__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2)
__CPROVER_bool __CPROVER_isnormald(double f)
__CPROVER_bool __CPROVER_signf(float f)
void __CPROVER_loop_entry(const void *)
__CPROVER_bool __CPROVER_pointer_in_range(const void *, const void *, const void *)
__CPROVER_size_t __CPROVER_cstrlen(const char *)
void __CPROVER_freeable(void *ptr)
__CPROVER_bool __CPROVER_isfinitef(float f)
__CPROVER_bool __CPROVER_separate(const void *, const void *,...)
__CPROVER_bool __CPROVER_isnanf(float f)
void __CPROVER_object_upto(void *ptr, __CPROVER_size_t size)
__CPROVER_bool __CPROVER_pointer_in_range_dfcc(void *lb, void *ptr, void *ub)
float __CPROVER_fabsf(float x)
__CPROVER_bool __CPROVER_isinfld(long double f)
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *)
void __VERIFIER_assume(__CPROVER_bool assumption)
int __CPROVER_islessf(float f, float g)
long double __CPROVER_infl(void)
long double __CPROVER_fabsl(long double x)
int __CPROVER_isgreaterd(double f, double g)
long double __CPROVER_remainderl(long double, long double)
void __CPROVER_clear_must(const void *, const char *)
void __CPROVER_cover(__CPROVER_bool condition)
int __CPROVER_scanf(const char *,...)
void __CPROVER_object_whole(void *ptr)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
__CPROVER_bool __CPROVER_is_dll(const void *)
int __CPROVER_isgreaterequalf(float f, float g)
void __CPROVER_assignable(void *ptr, __CPROVER_size_t size, __CPROVER_bool is_ptr_to_ptr)
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
__CPROVER_bool __CPROVER_isfinited(double f)
void __CPROVER_array_replace(const void *dest, const void *src)
long int __CPROVER_labs(long int x)
__CPROVER_bool __CPROVER_is_list(const void *)
__CPROVER_bool __CPROVER_isinff(float f)
__CPROVER_bool __CPROVER_is_invalid_pointer(const void *)
void __CPROVER_havoc_slice(void *, __CPROVER_size_t)
int __CPROVER_isunorderedd(double f, double g)
void __CPROVER_array_set(const void *dest,...)
int __CPROVER_islessgreaterd(double f, double g)
void __CPROVER_fence(const char *kind,...)
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *)
int __CPROVER_islessgreaterf(float f, float g)
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
int __CPROVER_isgreaterequald(double f, double g)
int __CPROVER_islessd(double f, double g)
int __CPROVER_isgreaterf(float f, float g)
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
__CPROVER_bool __CPROVER_WRITEABLE_OBJECT(const void *)
void __CPROVER_input(const char *id,...)
int __CPROVER_islessequald(double f, double g)
float __CPROVER_inff(void)
void __CPROVER_set_may(const void *, const char *)
int __CPROVER_abs(int x)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
__CPROVER_bool __CPROVER_LIVE_OBJECT(const void *)
void __CPROVER_output(const char *id,...)
int __CPROVER_islessequalf(float f, float g)
__CPROVER_bool __CPROVER_get_flag(const void *, const char *)
long long int __CPROVER_llabs(long long int x)
__CPROVER_bool __CPROVER_isinfd(double f)
__CPROVER_bool __CPROVER_is_freeable(const void *mem)
void __CPROVER_clear_may(const void *, const char *)
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
void __CPROVER_object_from(void *ptr)
__CPROVER_bool __CPROVER_isnanld(long double f)
__CPROVER_bool __CPROVER_isfiniteld(long double f)
__CPROVER_bool __CPROVER_is_cyclic_dll(const void *)
__CPROVER_bool __CPROVER_same_object(const void *, const void *)
_Bool __CPROVER_is_zero_string(const void *)
void __CPROVER_atomic_begin(void)
long double __CPROVER_fmodl(long double, long double)
__CPROVER_bool __CPROVER_was_freed(const void *mem)
double __CPROVER_remainder(double, double)
float __CPROVER_remainderf(float, float)
void __CPROVER_set_must(const void *, const char *)
__CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size)
__CPROVER_bool __CPROVER_is_cstring(const char *)
__CPROVER_bool __CPROVER_isnormalf(float f)
double __CPROVER_fmod(double, double)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
void __CPROVER_atomic_end(void)
double __CPROVER_inf(void)
int __CPROVER_fpclassify(int, int, int, int, int,...)
void __CPROVER_cleanup(const void *, const void *)
void __CPROVER_assume(__CPROVER_bool assumption)
__CPROVER_bool __CPROVER_signld(long double f)
void __CPROVER_array_copy(const void *dest, const void *src)
__CPROVER_bool __CPROVER_isnand(double f)
void __CPROVER_k_induction_hint(unsigned min, unsigned max, unsigned step, unsigned loop_free)
__CPROVER_bool __CPROVER_is_sentinel_dll(const void *,...)
int __CPROVER_isunorderedf(float f, float g)
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description)
void __CPROVER_havoc_object(void *)
__CPROVER_bool __CPROVER_signd(double f)
__CPROVER_bool __CPROVER_obeys_contract(void(*)(void), void(*)(void))
static format_containert< T > format(const T &o)
Definition format.h:37
void precondition(const namespacet &ns, value_setst &value_sets, const goto_programt::const_targett target, const symex_target_equationt &equation, const goto_symex_statet &s, exprt &dest)