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) |
void | check (const exprt &expr) |
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) |
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) |
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 |
irep_idt | mode |
Definition at line 38 of file goto_check.cpp.
|
protected |
Definition at line 143 of file goto_check.cpp.
|
protected |
Definition at line 142 of file goto_check.cpp.
|
protected |
Definition at line 116 of file goto_check.cpp.
|
protected |
Definition at line 139 of file goto_check.cpp.
Definition at line 72 of file goto_check.cpp.
|
inline |
Definition at line 41 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 1262 of file goto_check.cpp.
References goto_programt::add_instruction(), guardt::as_expr(), ASSERT, assertions, ASSUME, comment(), enable_assert_to_assume, enable_simplify, get_language_from_mode(), exprt::is_true(), mode, 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 1081 of file goto_check.cpp.
References array_name(), and ns.
Referenced by bounds_check().
|
protected |
Definition at line 1086 of file goto_check.cpp.
References add_guarded_claim(), index_exprt::array(), array_name(), object_descriptor_exprt::build(), typecast_exprt::conditional_cast(), 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 1310 of file goto_check.cpp.
References guardt::add(), bounds_check(), conversion_check(), div_by_zero_check(), enable_pointer_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(), goto_programt::instructiont::code, CPROVER_PREFIX, enable_pointer_check, forall_goto_functions, forall_goto_program_instructions, code_function_callt::function(), irept::id(), goto_programt::instructiont::is_function_call(), to_code_function_call(), and to_symbol_expr().
Definition at line 339 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(), ns, exprt::op0(), exprt::operands(), power(), ieee_floatt::to_expr(), to_floatbv_type(), to_signedbv_type(), to_unsignedbv_type(), and exprt::type().
Referenced by check_rec().
Definition at line 214 of file goto_check.cpp.
References add_guarded_claim(), 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 632 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 1499 of file goto_check.cpp.
References add_guarded_claim(), goto_programt::add_instruction(), code_function_callt::arguments(), ASSERT, assertions, ASSIGN, ASSUME, base_type_eq(), goto_functiont::body, check(), goto_programt::clear(), goto_programt::instructiont::code, 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_functionst::entry_point(), error_labels, Forall_goto_program_instructions, forall_operands, goto_programt::instructiont::function, code_function_callt::function(), local_bitvector_analysist::get(), irept::get(), irept::get_bool(), source_locationt::get_property_class(), codet::get_statement(), goto_program, goto_programt::instructiont::guard, irept::id(), goto_programt::insert_before_swap(), goto_programt::instructions, invalidate(), goto_programt::instructiont::is_assert(), goto_programt::instructiont::is_assign(), goto_programt::instructiont::is_assume(), goto_programt::instructiont::is_dead(), goto_programt::instructiont::is_end_function(), goto_programt::instructiont::is_function_call(), local_bitvector_analysist::flagst::is_null(), goto_programt::instructiont::is_other(), goto_programt::instructiont::is_return(), goto_programt::instructiont::is_target(), goto_programt::instructiont::is_throw(), local_bitvector_analysist::flagst::is_unknown(), goto_programt::instructiont::labels, code_assignt::lhs(), local_bitvector_analysis, namespacet::lookup(), goto_programt::instructiont::make_skip(), exprt::make_typecast(), mode, new_code, ns, exprt::op0(), exprt::operands(), remove_skip(), retain_trivial, code_assignt::rhs(), source_locationt::set_function(), goto_programt::instructiont::source_location, 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().
Definition at line 511 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_subexpr(), 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 314 of file goto_check.cpp.
References add_guarded_claim(), 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 754 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(), exprt::type(), and UNREACHABLE.
Referenced by check_rec().
Definition at line 893 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 863 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 919 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(), mode, 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 239 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 144 of file goto_check.cpp.
Referenced by collect_allocations(), and pointer_validity_check().
|
protected |
Definition at line 117 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and invalidate().
|
protected |
Definition at line 134 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and goto_checkt().
|
protected |
Definition at line 135 of file goto_check.cpp.
Referenced by 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 121 of file goto_check.cpp.
Referenced by bounds_check(), and goto_checkt().
|
protected |
Definition at line 136 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 128 of file goto_check.cpp.
Referenced by conversion_check(), and goto_checkt().
|
protected |
Definition at line 124 of file goto_check.cpp.
Referenced by div_by_zero_check(), goto_checkt(), and mod_by_zero_check().
|
protected |
Definition at line 130 of file goto_check.cpp.
Referenced by float_overflow_check(), and goto_checkt().
|
protected |
Definition at line 123 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 132 of file goto_check.cpp.
Referenced by goto_checkt(), and nan_check().
|
protected |
Definition at line 122 of file goto_check.cpp.
Referenced by check_rec(), collect_allocations(), goto_check(), goto_checkt(), pointer_rel_check(), and pointer_validity_check().
|
protected |
Definition at line 127 of file goto_check.cpp.
Referenced by goto_checkt(), and pointer_overflow_check().
|
protected |
Definition at line 125 of file goto_check.cpp.
Referenced by goto_checkt(), and integer_overflow_check().
|
protected |
Definition at line 131 of file goto_check.cpp.
Referenced by add_guarded_claim(), and goto_checkt().
|
protected |
Definition at line 129 of file goto_check.cpp.
Referenced by goto_checkt(), and undefined_shift_check().
|
protected |
Definition at line 126 of file goto_check.cpp.
Referenced by goto_checkt(), and integer_overflow_check().
|
protected |
Definition at line 140 of file goto_check.cpp.
Referenced by goto_check(), and goto_checkt().
|
protected |
Definition at line 80 of file goto_check.cpp.
Referenced by goto_check(), and pointer_validity_check().
|
protected |
Definition at line 146 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and pointer_validity_check().
|
protected |
Definition at line 115 of file goto_check.cpp.
Referenced by add_guarded_claim(), and goto_check().
|
protected |
Definition at line 79 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 133 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and goto_checkt().
|
protected |
Definition at line 81 of file goto_check.cpp.
Referenced by add_guarded_claim(), goto_check(), and pointer_validity_check().