cprover
|
Public Types | |
typedef goto_functionst::goto_functiont | goto_functiont |
Public Member Functions | |
goto_checkt (const namespacet &_ns, const optionst &_options) | |
void | goto_check (goto_functiont &goto_function, const irep_idt &mode) |
void | collect_allocations (const goto_functionst &goto_functions) |
Protected Types | |
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 (const exprt &expr, guardt &guard, bool address, const irep_idt &mode) |
void | check (const exprt &expr, const irep_idt &mode) |
void | bounds_check (const index_exprt &expr, const guardt &guard) |
void | div_by_zero_check (const div_exprt &expr, const guardt &guard) |
void | mod_by_zero_check (const mod_exprt &expr, const guardt &guard) |
void | undefined_shift_check (const shift_exprt &expr, const guardt &guard) |
void | pointer_rel_check (const exprt &expr, const guardt &guard) |
void | pointer_overflow_check (const exprt &expr, const guardt &guard) |
void | pointer_validity_check (const dereference_exprt &expr, const guardt &guard, const exprt &access_lb, const exprt &access_ub, const irep_idt &mode) |
void | integer_overflow_check (const exprt &expr, const guardt &guard) |
void | conversion_check (const exprt &expr, const guardt &guard) |
void | float_overflow_check (const exprt &expr, const guardt &guard) |
void | nan_check (const exprt &expr, const guardt &guard) |
std::string | array_name (const exprt &expr) |
void | add_guarded_claim (const exprt &expr, const std::string &comment, const std::string &property_class, const source_locationt &, const exprt &src_expr, const guardt &guard) |
void | invalidate (const exprt &lhs) |
Static Protected Member Functions | |
static bool | has_dereference (const exprt &src) |
Protected Attributes | |
const namespacet & | ns |
local_bitvector_analysist * | local_bitvector_analysis |
goto_programt::const_targett | t |
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_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 |
error_labelst | error_labels |
allocationst | allocations |
Definition at line 33 of file goto_check.cpp.
|
protected |
Definition at line 145 of file goto_check.cpp.
|
protected |
Definition at line 144 of file goto_check.cpp.
|
protected |
Definition at line 113 of file goto_check.cpp.
|
protected |
Definition at line 141 of file goto_check.cpp.
typedef goto_functionst::goto_functiont goto_checkt::goto_functiont |
Definition at line 67 of file goto_check.cpp.
|
inline |
Definition at line 36 of file goto_check.cpp.
References enable_assert_to_assume, enable_assertions, enable_assumptions, enable_bounds_check, enable_built_in_assertions, enable_conversion_check, enable_div_by_zero_check, enable_float_overflow_check, enable_memory_leak_check, enable_nan_check, enable_pointer_check, enable_pointer_overflow_check, enable_signed_overflow_check, enable_simplify, enable_undefined_shift_check, enable_unsigned_overflow_check, error_labels, optionst::get_bool_option(), optionst::get_list_option(), and retain_trivial.
|
protected |
Definition at line 1236 of file goto_check.cpp.
References goto_program_templatet< codeT, guardT >::add_instruction(), guardt::as_expr(), ASSERT, assertions, ASSUME, comment(), enable_assert_to_assume, enable_simplify, from_expr(), exprt::is_true(), exprt::move_to_operands(), new_code, ns, retain_trivial, simplify(), irept::swap(), and t.
Referenced by bounds_check(), conversion_check(), div_by_zero_check(), float_overflow_check(), goto_check(), integer_overflow_check(), mod_by_zero_check(), nan_check(), pointer_overflow_check(), pointer_rel_check(), pointer_validity_check(), and undefined_shift_check().
|
protected |
Definition at line 1076 of file goto_check.cpp.
References array_name(), and ns.
Referenced by bounds_check().
|
protected |
Definition at line 1081 of file goto_check.cpp.
References add_guarded_claim(), index_exprt::array(), array_name(), object_descriptor_exprt::build(), dynamic_object(), dynamic_size(), enable_bounds_check, irept::find(), exprt::find_source_location(), namespace_baset::follow(), from_integer(), irept::get_bool(), irept::id(), irept::id_string(), index_exprt::index(), irept::is_nil(), irept::is_not_nil(), exprt::is_zero(), exprt::make_typecast(), malloc_object(), ns, object_size(), object_descriptor_exprt::offset(), exprt::op0(), exprt::op1(), pointer_offset(), object_descriptor_exprt::root_object(), array_typet::size(), vector_typet::size(), size_of_expr(), to_array_type(), to_dereference_expr(), to_integer(), to_vector_type(), and exprt::type().
Referenced by check_rec().
|
protected |
Definition at line 1283 of file goto_check.cpp.
References guardt::add(), bounds_check(), conversion_check(), div_by_zero_check(), float_overflow_check(), forall_operands, irept::id(), irept::id_string(), integer_overflow_check(), exprt::is_boolean(), irept::is_not_nil(), member_offset(), member_offset_expr(), mod_by_zero_check(), nan_check(), ns, exprt::op0(), exprt::op1(), exprt::op2(), exprt::operands(), pointer_overflow_check(), pointer_rel_check(), pointer_validity_check(), irept::pretty(), size_of_expr(), member_exprt::struct_op(), irept::swap(), to_dereference_expr(), to_div_expr(), to_index_expr(), to_member_expr(), to_mod_expr(), to_shift_expr(), exprt::type(), and undefined_shift_check().
Referenced by check().
void goto_checkt::collect_allocations | ( | const goto_functionst & | goto_functions | ) |
Definition at line 149 of file goto_check.cpp.
References allocations, code_function_callt::arguments(), CPROVER_PREFIX, enable_pointer_check, forall_goto_functions, forall_goto_program_instructions, code_function_callt::function(), irept::id(), to_code_function_call(), and to_symbol_expr().
Definition at line 318 of file goto_check.cpp.
References add_guarded_claim(), enable_conversion_check, exprt::find_source_location(), namespace_baset::follow(), from_integer(), ieee_floatt::from_integer(), bitvector_typet::get_width(), irept::id(), binary_relation_exprt::lhs(), ns, exprt::op0(), exprt::operands(), power(), binary_relation_exprt::rhs(), ieee_floatt::to_expr(), to_floatbv_type(), to_signedbv_type(), to_unsignedbv_type(), and exprt::type().
Referenced by check_rec().
Definition at line 215 of file goto_check.cpp.
References add_guarded_claim(), exprt::copy_to_operands(), enable_div_by_zero_check, exprt::find_source_location(), from_integer(), irept::id_string(), irept::is_nil(), exprt::op1(), and exprt::type().
Referenced by check_rec().
Definition at line 618 of file goto_check.cpp.
References add_guarded_claim(), enable_float_overflow_check, exprt::find_source_location(), namespace_baset::follow(), irept::id(), make_binary(), ns, exprt::op0(), exprt::op1(), exprt::operands(), and exprt::type().
Referenced by check_rec().
void goto_checkt::goto_check | ( | goto_functiont & | goto_function, |
const irep_idt & | mode | ||
) |
Definition at line 1469 of file goto_check.cpp.
References add_guarded_claim(), goto_program_templatet< codeT, guardT >::add_instruction(), code_function_callt::arguments(), ASSERT, assertions, ASSIGN, ASSUME, base_type_eq(), check(), goto_program_templatet< codeT, guardT >::clear(), CPROVER_PREFIX, local_bitvector_analysist::dirty, enable_assert_to_assume, enable_assertions, enable_assumptions, enable_built_in_assertions, enable_memory_leak_check, enable_pointer_check, goto_functions_templatet< goto_programt >::entry_point(), error_labels, Forall_goto_program_instructions, forall_operands, code_function_callt::function(), local_bitvector_analysist::get(), irept::get(), irept::id(), goto_program_templatet< codeT, guardT >::insert_before_swap(), goto_program_templatet< codeT, guardT >::instructions, invalidate(), local_bitvector_analysist::flagst::is_null(), local_bitvector_analysist::flagst::is_unknown(), code_assignt::lhs(), local_bitvector_analysis, namespacet::lookup(), exprt::make_typecast(), new_code, ns, exprt::op0(), retain_trivial, code_assignt::rhs(), source_locationt::set_function(), SKIP, typet::subtype(), symbolt::symbol_expr(), t, to_code_assign(), to_code_function_call(), to_code_type(), to_pointer_type(), to_symbol_expr(), symbolt::type, and exprt::type().
|
inlinestaticprotected |
Definition at line 118 of file goto_check.cpp.
References has_subexpr().
Referenced by invalidate().
Definition at line 497 of file goto_check.cpp.
References add_guarded_claim(), enable_signed_overflow_check, enable_unsigned_overflow_check, exprt::find_source_location(), namespace_baset::follow(), from_integer(), irept::id(), irept::id_string(), ns, exprt::op0(), exprt::op1(), exprt::operands(), signedbv_typet::smallest_expr(), to_signedbv_type(), and exprt::type().
Referenced by check_rec().
|
protected |
Definition at line 181 of file goto_check.cpp.
References index_exprt::array(), assertions, has_dereference(), has_symbol(), irept::id(), member_exprt::struct_op(), to_index_expr(), to_member_expr(), and to_symbol_expr().
Referenced by goto_check().
Definition at line 292 of file goto_check.cpp.
References add_guarded_claim(), exprt::copy_to_operands(), enable_div_by_zero_check, exprt::find_source_location(), from_integer(), irept::id_string(), irept::is_nil(), exprt::op1(), and exprt::type().
Referenced by check_rec().
Definition at line 740 of file goto_check.cpp.
References add_guarded_claim(), enable_nan_check, exprt::find_source_location(), from_integer(), irept::id(), irept::id_string(), make_binary(), exprt::make_not(), ieee_floatt::minus_infinity(), exprt::op0(), exprt::op1(), exprt::operands(), ieee_floatt::plus_infinity(), ieee_floatt::to_expr(), to_floatbv_type(), and exprt::type().
Referenced by check_rec().
Definition at line 879 of file goto_check.cpp.
References add_guarded_claim(), enable_pointer_overflow_check, exprt::find_source_location(), irept::id(), irept::id_string(), and exprt::operands().
Referenced by check_rec().
Definition at line 849 of file goto_check.cpp.
References add_guarded_claim(), enable_pointer_check, exprt::find_source_location(), irept::id(), irept::id_string(), exprt::op0(), exprt::op1(), exprt::operands(), same_object(), and exprt::type().
Referenced by check_rec().
|
protected |
Definition at line 905 of file goto_check.cpp.
References add_guarded_claim(), allocations, base_type_eq(), dead_object(), deallocated(), disjunction(), dynamic_object(), dynamic_object_lower_bound(), dynamic_object_upper_bound(), enable_pointer_check, exprt::find_source_location(), namespace_baset::follow(), local_bitvector_analysist::get(), invalid_pointer(), local_bitvector_analysist::flagst::is_dynamic_heap(), local_bitvector_analysist::flagst::is_dynamic_local(), irept::is_not_nil(), local_bitvector_analysist::flagst::is_null(), local_bitvector_analysist::flagst::is_static_lifetime(), local_bitvector_analysist::flagst::is_uninitialized(), local_bitvector_analysist::flagst::is_unknown(), local_bitvector_analysis, malloc_object(), ns, null_pointer(), object_lower_bound(), object_upper_bound(), exprt::op0(), pointer_type(), typet::subtype(), t, to_pointer_type(), and exprt::type().
Referenced by check_rec().
|
protected |
Definition at line 241 of file goto_check.cpp.
References add_guarded_claim(), shift_exprt::distance(), enable_undefined_shift_check, exprt::find_source_location(), namespace_baset::follow(), from_integer(), irept::id(), irept::id_string(), irept::is_nil(), ns, shift_exprt::op(), to_bitvector_type(), and exprt::type().
Referenced by check_rec().
|
protected |
Definition at line 146 of file goto_check.cpp.
Referenced by collect_allocations(), and pointer_validity_check().
|
protected |
Definition at line 114 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and invalidate().
|
protected |
Definition at line 136 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and goto_checkt().
|
protected |
Definition at line 137 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 139 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 123 of file goto_check.cpp.
Referenced by bounds_check(), and goto_checkt().
|
protected |
Definition at line 138 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 130 of file goto_check.cpp.
Referenced by conversion_check(), and goto_checkt().
|
protected |
Definition at line 126 of file goto_check.cpp.
Referenced by div_by_zero_check(), goto_checkt(), and mod_by_zero_check().
|
protected |
Definition at line 132 of file goto_check.cpp.
Referenced by float_overflow_check(), and goto_checkt().
|
protected |
Definition at line 125 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 134 of file goto_check.cpp.
Referenced by goto_checkt(), and nan_check().
|
protected |
Definition at line 124 of file goto_check.cpp.
Referenced by collect_allocations(), goto_check(), goto_checkt(), pointer_rel_check(), and pointer_validity_check().
|
protected |
Definition at line 129 of file goto_check.cpp.
Referenced by goto_checkt(), and pointer_overflow_check().
|
protected |
Definition at line 127 of file goto_check.cpp.
Referenced by goto_checkt(), and integer_overflow_check().
|
protected |
Definition at line 133 of file goto_check.cpp.
Referenced by add_guarded_claim(), and goto_checkt().
|
protected |
Definition at line 131 of file goto_check.cpp.
Referenced by goto_checkt(), and undefined_shift_check().
|
protected |
Definition at line 128 of file goto_check.cpp.
Referenced by goto_checkt(), and integer_overflow_check().
|
protected |
Definition at line 142 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 75 of file goto_check.cpp.
Referenced by goto_check(), and pointer_validity_check().
|
protected |
Definition at line 112 of file goto_check.cpp.
Referenced by add_guarded_claim(), and goto_check().
|
protected |
Definition at line 74 of file goto_check.cpp.
Referenced by add_guarded_claim(), array_name(), bounds_check(), check_rec(), conversion_check(), float_overflow_check(), goto_check(), integer_overflow_check(), pointer_validity_check(), and undefined_shift_check().
|
protected |
Definition at line 135 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and goto_checkt().
|
protected |
Definition at line 76 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and pointer_validity_check().