cprover
|
Classes | |
struct | conditiont |
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
goto_check_javat (const namespacet &_ns, const optionst &_options, message_handlert &_message_handler) | |
void | goto_check (const irep_idt &function_identifier, goto_functiont &goto_function) |
Protected Types | |
using | conditionst = std::list< conditiont > |
typedef std::set< std::pair< exprt, exprt > > | assertionst |
typedef optionst::value_listt | error_labelst |
Protected Member Functions | |
void | check_rec_address (const exprt &expr) |
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... | |
bool | check_rec_member (const member_exprt &member) |
Check that a member expression is valid: More... | |
void | check_rec_div (const div_exprt &div_expr) |
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) |
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) |
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 exprt &) |
void | bounds_check_index (const index_exprt &) |
void | div_by_zero_check (const div_exprt &) |
void | mod_overflow_check (const mod_exprt &) |
check a mod expression for the case INT_MIN % -1 More... | |
void | pointer_validity_check (const dereference_exprt &expr, const exprt &src_expr) |
Generates VCCs for the validity of the given dereferencing operation. More... | |
optionalt< goto_check_javat::conditiont > | get_pointer_is_null_condition (const exprt &address, const exprt &size) |
conditionst | get_pointer_dereferenceable_conditions (const exprt &address, const exprt &size) |
void | integer_overflow_check (const exprt &) |
void | conversion_check (const exprt &) |
void | float_overflow_check (const exprt &) |
void | nan_check (const exprt &) |
optionalt< exprt > | rw_ok_check (exprt) |
expand the r_ok, w_ok and rw_ok predicates More... | |
std::string | array_name (const exprt &) |
void | add_property (const exprt &asserted_expr, const std::string &comment, const std::string &property_class, const source_locationt &source_location, const exprt &src_expr) |
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 |
messaget | log |
goto_programt | new_code |
assertionst | assertions |
bool | enable_bounds_check |
bool | enable_pointer_check |
bool | enable_div_by_zero_check |
bool | enable_signed_overflow_check |
bool | enable_unsigned_overflow_check |
bool | enable_pointer_overflow_check |
bool | enable_conversion_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 |
error_labelst | error_labels |
Definition at line 46 of file goto_check_java.cpp.
|
protected |
Definition at line 178 of file goto_check_java.cpp.
|
protected |
Definition at line 136 of file goto_check_java.cpp.
|
protected |
Definition at line 203 of file goto_check_java.cpp.
Definition at line 76 of file goto_check_java.cpp.
|
inline |
Definition at line 49 of file goto_check_java.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 |
Definition at line 1077 of file goto_check_java.cpp.
|
protected |
Definition at line 920 of file goto_check_java.cpp.
|
protected |
Definition at line 925 of file goto_check_java.cpp.
|
protected |
Definition at line 941 of file goto_check_java.cpp.
|
protected |
Initiate the recursively analysis of expr
with its ‘guard’ set to TRUE.
expr | the expression to be checked |
Definition at line 1250 of file goto_check_java.cpp.
|
protected |
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 |
Definition at line 1197 of file goto_check_java.cpp.
|
protected |
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 |
Definition at line 1110 of file goto_check_java.cpp.
|
protected |
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 |
Definition at line 1184 of file goto_check_java.cpp.
|
protected |
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 |
Definition at line 1171 of file goto_check_java.cpp.
|
protected |
Check that a member expression is valid:
member | the expression to be checked |
member
or its sub-expressions Definition at line 1133 of file goto_check_java.cpp.
|
protected |
Definition at line 285 of file goto_check_java.cpp.
|
protected |
Definition at line 237 of file goto_check_java.cpp.
|
protected |
Definition at line 657 of file goto_check_java.cpp.
|
protected |
Definition at line 908 of file goto_check_java.cpp.
|
protected |
Definition at line 1588 of file goto_check_java.cpp.
void goto_check_javat::goto_check | ( | const irep_idt & | function_identifier, |
goto_functiont & | goto_function | ||
) |
Definition at line 1292 of file goto_check_java.cpp.
|
protected |
Definition at line 441 of file goto_check_java.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 207 of file goto_check_java.cpp.
|
protected |
check a mod expression for the case INT_MIN % -1
Definition at line 256 of file goto_check_java.cpp.
|
protected |
Definition at line 761 of file goto_check_java.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 |
Definition at line 868 of file goto_check_java.cpp.
expand the r_ok, w_ok and rw_ok predicates
Definition at line 1256 of file goto_check_java.cpp.
|
protected |
Definition at line 179 of file goto_check_java.cpp.
|
protected |
Definition at line 85 of file goto_check_java.cpp.
|
protected |
Definition at line 198 of file goto_check_java.cpp.
|
protected |
Definition at line 199 of file goto_check_java.cpp.
|
protected |
Definition at line 201 of file goto_check_java.cpp.
|
protected |
Definition at line 187 of file goto_check_java.cpp.
|
protected |
Definition at line 200 of file goto_check_java.cpp.
|
protected |
Definition at line 193 of file goto_check_java.cpp.
|
protected |
Definition at line 189 of file goto_check_java.cpp.
|
protected |
Definition at line 194 of file goto_check_java.cpp.
|
protected |
Definition at line 196 of file goto_check_java.cpp.
|
protected |
Definition at line 188 of file goto_check_java.cpp.
|
protected |
Definition at line 192 of file goto_check_java.cpp.
|
protected |
Definition at line 190 of file goto_check_java.cpp.
|
protected |
Definition at line 195 of file goto_check_java.cpp.
|
protected |
Definition at line 191 of file goto_check_java.cpp.
|
protected |
Definition at line 204 of file goto_check_java.cpp.
|
protected |
Definition at line 84 of file goto_check_java.cpp.
|
protected |
Definition at line 86 of file goto_check_java.cpp.
|
protected |
Definition at line 177 of file goto_check_java.cpp.
|
protected |
Definition at line 83 of file goto_check_java.cpp.
|
protected |
Definition at line 197 of file goto_check_java.cpp.