cprover
cprover_builtin_headers.h
Go to the documentation of this file.
1 // clang-format off
2 void __CPROVER_assume(__CPROVER_bool assumption);
3 void __VERIFIER_assume(__CPROVER_bool assumption);
4 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
5 void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);
6 void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
7 void __CPROVER_havoc_object(void *);
8 void __CPROVER_havoc_slice(void *, __CPROVER_size_t);
9 __CPROVER_bool __CPROVER_equal();
10 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
11 __CPROVER_bool __CPROVER_is_invalid_pointer(const void *);
12 _Bool __CPROVER_is_zero_string(const void *);
13 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
14 __CPROVER_size_t __CPROVER_buffer_size(const void *);
15 __CPROVER_bool __CPROVER_r_ok();
16 __CPROVER_bool __CPROVER_w_ok();
17 __CPROVER_bool __CPROVER_rw_ok();
18 
19 // bitvector analysis
20 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);
21 void __CPROVER_set_must(const void *, const char *);
22 void __CPROVER_clear_must(const void *, const char *);
23 void __CPROVER_set_may(const void *, const char *);
24 void __CPROVER_clear_may(const void *, const char *);
25 void __CPROVER_cleanup(const void *, const void *);
26 __CPROVER_bool __CPROVER_get_must(const void *, const char *);
27 __CPROVER_bool __CPROVER_get_may(const void *, const char *);
28 
29 void __CPROVER_printf(const char *format, ...);
30 void __CPROVER_input(const char *id, ...);
31 void __CPROVER_output(const char *id, ...);
32 void __CPROVER_cover(__CPROVER_bool condition);
33 
34 // concurrency-related
37 void __CPROVER_fence(const char *kind, ...);
38 
39 // contract-related functions
40 __CPROVER_bool __CPROVER_is_fresh(const void *mem, __CPROVER_size_t size);
41 void __CPROVER_old(const void *);
42 void __CPROVER_loop_entry(const void *);
43 
44 // pointers
45 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
47 __CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *);
48 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
49 void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
50 
51 // float stuff
52 int __CPROVER_fpclassify(int, int, int, int, int, ...);
53 __CPROVER_bool __CPROVER_isnanf(float f);
54 __CPROVER_bool __CPROVER_isnand(double f);
55 __CPROVER_bool __CPROVER_isnanld(long double f);
56 __CPROVER_bool __CPROVER_isfinitef(float f);
57 __CPROVER_bool __CPROVER_isfinited(double f);
58 __CPROVER_bool __CPROVER_isfiniteld(long double f);
59 __CPROVER_bool __CPROVER_isinff(float f);
60 __CPROVER_bool __CPROVER_isinfd(double f);
61 __CPROVER_bool __CPROVER_isinfld(long double f);
62 __CPROVER_bool __CPROVER_isnormalf(float f);
63 __CPROVER_bool __CPROVER_isnormald(double f);
64 __CPROVER_bool __CPROVER_isnormalld(long double f);
65 __CPROVER_bool __CPROVER_signf(float f);
66 __CPROVER_bool __CPROVER_signd(double f);
67 __CPROVER_bool __CPROVER_signld(long double f);
68 double __CPROVER_inf(void);
69 float __CPROVER_inff(void);
70 long double __CPROVER_infl(void);
71 int __CPROVER_isgreaterf(float f, float g);
72 int __CPROVER_isgreaterd(double f, double g);
73 int __CPROVER_isgreaterequalf(float f, float g);
74 int __CPROVER_isgreaterequald(double f, double g);
75 int __CPROVER_islessf(float f, float g);
76 int __CPROVER_islessd(double f, double g);
77 int __CPROVER_islessequalf(float f, float g);
78 int __CPROVER_islessequald(double f, double g);
79 int __CPROVER_islessgreaterf(float f, float g);
80 int __CPROVER_islessgreaterd(double f, double g);
81 int __CPROVER_isunorderedf(float f, float g);
82 int __CPROVER_isunorderedd(double f, double g);
83 
84 // absolute value
85 int __CPROVER_abs(int x);
86 long int __CPROVER_labs(long int x);
87 long long int __CPROVER_llabs(long long int x);
88 double __CPROVER_fabs(double x);
89 long double __CPROVER_fabsl(long double x);
90 float __CPROVER_fabsf(float x);
91 
92 // modulo and remainder
93 double __CPROVER_fmod(double, double);
94 float __CPROVER_fmodf(float, float);
95 long double __CPROVER_fmodl(long double, long double);
96 double __CPROVER_remainder(double, double);
97 float __CPROVER_remainderf(float, float);
98 long double __CPROVER_remainderl(long double, long double);
99 
100 // arrays
101 __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
102 // overwrite all of *dest (possibly using nondet values), even
103 // if *src is smaller
104 void __CPROVER_array_copy(const void *dest, const void *src);
105 // replace at most size-of-*src bytes in *dest
106 void __CPROVER_array_replace(const void *dest, const void *src);
107 void __CPROVER_array_set(const void *dest, ...);
108 
109 // k-induction
110 void __CPROVER_k_induction_hint(unsigned min, unsigned max,
111  unsigned step, unsigned loop_free);
112 
113 // format string-related
114 int __CPROVER_scanf(const char *, ...);
115 
116 // detect overflow
117 __CPROVER_bool __CPROVER_overflow_minus();
118 __CPROVER_bool __CPROVER_overflow_mult();
119 __CPROVER_bool __CPROVER_overflow_plus();
120 __CPROVER_bool __CPROVER_overflow_shl();
122 
123 // enumerations
124 __CPROVER_bool __CPROVER_enum_is_in_range();
125 // clang-format on
signed long long __CPROVER_ssize_t
Definition: cprover.h:19
__CPROVER_size_t __CPROVER_buffer_size(const void *)
__CPROVER_bool __CPROVER_enum_is_in_range()
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_isfinitef(float f)
void __CPROVER_atomic_end()
__CPROVER_bool __CPROVER_isnanf(float f)
__CPROVER_bool __CPROVER_overflow_mult()
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_assert(__CPROVER_bool assertion, const char *description)
__CPROVER_bool __CPROVER_rw_ok()
int __CPROVER_isgreaterequalf(float f, float g)
__CPROVER_bool __CPROVER_overflow_unary_minus()
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
__CPROVER_bool __CPROVER_isfinited(double f)
__CPROVER_bool __CPROVER_r_ok()
void __CPROVER_array_replace(const void *dest, const void *src)
long int __CPROVER_labs(long int x)
__CPROVER_bool __CPROVER_isinff(float f)
__CPROVER_bool __CPROVER_is_invalid_pointer(const void *)
void __CPROVER_atomic_begin()
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,...)
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)
__CPROVER_bool __CPROVER_equal()
int __CPROVER_isgreaterf(float f, float g)
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
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 *)
__CPROVER_bool __CPROVER_w_ok()
int __CPROVER_abs(int x)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
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)
void __CPROVER_clear_may(const void *, const char *)
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
__CPROVER_bool __CPROVER_isnanld(long double f)
__CPROVER_bool __CPROVER_isfiniteld(long double f)
__CPROVER_bool __CPROVER_same_object(const void *, const void *)
_Bool __CPROVER_is_zero_string(const void *)
__CPROVER_bool __CPROVER_overflow_plus()
long double __CPROVER_fmodl(long double, long double)
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_isnormalf(float f)
double __CPROVER_fmod(double, double)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
__CPROVER_bool __CPROVER_overflow_minus()
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_overflow_shl()
int __CPROVER_isunorderedf(float f, float g)
__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *)
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description)
void __CPROVER_havoc_object(void *)
__CPROVER_bool __CPROVER_signd(double f)
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)