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< std::pair< exprt, 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_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... | |
optionalt< goto_checkt::conditiont > | get_pointer_is_null_condition (const exprt &address, const exprt &size) |
conditionst | get_pointer_points_to_valid_memory_conditions (const exprt &address, const exprt &size) |
exprt | is_in_bounds_of_some_explicit_allocation (const exprt &pointer, const exprt &size) |
conditionst | get_pointer_dereferenceable_conditions (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 45 of file goto_check.cpp.
|
protected |
Definition at line 280 of file goto_check.cpp.
|
protected |
Definition at line 279 of file goto_check.cpp.
|
protected |
Definition at line 245 of file goto_check.cpp.
|
protected |
Definition at line 173 of file goto_check.cpp.
|
protected |
Definition at line 274 of file goto_check.cpp.
Definition at line 83 of file goto_check.cpp.
|
inline |
Definition at line 48 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 1499 of file goto_check.cpp.
|
protected |
Definition at line 1308 of file goto_check.cpp.
|
protected |
Definition at line 1313 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 1757 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 1681 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 1537 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 1656 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 1643 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 1582 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 1560 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 1605 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 286 of file goto_check.cpp.
Definition at line 522 of file goto_check.cpp.
Definition at line 353 of file goto_check.cpp.
Definition at line 374 of file goto_check.cpp.
Definition at line 906 of file goto_check.cpp.
|
protected |
Definition at line 1295 of file goto_check.cpp.
|
protected |
Definition at line 2245 of file goto_check.cpp.
|
protected |
Definition at line 2159 of file goto_check.cpp.
void goto_checkt::goto_check | ( | const irep_idt & | function_identifier, |
goto_functiont & | goto_function | ||
) |
Definition at line 1826 of file goto_check.cpp.
Definition at line 688 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 323 of file goto_check.cpp.
|
protected |
Definition at line 2272 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 1285 of file goto_check.cpp.
Definition at line 470 of file goto_check.cpp.
check a mod expression for the case INT_MIN % -1
Definition at line 492 of file goto_check.cpp.
Definition at line 1016 of file goto_check.cpp.
Definition at line 1170 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 1241 of file goto_check.cpp.
|
protected |
Definition at line 1127 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 1200 of file goto_check.cpp.
expand the r_ok and w_ok predicates
Definition at line 1764 of file goto_check.cpp.
|
protected |
Definition at line 403 of file goto_check.cpp.
|
protected |
Definition at line 281 of file goto_check.cpp.
|
protected |
Definition at line 246 of file goto_check.cpp.
|
protected |
Definition at line 99 of file goto_check.cpp.
|
protected |
Definition at line 268 of file goto_check.cpp.
|
protected |
Definition at line 269 of file goto_check.cpp.
|
protected |
Definition at line 271 of file goto_check.cpp.
|
protected |
Definition at line 254 of file goto_check.cpp.
|
protected |
Definition at line 270 of file goto_check.cpp.
|
protected |
Definition at line 262 of file goto_check.cpp.
|
protected |
Definition at line 257 of file goto_check.cpp.
|
protected |
Definition at line 258 of file goto_check.cpp.
|
protected |
Definition at line 264 of file goto_check.cpp.
|
protected |
Definition at line 256 of file goto_check.cpp.
|
protected |
Definition at line 266 of file goto_check.cpp.
|
protected |
Definition at line 255 of file goto_check.cpp.
|
protected |
Definition at line 261 of file goto_check.cpp.
|
protected |
Definition at line 272 of file goto_check.cpp.
|
protected |
Definition at line 259 of file goto_check.cpp.
|
protected |
Definition at line 265 of file goto_check.cpp.
|
protected |
Definition at line 263 of file goto_check.cpp.
|
protected |
Definition at line 260 of file goto_check.cpp.
|
protected |
Definition at line 275 of file goto_check.cpp.
|
protected |
Definition at line 100 of file goto_check.cpp.
|
protected |
Definition at line 98 of file goto_check.cpp.
|
protected |
Definition at line 283 of file goto_check.cpp.
|
protected |
Definition at line 244 of file goto_check.cpp.
|
protected |
Definition at line 101 of file goto_check.cpp.
|
protected |
Definition at line 97 of file goto_check.cpp.
|
protected |
Definition at line 267 of file goto_check.cpp.