|
void | check_rec (const exprt &expr, guardt &guard, bool address) |
|
void | check (const exprt &expr) |
|
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 | undefined_shift_check (const shift_exprt &, const guardt &) |
|
void | pointer_rel_check (const exprt &, const guardt &) |
|
void | pointer_overflow_check (const exprt &, const guardt &) |
|
void | pointer_validity_check (const dereference_exprt &, const guardt &) |
|
conditionst | address_check (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 &) |
|
void | rw_ok_check (exprt &) |
| expand the r_ok and w_ok predicates More...
|
|
std::string | array_name (const exprt &) |
|
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) |
|
Definition at line 40 of file goto_check.cpp.
◆ allocationst
◆ allocationt
◆ assertionst
◆ conditionst
◆ error_labelst
◆ goto_functiont
◆ goto_checkt()
◆ add_guarded_claim()
void goto_checkt::add_guarded_claim |
( |
const exprt & |
expr, |
|
|
const std::string & |
comment, |
|
|
const std::string & |
property_class, |
|
|
const source_locationt & |
source_location, |
|
|
const exprt & |
src_expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ address_check()
◆ array_name()
std::string goto_checkt::array_name |
( |
const exprt & |
expr | ) |
|
|
protected |
◆ bounds_check()
◆ check()
void goto_checkt::check |
( |
const exprt & |
expr | ) |
|
|
protected |
◆ check_rec()
void goto_checkt::check_rec |
( |
const exprt & |
expr, |
|
|
guardt & |
guard, |
|
|
bool |
address |
|
) |
| |
|
protected |
◆ collect_allocations()
void goto_checkt::collect_allocations |
( |
const goto_functionst & |
goto_functions | ) |
|
◆ conversion_check()
void goto_checkt::conversion_check |
( |
const exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ div_by_zero_check()
void goto_checkt::div_by_zero_check |
( |
const div_exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ float_overflow_check()
void goto_checkt::float_overflow_check |
( |
const exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ goto_check()
◆ integer_overflow_check()
void goto_checkt::integer_overflow_check |
( |
const exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ invalidate()
void goto_checkt::invalidate |
( |
const exprt & |
lhs | ) |
|
|
protected |
◆ mod_by_zero_check()
void goto_checkt::mod_by_zero_check |
( |
const mod_exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ nan_check()
void goto_checkt::nan_check |
( |
const exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ pointer_overflow_check()
void goto_checkt::pointer_overflow_check |
( |
const exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ pointer_rel_check()
void goto_checkt::pointer_rel_check |
( |
const exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ pointer_validity_check()
◆ rw_ok_check()
void goto_checkt::rw_ok_check |
( |
exprt & |
expr | ) |
|
|
protected |
◆ undefined_shift_check()
void goto_checkt::undefined_shift_check |
( |
const shift_exprt & |
expr, |
|
|
const guardt & |
guard |
|
) |
| |
|
protected |
◆ allocations
◆ assertions
◆ current_target
◆ enable_assert_to_assume
bool goto_checkt::enable_assert_to_assume |
|
protected |
◆ enable_assertions
bool goto_checkt::enable_assertions |
|
protected |
◆ enable_assumptions
bool goto_checkt::enable_assumptions |
|
protected |
◆ enable_bounds_check
bool goto_checkt::enable_bounds_check |
|
protected |
◆ enable_built_in_assertions
bool goto_checkt::enable_built_in_assertions |
|
protected |
◆ enable_conversion_check
bool goto_checkt::enable_conversion_check |
|
protected |
◆ enable_div_by_zero_check
bool goto_checkt::enable_div_by_zero_check |
|
protected |
◆ enable_float_overflow_check
bool goto_checkt::enable_float_overflow_check |
|
protected |
◆ enable_memory_leak_check
bool goto_checkt::enable_memory_leak_check |
|
protected |
◆ enable_nan_check
bool goto_checkt::enable_nan_check |
|
protected |
◆ enable_pointer_check
bool goto_checkt::enable_pointer_check |
|
protected |
◆ enable_pointer_overflow_check
bool goto_checkt::enable_pointer_overflow_check |
|
protected |
◆ enable_signed_overflow_check
bool goto_checkt::enable_signed_overflow_check |
|
protected |
◆ enable_simplify
bool goto_checkt::enable_simplify |
|
protected |
◆ enable_undefined_shift_check
bool goto_checkt::enable_undefined_shift_check |
|
protected |
◆ enable_unsigned_overflow_check
bool goto_checkt::enable_unsigned_overflow_check |
|
protected |
◆ error_labels
◆ local_bitvector_analysis
◆ mode
◆ new_code
◆ ns
◆ retain_trivial
bool goto_checkt::retain_trivial |
|
protected |
The documentation for this class was generated from the following file: