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_malloc(__CPROVER_size_t size);
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 
20 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
21 void __CPROVER_assert(__CPROVER_bool assertion, const char *description);
22 
23 __CPROVER_bool __CPROVER_is_zero_string(const void *);
24 __CPROVER_size_t __CPROVER_zero_string_length(const void *);
25 __CPROVER_size_t __CPROVER_buffer_size(const void *);
26 
27 #if 0
28 __CPROVER_bool __CPROVER_equal();
29 __CPROVER_bool __CPROVER_same_object(const void *, const void *);
30 
31 const unsigned __CPROVER_constant_infinity_uint;
32 typedef void __CPROVER_integer;
33 typedef void __CPROVER_rational;
34 void __CPROVER_initialize(void);
35 void __CPROVER_cover(__CPROVER_bool condition);
36 #endif
37 
38 void __CPROVER_input(const char *id, ...);
39 void __CPROVER_output(const char *id, ...);
40 
41 // concurrency-related
44 void __CPROVER_fence(const char *kind, ...);
45 #if 0
46 __CPROVER_thread_local unsigned long __CPROVER_thread_id=0;
47 __CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
48 unsigned long __CPROVER_next_thread_id=0;
49 
50 // traces
51 void CBMC_trace(int lvl, const char *event, ...);
52 #endif
53 
54 // pointers
55 unsigned __CPROVER_POINTER_OBJECT(const void *p);
56 signed __CPROVER_POINTER_OFFSET(const void *p);
57 __CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p);
58 #if 0
59 extern unsigned char __CPROVER_memory[__CPROVER_constant_infinity_uint];
60 void __CPROVER_allocated_memory(
61  __CPROVER_size_t address, __CPROVER_size_t extent);
62 
63 // this is ANSI-C
64 extern __CPROVER_thread_local const char __func__[__CPROVER_constant_infinity_uint];
65 
66 // this is GCC
67 extern __CPROVER_thread_local const char __FUNCTION__[__CPROVER_constant_infinity_uint];
68 extern __CPROVER_thread_local const char __PRETTY_FUNCTION__[__CPROVER_constant_infinity_uint];
69 #endif
70 
71 // float stuff
72 __CPROVER_bool __CPROVER_isfinite(double f);
73 __CPROVER_bool __CPROVER_isinf(double f);
74 __CPROVER_bool __CPROVER_isnormal(double f);
75 __CPROVER_bool __CPROVER_sign(double f);
76 __CPROVER_bool __CPROVER_isnanf(float f);
77 __CPROVER_bool __CPROVER_isnand(double f);
78 __CPROVER_bool __CPROVER_isnanld(long double f);
79 __CPROVER_bool __CPROVER_isfinitef(float f);
80 __CPROVER_bool __CPROVER_isfinited(double f);
81 __CPROVER_bool __CPROVER_isfiniteld(long double f);
82 __CPROVER_bool __CPROVER_isinff(float f);
83 __CPROVER_bool __CPROVER_isinfd(double f);
84 __CPROVER_bool __CPROVER_isinfld(long double f);
85 __CPROVER_bool __CPROVER_isnormalf(float f);
86 __CPROVER_bool __CPROVER_isnormald(double f);
87 __CPROVER_bool __CPROVER_isnormalld(long double f);
88 __CPROVER_bool __CPROVER_signf(float f);
89 __CPROVER_bool __CPROVER_signd(double f);
90 __CPROVER_bool __CPROVER_signld(long double f);
91 double __CPROVER_inf(void);
92 float __CPROVER_inff(void);
93 long double __CPROVER_infl(void);
94 //extern int __CPROVER_thread_local __CPROVER_rounding_mode;
95 int __CPROVER_isgreaterd(double f, double g);
96 
97 // absolute value
98 int __CPROVER_abs(int);
99 long int __CPROVER_labs(long int);
100 long long int __CPROVER_llabs(long long int);
101 double __CPROVER_fabs(double);
102 long double __CPROVER_fabsl(long double);
103 float __CPROVER_fabsf(float);
104 
105 // arrays
106 //__CPROVER_bool __CPROVER_array_equal(const void *array1, const void *array2);
107 void __CPROVER_array_copy(const void *dest, const void *src);
108 void __CPROVER_array_set(const void *dest, ...);
109 void __CPROVER_array_replace(const void *dest, const void *src);
110 
111 #if 0
112 // k-induction
113 void __CPROVER_k_induction_hint(unsigned min, unsigned max,
114 unsigned step, unsigned loop_free);
115 
116 // manual specification of predicates
117 void __CPROVER_predicate(__CPROVER_bool predicate);
118 void __CPROVER_parameter_predicates();
119 void __CPROVER_return_predicates();
120 #endif
121 
122 // pipes, write, read, close
124  _Bool widowed;
125  char data[4];
126  short next_avail;
127  short next_unread;
128 };
129 #if 0
130 extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
131 // offset to make sure we don't collide with other fds
132 extern const int __CPROVER_pipe_offset;
133 extern unsigned __CPROVER_pipe_count;
134 #endif
135 
136 void __CPROVER_set_must(const void *, const char *);
137 void __CPROVER_set_may(const void *, const char *);
138 void __CPROVER_clear_must(const void *, const char *);
139 void __CPROVER_clear_may(const void *, const char *);
140 void __CPROVER_cleanup(const void *, void (*)(void *));
141 __CPROVER_bool __CPROVER_get_must(const void *, const char *);
142 __CPROVER_bool __CPROVER_get_may(const void *, const char *);
143 
144 #define __CPROVER_danger_number_of_ops 1
145 #define __CPROVER_danger_max_solution_size 1
146 #define __CPROVER_danger_number_of_vars 1
147 #define __CPROVER_danger_number_of_consts 1
148 
149 #endif // CPROVER_ANSI_C_LIBRARY_CPROVER_H
long double __CPROVER_fabsl(long double)
_Bool __CPROVER_malloc_is_new_array
const void * __CPROVER_deallocated
void __CPROVER_array_set(const void *dest,...)
void __CPROVER_atomic_end()
__CPROVER_bool __CPROVER_isfinitef(float f)
float __CPROVER_fabsf(float)
float __CPROVER_inff(void)
int __CPROVER_isgreaterd(double f, double g)
__CPROVER_bool __CPROVER_isinfld(long double f)
unsigned __CPROVER_POINTER_OBJECT(const void *p)
const void * __CPROVER_malloc_object
__CPROVER_size_t __CPROVER_malloc_size
_Bool widowed
Definition: cprover.h:124
__CPROVER_bool __CPROVER_isnanld(long double f)
double __CPROVER_inf(void)
long int __CPROVER_labs(long int)
void __CPROVER_atomic_begin()
__CPROVER_size_t __CPROVER_zero_string_length(const void *)
short next_unread
Definition: cprover.h:127
const void * __CPROVER_memory_leak
__CPROVER_bool __CPROVER_isinf(double f)
void __CPROVER_array_copy(const void *dest, const void *src)
double __CPROVER_fabs(double)
__CPROVER_bool __CPROVER_isinfd(double f)
void __CPROVER_clear_may(const void *, const char *)
float __gcc_v4sf __attribute__((__vector_size__(16)))
__CPROVER_bool __CPROVER_signf(float f)
long double __CPROVER_infl(void)
void __CPROVER_set_must(const void *, const char *)
__CPROVER_bool __CPROVER_isfinite(double f)
__CPROVER_bool __CPROVER_signd(double f)
__CPROVER_bool __CPROVER_isinff(float f)
__CPROVER_bool __CPROVER_isnormalld(long double f)
void __CPROVER_clear_must(const void *, const char *)
__CPROVER_size_t __CPROVER_buffer_size(const void *)
void __CPROVER_output(const char *id,...)
void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__))
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *p)
__CPROVER_bool __CPROVER_is_zero_string(const void *)
long long int __CPROVER_llabs(long long int)
short next_avail
Definition: cprover.h:126
void * __CPROVER_malloc(__CPROVER_size_t size)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
int __CPROVER_abs(int)
__CPROVER_bool __CPROVER_signld(long double f)
void __CPROVER_set_may(const void *, const char *)
__CPROVER_bool __CPROVER_isfinited(double f)
void __CPROVER_array_replace(const void *dest, const void *src)
__CPROVER_bool __CPROVER_isnormal(double f)
__CPROVER_bool __CPROVER_sign(double f)
signed __CPROVER_POINTER_OFFSET(const void *p)
void __CPROVER_input(const char *id,...)
__CPROVER_bool __CPROVER_get_may(const void *, const char *)
__CPROVER_bool __CPROVER_isnanf(float f)
void __CPROVER_cleanup(const void *, void(*)(void *))
__CPROVER_bool __CPROVER_get_must(const void *, const char *)
__CPROVER_bool __CPROVER_isfiniteld(long double f)
typedef __typeof__(sizeof(int)) __CPROVER_size_t
Definition: kdev_t.h:24
void __CPROVER_fence(const char *kind,...)
__CPROVER_bool __CPROVER_isnand(double f)
__CPROVER_bool __CPROVER_isnormalf(float f)
__CPROVER_bool __CPROVER_isnormald(double f)