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_ANSI_C_LIBRARY_CPROVER_H
10 #define CPROVER_ANSI_C_LIBRARY_CPROVER_H
11 
12 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
13 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
14 extern const void *__CPROVER_deallocated;
15 extern const void *__CPROVER_malloc_object;
16 extern __CPROVER_size_t __CPROVER_malloc_size;
18 extern const void *__CPROVER_memory_leak;
19 
21 extern __CPROVER_size_t __CPROVER_max_malloc_size;
22 extern _Bool __CPROVER_malloc_may_fail;
23 
24 // malloc failure modes
27 
28 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
29 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
30 void __CPROVER_precondition(__CPROVER_bool assertion, const char *description);
31 void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description);
32 
33 _Bool __CPROVER_is_zero_string(const void *);
34 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
35 __CPROVER_size_t __CPROVER_buffer_size(const void *);
36 __CPROVER_bool __CPROVER_r_ok();
37 __CPROVER_bool __CPROVER_w_ok();
38 __CPROVER_bool __CPROVER_rw_ok();
39 
40 #if 0
41 __CPROVER_bool __CPROVER_equal();
42 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
43 
44 const unsigned __CPROVER_constant_infinity_uint;
45 typedef void __CPROVER_integer;
46 typedef void __CPROVER_rational;
47 void __CPROVER_initialize(void);
48 void __CPROVER_cover(__CPROVER_bool condition);
49 #endif
50 
51 void __CPROVER_printf(const char *format, ...);
52 void __CPROVER_input(const char *id, ...);
53 void __CPROVER_output(const char *id, ...);
54 
55 // concurrency-related
58 void __CPROVER_fence(const char *kind, ...);
59 #if 0
60 __CPROVER_thread_local unsigned long __CPROVER_thread_id=0;
61 __CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
62 unsigned long __CPROVER_next_thread_id=0;
63 
64 // traces
65 void CBMC_trace(int lvl, const char *event, ...);
66 #endif
67 
68 // pointers
69 unsigned __CPROVER_POINTER_OBJECT(const void *p);
70 signed __CPROVER_POINTER_OFFSET(const void *p);
71 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
72 #if 0
73 extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];
75  __CPROVER_size_t address, __CPROVER_size_t extent);
76 
77 // this is ANSI-C
78 extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];
79 
80 // this is GCC
81 extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];
82 extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];
83 #endif
84 
85 // float stuff
86 int __CPROVER_fpclassify(int, int, int, int, int, ...);
87 __CPROVER_bool __CPROVER_isfinite(double f);
88 __CPROVER_bool __CPROVER_isinf(double f);
89 __CPROVER_bool __CPROVER_isnormal(double f);
90 __CPROVER_bool __CPROVER_sign(double f);
91 __CPROVER_bool __CPROVER_isnanf(float f);
92 __CPROVER_bool __CPROVER_isnand(double f);
93 __CPROVER_bool __CPROVER_isnanld(long double f);
94 __CPROVER_bool __CPROVER_isfinitef(float f);
95 __CPROVER_bool __CPROVER_isfinited(double f);
96 __CPROVER_bool __CPROVER_isfiniteld(long double f);
97 __CPROVER_bool __CPROVER_isinff(float f);
98 __CPROVER_bool __CPROVER_isinfd(double f);
99 __CPROVER_bool __CPROVER_isinfld(long double f);
100 __CPROVER_bool __CPROVER_isnormalf(float f);
101 __CPROVER_bool __CPROVER_isnormald(double f);
102 __CPROVER_bool __CPROVER_isnormalld(long double f);
103 __CPROVER_bool __CPROVER_signf(float f);
104 __CPROVER_bool __CPROVER_signd(double f);
105 __CPROVER_bool __CPROVER_signld(long double f);
106 double __CPROVER_inf(void);
107 float __CPROVER_inff(void);
108 long double __CPROVER_infl(void);
109 //extern int __CPROVER_thread_local __CPROVER_rounding_mode;
110 int __CPROVER_isgreaterd(double f, double g);
111 
112 // absolute value
113 int __CPROVER_abs(int);
114 long int __CPROVER_labs(long int);
115 long long int __CPROVER_llabs(long long int);
116 double __CPROVER_fabs(double);
117 long double __CPROVER_fabsl(long double);
118 float __CPROVER_fabsf(float);
119 
120 // modulo and remainder
121 double __CPROVER_fmod(double, double);
122 float __CPROVER_fmodf(float, float);
123 long double __CPROVER_fmodl(long double, long double);
124 double __CPROVER_remainder(double, double);
125 float __CPROVER_remainderf(float, float);
126 long double __CPROVER_remainderl(long double, long double);
127 
128 // arrays
129 //__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
130 void __CPROVER_array_copy(const void *dest, const void *src);
131 void __CPROVER_array_set(const void *dest, ...);
132 void __CPROVER_array_replace(const void *dest, const void *src);
133 
134 #if 0
135 // k-induction
136 void __CPROVER_k_induction_hint(unsigned min, unsigned max,
137 unsigned step, unsigned loop_free);
138 
139 // manual specification of predicates
140 void __CPROVER_predicate(__CPROVER_bool predicate);
141 void __CPROVER_parameter_predicates();
142 void __CPROVER_return_predicates();
143 #endif
144 
145 // pipes, write, read, close
147  _Bool widowed;
148  char data[4];
149  short next_avail;
150  short next_unread;
151 };
152 #if 0
153 extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
154 // offset to make sure we don't collide with other fds
155 extern const int __CPROVER_pipe_offset;
156 extern unsigned __CPROVER_pipe_count;
157 #endif
158 
159 void __CPROVER_set_must(const void *, const char *);
160 void __CPROVER_set_may(const void *, const char *);
161 void __CPROVER_clear_must(const void *, const char *);
162 void __CPROVER_clear_may(const void *, const char *);
163 void __CPROVER_cleanup(const void *, void (*)(void *));
164 __CPROVER_bool __CPROVER_get_must(const void *, const char *);
165 __CPROVER_bool __CPROVER_get_may(const void *, const char *);
166 
167 #define __CPROVER_danger_number_of_ops 1
168 #define __CPROVER_danger_max_solution_size 1
169 #define __CPROVER_danger_number_of_vars 1
170 #define __CPROVER_danger_number_of_consts 1
171 
172 // detect overflow
173 __CPROVER_bool __CPROVER_overflow_minus();
174 __CPROVER_bool __CPROVER_overflow_mult();
175 __CPROVER_bool __CPROVER_overflow_plus();
176 __CPROVER_bool __CPROVER_overflow_shl();
178 
179 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H
__CPROVER_malloc_failure_mode_assert_then_assume
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_isnanld
__CPROVER_bool __CPROVER_isnanld(long double f)
__CPROVER_signld
__CPROVER_bool __CPROVER_signld(long double f)
__CPROVER_equal
__CPROVER_bool __CPROVER_equal()
format
static format_containert< T > format(const T &o)
Definition: format.h:37
__CPROVER_isinfd
__CPROVER_bool __CPROVER_isinfd(double f)
__typeof__
typedef __typeof__(sizeof(int)) __CPROVER_size_t
__CPROVER_is_zero_string
_Bool __CPROVER_is_zero_string(const void *)
__CPROVER_fmodf
float __CPROVER_fmodf(float, float)
__CPROVER_atomic_end
void __CPROVER_atomic_end()
__CPROVER_isinff
__CPROVER_bool __CPROVER_isinff(float f)
__CPROVER_overflow_mult
__CPROVER_bool __CPROVER_overflow_mult()
__CPROVER_fpclassify
int __CPROVER_fpclassify(int, int, int, int, int,...)
__CPROVER_malloc_object
const void * __CPROVER_malloc_object
__CPROVER_signf
__CPROVER_bool __CPROVER_signf(float f)
__CPROVER_overflow_plus
__CPROVER_bool __CPROVER_overflow_plus()
__CPROVER_get_may
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
__CPROVER_allocated_memory
void __CPROVER_allocated_memory(__CPROVER_size_t address, __CPROVER_size_t extent)
__CPROVER_llabs
long long int __CPROVER_llabs(long long int)
data
Definition: kdev_t.h:24
__CPROVER_isfinitef
__CPROVER_bool __CPROVER_isfinitef(float f)
__CPROVER_fmodl
long double __CPROVER_fmodl(long double, long double)
__CPROVER_overflow_shl
__CPROVER_bool __CPROVER_overflow_shl()
__CPROVER_pipet::next_unread
short next_unread
Definition: cprover.h:150
__CPROVER_deallocated
const void * __CPROVER_deallocated
__CPROVER_assume
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__))
__CPROVER_infl
long double __CPROVER_infl(void)
__CPROVER_malloc_may_fail
_Bool __CPROVER_malloc_may_fail
__CPROVER_get_must
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
__CPROVER_pipet::widowed
_Bool widowed
Definition: cprover.h:147
__CPROVER_memory_leak
const void * __CPROVER_memory_leak
__CPROVER_output
void __CPROVER_output(const char *id,...)
__CPROVER_array_copy
void __CPROVER_array_copy(const void *dest, const void *src)
__CPROVER_isnand
__CPROVER_bool __CPROVER_isnand(double f)
__CPROVER_malloc_size
__CPROVER_size_t __CPROVER_malloc_size
__CPROVER_atomic_begin
void __CPROVER_atomic_begin()
__CPROVER_buffer_size
__CPROVER_size_t __CPROVER_buffer_size(const void *)
__CPROVER_remainderl
long double __CPROVER_remainderl(long double, long double)
__CPROVER_sign
__CPROVER_bool __CPROVER_sign(double f)
__CPROVER_isinfld
__CPROVER_bool __CPROVER_isinfld(long double f)
__attribute__
int __gcc_m64 __attribute__((__vector_size__(8), __may_alias__))
Definition: gcc_builtin_headers_types.h:4
__CPROVER_malloc_is_new_array
_Bool __CPROVER_malloc_is_new_array
__CPROVER_cleanup
void __CPROVER_cleanup(const void *, void(*)(void *))
__CPROVER_overflow_unary_minus
__CPROVER_bool __CPROVER_overflow_unary_minus()
__CPROVER_labs
long int __CPROVER_labs(long int)
__CPROVER_inff
float __CPROVER_inff(void)
__CPROVER_malloc_failure_mode
int __CPROVER_malloc_failure_mode
__CPROVER_isfinite
__CPROVER_bool __CPROVER_isfinite(double f)
__CPROVER_w_ok
__CPROVER_bool __CPROVER_w_ok()
__CPROVER_fence
void __CPROVER_fence(const char *kind,...)
__CPROVER_printf
void __CPROVER_printf(const char *format,...)
__CPROVER_fmod
double __CPROVER_fmod(double, double)
__CPROVER_set_may
void __CPROVER_set_may(const void *, const char *)
__CPROVER_array_replace
void __CPROVER_array_replace(const void *dest, const void *src)
__CPROVER_set_must
void __CPROVER_set_must(const void *, const char *)
__CPROVER_overflow_minus
__CPROVER_bool __CPROVER_overflow_minus()
__CPROVER_isfinited
__CPROVER_bool __CPROVER_isfinited(double f)
__CPROVER_POINTER_OFFSET
signed __CPROVER_POINTER_OFFSET(const void *p)
__CPROVER_isgreaterd
int __CPROVER_isgreaterd(double f, double g)
__CPROVER_clear_may
void __CPROVER_clear_may(const void *, const char *)
__CPROVER_assert
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
__CPROVER_precondition
void __CPROVER_precondition(__CPROVER_bool assertion, const char *description)
__CPROVER_isinf
__CPROVER_bool __CPROVER_isinf(double f)
__CPROVER_fabsl
long double __CPROVER_fabsl(long double)
__CPROVER_POINTER_OBJECT
unsigned __CPROVER_POINTER_OBJECT(const void *p)
__CPROVER_input
void __CPROVER_input(const char *id,...)
__CPROVER_max_malloc_size
__CPROVER_size_t __CPROVER_max_malloc_size
__CPROVER_abs
int __CPROVER_abs(int)
__CPROVER_fabsf
float __CPROVER_fabsf(float)
__CPROVER_k_induction_hint
void __CPROVER_k_induction_hint(unsigned min, unsigned max, unsigned step, unsigned loop_free)
__CPROVER_remainderf
float __CPROVER_remainderf(float, float)
__CPROVER_cover
void __CPROVER_cover(__CPROVER_bool condition)
__CPROVER_postcondition
void __CPROVER_postcondition(__CPROVER_bool assertion, const char *description)
__CPROVER_pipet::next_avail
short next_avail
Definition: cprover.h:149
__CPROVER_isnanf
__CPROVER_bool __CPROVER_isnanf(float f)
__CPROVER_isfiniteld
__CPROVER_bool __CPROVER_isfiniteld(long double f)
__CPROVER_same_object
__CPROVER_bool __CPROVER_same_object(const void *, const void *)
__CPROVER_inf
double __CPROVER_inf(void)
__CPROVER_isnormalf
__CPROVER_bool __CPROVER_isnormalf(float f)
__CPROVER_fabs
double __CPROVER_fabs(double)
__CPROVER_isnormald
__CPROVER_bool __CPROVER_isnormald(double f)
__CPROVER_allocate
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_zero_string_length
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
__CPROVER_malloc_failure_mode_return_null
int __CPROVER_malloc_failure_mode_return_null
__CPROVER_remainder
double __CPROVER_remainder(double, double)
__CPROVER_isnormalld
__CPROVER_bool __CPROVER_isnormalld(long double f)
__CPROVER_clear_must
void __CPROVER_clear_must(const void *, const char *)
__CPROVER_pipet
Definition: cprover.h:146
__CPROVER_rw_ok
__CPROVER_bool __CPROVER_rw_ok()
__CPROVER_array_set
void __CPROVER_array_set(const void *dest,...)
__CPROVER_isnormal
__CPROVER_bool __CPROVER_isnormal(double f)
__CPROVER_r_ok
__CPROVER_bool __CPROVER_r_ok()
__CPROVER_DYNAMIC_OBJECT
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p)
__CPROVER_signd
__CPROVER_bool __CPROVER_signd(double f)