cprover
|
Classes | |
struct | conditiont |
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
goto_check_ct (const namespacet &_ns, const optionst &_options, message_handlert &_message_handler) | |
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. | |
Protected Types | |
enum | check_statust { ENABLE , DISABLE , CHECKED } |
activation statuses for named checks More... | |
using | guardt = std::function< exprt(exprt)> |
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 |
using | named_check_statust = optionalt< std::pair< irep_idt, check_statust > > |
optional (named-check, status) pair | |
Protected Member Functions | |
void | check_rec_address (const exprt &expr, const 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. | |
void | check_rec_logical_op (const exprt &expr, const guardt &guard) |
Check a logical operation: check each operand in separation while extending the guarding condition as follows. | |
void | check_rec_if (const if_exprt &if_expr, const 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. | |
bool | check_rec_member (const member_exprt &member, const guardt &guard) |
Check that a member expression is valid: | |
void | check_rec_div (const div_exprt &div_expr, const guardt &guard) |
Check that a division is valid: check for division by zero, overflow and NaN (for floating point numbers). | |
void | check_rec_arithmetic_op (const exprt &expr, const guardt &guard) |
Check that an arithmetic operation is valid: overflow check, NaN-check (for floating point numbers), and pointer overflow check. | |
void | check_rec (const exprt &expr, const guardt &guard) |
Recursively descend into expr and run the appropriate check for each sub-expression, while collecting the condition for the check in guard . | |
void | check (const exprt &expr) |
Initiate the recursively analysis of expr with its ‘guard’ set to TRUE. | |
void | bounds_check (const exprt &, const guardt &) |
void | bounds_check_index (const index_exprt &, const guardt &) |
void | bounds_check_bit_count (const unary_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 | |
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. | |
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. | |
bool | requires_pointer_primitive_check (const exprt &expr) |
Returns true if the given expression is a pointer primitive that requires validation of the operand to guard against misuse. | |
optionalt< goto_check_ct::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, w_ok and rw_ok predicates | |
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 . | |
void | invalidate (const exprt &lhs) |
Remove all assertions containing the symbol in lhs as well as all assertions containing dereference. | |
void | add_active_named_check_pragmas (source_locationt &source_location) const |
Adds "checked" pragmas for all currently active named checks on the given source location. | |
void | add_all_disable_named_check_pragmas (source_locationt &source_location) const |
Adds "disable" pragmas for all named checks on the given source location. | |
named_check_statust | match_named_check (const irep_idt &named_check) const |
Matches a named-check string of the form. | |
Definition at line 48 of file goto_check_c.cpp.
|
protected |
Definition at line 307 of file goto_check_c.cpp.
|
protected |
Definition at line 306 of file goto_check_c.cpp.
|
protected |
Definition at line 256 of file goto_check_c.cpp.
|
protected |
Definition at line 181 of file goto_check_c.cpp.
|
protected |
Definition at line 301 of file goto_check_c.cpp.
Definition at line 87 of file goto_check_c.cpp.
|
protected |
Definition at line 108 of file goto_check_c.cpp.
|
protected |
optional (named-check, status) pair
Definition at line 330 of file goto_check_c.cpp.
|
protected |
activation statuses for named checks
Enumerator | |
---|---|
ENABLE | |
DISABLE | |
CHECKED |
Definition at line 322 of file goto_check_c.cpp.
|
inline |
Definition at line 51 of file goto_check_c.cpp.
|
protected |
Adds "checked" pragmas for all currently active named checks on the given source location.
Definition at line 2464 of file goto_check_c.cpp.
|
protected |
Adds "disable" pragmas for all named checks on the given source location.
Definition at line 2472 of file goto_check_c.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 1605 of file goto_check_c.cpp.
|
protected |
Definition at line 1407 of file goto_check_c.cpp.
Definition at line 1412 of file goto_check_c.cpp.
|
protected |
Definition at line 1583 of file goto_check_c.cpp.
|
protected |
Definition at line 1433 of file goto_check_c.cpp.
|
protected |
Initiate the recursively analysis of expr
with its ‘guard’ set to TRUE.
expr | the expression to be checked |
Definition at line 1888 of file goto_check_c.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 1798 of file goto_check_c.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 |
Definition at line 1643 of file goto_check_c.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 |
Definition at line 1771 of file goto_check_c.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 |
Definition at line 1756 of file goto_check_c.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 1693 of file goto_check_c.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 1666 of file goto_check_c.cpp.
|
protected |
Check that a member expression is valid:
member | the expression to be checked |
guard | the condition for the check |
member
or its sub-expressions Definition at line 1716 of file goto_check_c.cpp.
void goto_check_ct::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 358 of file goto_check_c.cpp.
Definition at line 591 of file goto_check_c.cpp.
Definition at line 420 of file goto_check_c.cpp.
Definition at line 441 of file goto_check_c.cpp.
Definition at line 999 of file goto_check_c.cpp.
|
protected |
Definition at line 1394 of file goto_check_c.cpp.
|
protected |
Definition at line 2385 of file goto_check_c.cpp.
|
protected |
Definition at line 2307 of file goto_check_c.cpp.
void goto_check_ct::goto_check | ( | const irep_idt & | function_identifier, |
goto_functiont & | goto_function | ||
) |
Definition at line 2009 of file goto_check_c.cpp.
Definition at line 754 of file goto_check_c.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 390 of file goto_check_c.cpp.
|
protected |
Definition at line 2405 of file goto_check_c.cpp.
|
protected |
Matches a named-check string of the form.
Definition at line 2480 of file goto_check_c.cpp.
Definition at line 537 of file goto_check_c.cpp.
check a mod expression for the case INT_MIN % -1
Definition at line 559 of file goto_check_c.cpp.
Definition at line 1107 of file goto_check_c.cpp.
Definition at line 1259 of file goto_check_c.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 1330 of file goto_check_c.cpp.
|
protected |
Definition at line 1215 of file goto_check_c.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 1289 of file goto_check_c.cpp.
|
protected |
Returns true if the given expression is a pointer primitive that requires validation of the operand to guard against misuse.
expr | expression |
Definition at line 1376 of file goto_check_c.cpp.
expand the r_ok, w_ok and rw_ok predicates
Definition at line 1894 of file goto_check_c.cpp.
|
protected |
Definition at line 470 of file goto_check_c.cpp.
|
protected |
Definition at line 308 of file goto_check_c.cpp.
|
protected |
Definition at line 257 of file goto_check_c.cpp.
|
protected |
Definition at line 103 of file goto_check_c.cpp.
|
protected |
Definition at line 279 of file goto_check_c.cpp.
|
protected |
Definition at line 280 of file goto_check_c.cpp.
|
protected |
Definition at line 282 of file goto_check_c.cpp.
|
protected |
Definition at line 265 of file goto_check_c.cpp.
|
protected |
Definition at line 281 of file goto_check_c.cpp.
|
protected |
Definition at line 273 of file goto_check_c.cpp.
|
protected |
Definition at line 268 of file goto_check_c.cpp.
|
protected |
Definition at line 269 of file goto_check_c.cpp.
|
protected |
Definition at line 275 of file goto_check_c.cpp.
|
protected |
Definition at line 267 of file goto_check_c.cpp.
|
protected |
Definition at line 277 of file goto_check_c.cpp.
|
protected |
Definition at line 266 of file goto_check_c.cpp.
|
protected |
Definition at line 272 of file goto_check_c.cpp.
|
protected |
Definition at line 283 of file goto_check_c.cpp.
|
protected |
Definition at line 270 of file goto_check_c.cpp.
|
protected |
Definition at line 276 of file goto_check_c.cpp.
|
protected |
Definition at line 274 of file goto_check_c.cpp.
|
protected |
Definition at line 271 of file goto_check_c.cpp.
|
protected |
Definition at line 302 of file goto_check_c.cpp.
Definition at line 109 of file goto_check_c.cpp.
|
protected |
Definition at line 102 of file goto_check_c.cpp.
|
protected |
Definition at line 104 of file goto_check_c.cpp.
|
protected |
Definition at line 310 of file goto_check_c.cpp.
|
protected |
Maps a named-check name to the corresponding boolean flag.
Definition at line 286 of file goto_check_c.cpp.
|
protected |
Definition at line 255 of file goto_check_c.cpp.
|
protected |
Definition at line 106 of file goto_check_c.cpp.
|
protected |
Definition at line 101 of file goto_check_c.cpp.
|
protected |
Definition at line 278 of file goto_check_c.cpp.