cprover
|
Classes | |
struct | conditiont |
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
goto_checkt (const namespacet &_ns, const optionst &_options) | |
void | goto_check (const irep_idt &function_identifier, goto_functiont &goto_function) |
void | collect_allocations (const goto_functionst &goto_functions) |
Fill the list of allocations allocationst with <address, size> for every allocation instruction. More... | |
Protected Types | |
using | conditionst = std::list< conditiont > |
typedef std::set< exprt > | assertionst |
typedef optionst::value_listt | error_labelst |
typedef std::pair< exprt, exprt > | allocationt |
typedef std::list< allocationt > | allocationst |
Protected Member Functions | |
void | check_rec_address (const exprt &expr, guardt &guard) |
Check an address-of expression: if it is a dereference then check the pointer if it is an index then address-check the array and then check the index. More... | |
void | check_rec_logical_op (const exprt &expr, guardt &guard) |
Check a logical operation: check each operand in separation while extending the guarding condition as follows. More... | |
void | check_rec_if (const if_exprt &if_expr, guardt &guard) |
Check an if expression: check the if-condition alone, and then check the true/false-cases with the guard extended with if-condition and it's negation, respectively. More... | |
bool | check_rec_member (const member_exprt &member, guardt &guard) |
Check that a member expression is valid: More... | |
void | check_rec_div (const div_exprt &div_expr, guardt &guard) |
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers). More... | |
void | check_rec_arithmetic_op (const exprt &expr, guardt &guard) |
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check. More... | |
void | check_rec (const exprt &expr, guardt &guard) |
Recursively descend into expr and run the appropriate check for each sub-expression, while collecting the condition for the check in guard . More... | |
void | check (const exprt &expr) |
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE. More... | |
void | bounds_check (const index_exprt &, const guardt &) |
void | div_by_zero_check (const div_exprt &, const guardt &) |
void | mod_by_zero_check (const mod_exprt &, const guardt &) |
void | mod_overflow_check (const mod_exprt &, const guardt &) |
check a mod expression for the case INT_MIN % -1 More... | |
void | enum_range_check (const exprt &, const guardt &) |
void | undefined_shift_check (const shift_exprt &, const guardt &) |
void | pointer_rel_check (const binary_relation_exprt &, const guardt &) |
void | pointer_overflow_check (const exprt &, const guardt &) |
void | pointer_validity_check (const dereference_exprt &expr, const exprt &src_expr, const guardt &guard) |
Generates VCCs for the validity of the given dereferencing operation. More... | |
void | pointer_primitive_check (const exprt &expr, const guardt &guard) |
Generates VCCs to check that pointers passed to pointer primitives are either null or valid. More... | |
bool | is_pointer_primitive (const exprt &expr) |
Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok() More... | |
conditionst | address_check (const exprt &address, const exprt &size) |
void | integer_overflow_check (const exprt &, const guardt &) |
void | conversion_check (const exprt &, const guardt &) |
void | float_overflow_check (const exprt &, const guardt &) |
void | nan_check (const exprt &, const guardt &) |
optionalt< exprt > | rw_ok_check (exprt) |
expand the r_ok and w_ok predicates More... | |
std::string | array_name (const exprt &) |
void | add_guarded_property (const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr, const guardt &guard) |
Include the asserted_expr in the code conditioned by the guard . More... | |
void | invalidate (const exprt &lhs) |
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference. More... | |
Protected Attributes | |
const namespacet & | ns |
std::unique_ptr< local_bitvector_analysist > | local_bitvector_analysis |
goto_programt::const_targett | current_target |
guard_managert | guard_manager |
bool | no_enum_check |
goto_programt | new_code |
assertionst | assertions |
bool | enable_bounds_check |
bool | enable_pointer_check |
bool | enable_memory_leak_check |
bool | enable_div_by_zero_check |
bool | enable_enum_range_check |
bool | enable_signed_overflow_check |
bool | enable_unsigned_overflow_check |
bool | enable_pointer_overflow_check |
bool | enable_conversion_check |
bool | enable_undefined_shift_check |
bool | enable_float_overflow_check |
bool | enable_simplify |
bool | enable_nan_check |
bool | retain_trivial |
bool | enable_assert_to_assume |
bool | enable_assertions |
bool | enable_built_in_assertions |
bool | enable_assumptions |
bool | enable_pointer_primitive_check |
error_labelst | error_labels |
allocationst | allocations |
irep_idt | mode |
Definition at line 42 of file goto_check.cpp.
|
protected |
Definition at line 266 of file goto_check.cpp.
|
protected |
Definition at line 265 of file goto_check.cpp.
|
protected |
Definition at line 231 of file goto_check.cpp.
|
protected |
Definition at line 170 of file goto_check.cpp.
|
protected |
Definition at line 260 of file goto_check.cpp.
Definition at line 80 of file goto_check.cpp.
|
inline |
Definition at line 45 of file goto_check.cpp.
|
protected |
Include the asserted_expr
in the code conditioned by the guard
.
asserted_expr | expression to be asserted |
comment | human readable comment |
property_class | classification of the property |
source_location | the source location of the original expression |
src_expr | the original expression to be included in the comment |
guard | the condition under which the asserted expression should be taken into account |
Definition at line 1581 of file goto_check.cpp.
|
protected |
Definition at line 1257 of file goto_check.cpp.
|
protected |
Definition at line 1375 of file goto_check.cpp.
|
protected |
Definition at line 1380 of file goto_check.cpp.
|
protected |
Initiate the recursively analysis of expr
with its ‘guard’ set to TRUE.
expr | the expression to be checked |
Definition at line 1831 of file goto_check.cpp.
Recursively descend into expr
and run the appropriate check for each sub-expression, while collecting the condition for the check in guard
.
expr | the expression to be checked |
guard | the condition for when the check should be made |
Definition at line 1755 of file goto_check.cpp.
Check an address-of expression: if it is a dereference then check the pointer if it is an index then address-check the array and then check the index.
expr | the expression to be checked |
guard | the condition for the check (unmodified here) |
Definition at line 1619 of file goto_check.cpp.
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check.
expr | the expression to be checked |
guard | the condition for the check (unmodified here) |
Definition at line 1738 of file goto_check.cpp.
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers).
div_expr | the expression to be checked |
guard | the condition for the check (unmodified here) |
Definition at line 1725 of file goto_check.cpp.
Check an if expression: check the if-condition alone, and then check the true/false-cases with the guard extended with if-condition and it's negation, respectively.
if_expr | the expression to be checked |
guard | the condition for the check (extended with the (negation of the) if-condition for recursively calls) |
Definition at line 1664 of file goto_check.cpp.
Check a logical operation: check each operand in separation while extending the guarding condition as follows.
a /\ b /\ c ==> check(a, TRUE), check(b, a), check (c, a /\ b) a \/ b \/ c ==> check(a, TRUE), check(b, ~a), check (c, ~a /\ ~b)
expr | the expression to be checked |
guard | the condition for the check (extended with the previous operands (or their negations) for recursively calls) |
Definition at line 1642 of file goto_check.cpp.
|
protected |
Check that a member expression is valid:
member | the expression to be checked |
guard | the condition for the check (unmodified here) |
member
or its sub-expressions Definition at line 1687 of file goto_check.cpp.
void goto_checkt::collect_allocations | ( | const goto_functionst & | goto_functions | ) |
Fill the list of allocations allocationst with <address, size> for every allocation instruction.
Also check that each allocation is well-formed.
goto_functions | goto functions from which the allocations are to be collected |
Definition at line 272 of file goto_check.cpp.
Definition at line 499 of file goto_check.cpp.
Definition at line 330 of file goto_check.cpp.
Definition at line 351 of file goto_check.cpp.
Definition at line 883 of file goto_check.cpp.
void goto_checkt::goto_check | ( | const irep_idt & | function_identifier, |
goto_functiont & | goto_function | ||
) |
Definition at line 1900 of file goto_check.cpp.
Definition at line 665 of file goto_check.cpp.
|
protected |
Remove all assertions containing the symbol in lhs
as well as all assertions containing dereference.
lhs | the left-hand-side expression whose symbol should be invalidated |
Definition at line 304 of file goto_check.cpp.
|
protected |
Returns true if the given expression is a pointer primitive such as __CPROVER_r_ok()
expr | expression |
Definition at line 1246 of file goto_check.cpp.
Definition at line 447 of file goto_check.cpp.
check a mod expression for the case INT_MIN % -1
Definition at line 469 of file goto_check.cpp.
Definition at line 993 of file goto_check.cpp.
Definition at line 1131 of file goto_check.cpp.
Generates VCCs to check that pointers passed to pointer primitives are either null or valid.
expr | the pointer primitive expression |
guard | the condition under which the operation happens |
Definition at line 1198 of file goto_check.cpp.
|
protected |
Definition at line 1104 of file goto_check.cpp.
|
protected |
Generates VCCs for the validity of the given dereferencing operation.
expr | the expression to be checked |
src_expr | The expression as found in the program, prior to any rewriting |
guard | the condition under which the operation happens |
Definition at line 1157 of file goto_check.cpp.
expand the r_ok and w_ok predicates
Definition at line 1838 of file goto_check.cpp.
|
protected |
Definition at line 380 of file goto_check.cpp.
|
protected |
Definition at line 267 of file goto_check.cpp.
|
protected |
Definition at line 232 of file goto_check.cpp.
|
protected |
Definition at line 96 of file goto_check.cpp.
|
protected |
Definition at line 254 of file goto_check.cpp.
|
protected |
Definition at line 255 of file goto_check.cpp.
|
protected |
Definition at line 257 of file goto_check.cpp.
|
protected |
Definition at line 240 of file goto_check.cpp.
|
protected |
Definition at line 256 of file goto_check.cpp.
|
protected |
Definition at line 248 of file goto_check.cpp.
|
protected |
Definition at line 243 of file goto_check.cpp.
|
protected |
Definition at line 244 of file goto_check.cpp.
|
protected |
Definition at line 250 of file goto_check.cpp.
|
protected |
Definition at line 242 of file goto_check.cpp.
|
protected |
Definition at line 252 of file goto_check.cpp.
|
protected |
Definition at line 241 of file goto_check.cpp.
|
protected |
Definition at line 247 of file goto_check.cpp.
|
protected |
Definition at line 258 of file goto_check.cpp.
|
protected |
Definition at line 245 of file goto_check.cpp.
|
protected |
Definition at line 251 of file goto_check.cpp.
|
protected |
Definition at line 249 of file goto_check.cpp.
|
protected |
Definition at line 246 of file goto_check.cpp.
|
protected |
Definition at line 261 of file goto_check.cpp.
|
protected |
Definition at line 97 of file goto_check.cpp.
|
protected |
Definition at line 95 of file goto_check.cpp.
|
protected |
Definition at line 269 of file goto_check.cpp.
|
protected |
Definition at line 230 of file goto_check.cpp.
|
protected |
Definition at line 98 of file goto_check.cpp.
|
protected |
Definition at line 94 of file goto_check.cpp.
|
protected |
Definition at line 253 of file goto_check.cpp.