cprover
cprover_builtin_headers.h
Go to the documentation of this file.
1 void __CPROVER_assume(__CPROVER_bool assumption);
2 void __VERIFIER_assume(__CPROVER_bool assumption);
3 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
4 void __CPROVER_precondition(__CPROVER_bool precondition, const char *description);
5 void __CPROVER_havoc_object(void *);
6 __CPROVER_bool __CPROVER_equal();
7 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
8 __CPROVER_bool __CPROVER_invalid_pointer(const void *);
9 __CPROVER_bool __CPROVER_is_zero_string(const void *);
10 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
11 __CPROVER_size_t __CPROVER_buffer_size(const void *);
12 
13 // bitvector analysis
14 __CPROVER_bool __CPROVER_get_flag(const void *, const char *);
15 void __CPROVER_set_must(const void *, const char *);
16 void __CPROVER_clear_must(const void *, const char *);
17 void __CPROVER_set_may(const void *, const char *);
18 void __CPROVER_clear_may(const void *, const char *);
19 void __CPROVER_cleanup(const void *, const void *);
20 __CPROVER_bool __CPROVER_get_must(const void *, const char *);
21 __CPROVER_bool __CPROVER_get_may(const void *, const char *);
22 
23 void __CPROVER_input(const char *id, ...);
24 void __CPROVER_output(const char *id, ...);
25 void __CPROVER_cover(__CPROVER_bool condition);
26 
27 // concurrency-related
30 void __CPROVER_fence(const char *kind, ...);
31 
32 // traces
33 void CBMC_trace(int lvl, const char *event, ...);
34 
35 // pointers
36 __CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *);
37 __CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *);
38 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *);
39 void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent);
40 
41 // float stuff
42 int __CPROVER_fpclassify(int, int, int, int, int, ...);
43 __CPROVER_bool __CPROVER_isnanf(float f);
44 __CPROVER_bool __CPROVER_isnand(double f);
45 __CPROVER_bool __CPROVER_isnanld(long double f);
46 __CPROVER_bool __CPROVER_isfinitef(float f);
47 __CPROVER_bool __CPROVER_isfinited(double f);
48 __CPROVER_bool __CPROVER_isfiniteld(long double f);
49 __CPROVER_bool __CPROVER_isinff(float f);
50 __CPROVER_bool __CPROVER_isinfd(double f);
51 __CPROVER_bool __CPROVER_isinfld(long double f);
52 __CPROVER_bool __CPROVER_isnormalf(float f);
53 __CPROVER_bool __CPROVER_isnormald(double f);
54 __CPROVER_bool __CPROVER_isnormalld(long double f);
55 __CPROVER_bool __CPROVER_signf(float f);
56 __CPROVER_bool __CPROVER_signd(double f);
57 __CPROVER_bool __CPROVER_signld(long double f);
58 double __CPROVER_inf(void);
59 float __CPROVER_inff(void);
60 long double __CPROVER_infl(void);
61 int __CPROVER_isgreaterf(float f, float g);
62 int __CPROVER_isgreaterd(double f, double g);
63 int __CPROVER_isgreaterequalf(float f, float g);
64 int __CPROVER_isgreaterequald(double f, double g);
65 int __CPROVER_islessf(float f, float g);
66 int __CPROVER_islessd(double f, double g);
67 int __CPROVER_islessequalf(float f, float g);
68 int __CPROVER_islessequald(double f, double g);
69 int __CPROVER_islessgreaterf(float f, float g);
70 int __CPROVER_islessgreaterd(double f, double g);
71 int __CPROVER_isunorderedf(float f, float g);
72 int __CPROVER_isunorderedd(double f, double g);
73 
74 // absolute value
75 int __CPROVER_abs(int x);
76 long int __CPROVER_labs(long int x);
77 long int __CPROVER_llabs(long long int x);
78 double __CPROVER_fabs(double x);
79 long double __CPROVER_fabsl(long double x);
80 float __CPROVER_fabsf(float x);
81 
82 // arrays
83 __CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
84 // overwrite all of *dest (possibly using nondet values), even
85 // if *src is smaller
86 void __CPROVER_array_copy(const void *dest, const void *src);
87 // replace at most size-of-*src bytes in *dest
88 void __CPROVER_array_replace(const void *dest, const void *src);
89 void __CPROVER_array_set(const void *dest, ...);
90 
91 // k-induction
92 void __CPROVER_k_induction_hint(unsigned min, unsigned max,
93  unsigned step, unsigned loop_free);
94 
95 // format string-related
96 int __CPROVER_scanf(const char *, ...);
97 
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
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)
int __CPROVER_isunorderedf(float f, float g)
int __CPROVER_islessgreaterf(float f, float g)
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
long int __CPROVER_llabs(long long int x)
void CBMC_trace(int lvl, const char *event,...)
void __CPROVER_set_must(const void *, const char *)
int __CPROVER_islessequalf(float f, float g)
int __CPROVER_islessf(float f, float g)
int __CPROVER_fpclassify(int, int, int, int, int,...)
int __CPROVER_isgreaterequalf(float f, float g)
void __CPROVER_array_replace(const void *dest, const void *src)
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
int __CPROVER_scanf(const char *,...)
void __CPROVER_clear_must(const void *, const char *)
void __CPROVER_input(const char *id,...)
double __CPROVER_inf(void)
__CPROVER_bool __CPROVER_isnormalf(float f)
void __CPROVER_assume(__CPROVER_bool assumption)
int __CPROVER_isgreaterd(double f, double g)
int __CPROVER_islessequald(double f, double g)
void __CPROVER_clear_may(const void *, const char *)
long int __CPROVER_labs(long int x)
__CPROVER_bool __CPROVER_isnanld(long double f)
void __CPROVER_atomic_end()
__CPROVER_bool __CPROVER_isinfld(long double f)
__CPROVER_bool __CPROVER_isinfd(double f)
int __CPROVER_islessd(double f, double g)
__CPROVER_bool __CPROVER_isfiniteld(long double f)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
__CPROVER_bool __CPROVER_isfinited(double f)
void __CPROVER_havoc_object(void *)
void __CPROVER_array_set(const void *dest,...)
__CPROVER_size_t __CPROVER_buffer_size(const void *)
__CPROVER_bool __CPROVER_is_zero_string(const void *)
void __CPROVER_atomic_begin()
double __CPROVER_fabs(double x)
float __CPROVER_fabsf(float x)
void __CPROVER_output(const char *id,...)
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
__CPROVER_ssize_t __CPROVER_POINTER_OFFSET(const void *)
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_bool __CPROVER_isnormalld(long double f)
void __CPROVER_cover(__CPROVER_bool condition)
__CPROVER_bool __CPROVER_isinff(float f)
int __CPROVER_isgreaterf(float f, float g)
void __CPROVER_set_may(const void *, const char *)
__CPROVER_bool __CPROVER_signf(float f)
__CPROVER_bool __CPROVER_isfinitef(float f)
__CPROVER_bool __CPROVER_isnanf(float f)
int __CPROVER_abs(int x)
__CPROVER_bool __CPROVER_same_object(const void *, const void *)
void __CPROVER_k_induction_hint(unsigned min, unsigned max, unsigned step, unsigned loop_free)
__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
int __CPROVER_islessgreaterd(double f, double g)
void __VERIFIER_assume(__CPROVER_bool assumption)
__CPROVER_bool __CPROVER_isnand(double f)
void __CPROVER_precondition(__CPROVER_bool precondition, const char *description)
void __CPROVER_array_copy(const void *dest, const void *src)
__CPROVER_bool __CPROVER_isnormald(double f)
__CPROVER_bool __CPROVER_get_flag(const void *, const char *)
float __CPROVER_inff(void)
__CPROVER_bool __CPROVER_signd(double f)
int __CPROVER_isgreaterequald(double f, double g)
long double __CPROVER_infl(void)
void __CPROVER_cleanup(const void *, const void *)
__CPROVER_bool __CPROVER_signld(long double f)
int __CPROVER_isunorderedd(double f, double g)
__CPROVER_bool __CPROVER_equal()
void __CPROVER_fence(const char *kind,...)
__CPROVER_bool __CPROVER_invalid_pointer(const void *)
long double __CPROVER_fabsl(long double x)