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