|
cprover
|
This is the complete list of members for goto_checkt, including all inherited members.
| 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) | goto_checkt | protected |
| allocations | goto_checkt | protected |
| allocationst typedef | goto_checkt | protected |
| allocationt typedef | goto_checkt | protected |
| array_name(const exprt &expr) | goto_checkt | protected |
| assertions | goto_checkt | protected |
| assertionst typedef | goto_checkt | protected |
| bounds_check(const index_exprt &expr, const guardt &guard) | goto_checkt | protected |
| check(const exprt &expr, const irep_idt &mode) | goto_checkt | protected |
| check_rec(const exprt &expr, guardt &guard, bool address, const irep_idt &mode) | goto_checkt | protected |
| collect_allocations(const goto_functionst &goto_functions) | goto_checkt | |
| conversion_check(const exprt &expr, const guardt &guard) | goto_checkt | protected |
| div_by_zero_check(const div_exprt &expr, const guardt &guard) | goto_checkt | protected |
| enable_assert_to_assume | goto_checkt | protected |
| enable_assertions | goto_checkt | protected |
| enable_assumptions | goto_checkt | protected |
| enable_bounds_check | goto_checkt | protected |
| enable_built_in_assertions | goto_checkt | protected |
| enable_conversion_check | goto_checkt | protected |
| enable_div_by_zero_check | goto_checkt | protected |
| enable_float_overflow_check | goto_checkt | protected |
| enable_memory_leak_check | goto_checkt | protected |
| enable_nan_check | goto_checkt | protected |
| enable_pointer_check | goto_checkt | protected |
| enable_pointer_overflow_check | goto_checkt | protected |
| enable_signed_overflow_check | goto_checkt | protected |
| enable_simplify | goto_checkt | protected |
| enable_undefined_shift_check | goto_checkt | protected |
| enable_unsigned_overflow_check | goto_checkt | protected |
| error_labels | goto_checkt | protected |
| error_labelst typedef | goto_checkt | protected |
| float_overflow_check(const exprt &expr, const guardt &guard) | goto_checkt | protected |
| goto_check(goto_functiont &goto_function, const irep_idt &mode) | goto_checkt | |
| goto_checkt(const namespacet &_ns, const optionst &_options) | goto_checkt | inline |
| goto_functiont typedef | goto_checkt | |
| has_dereference(const exprt &src) | goto_checkt | inlineprotectedstatic |
| integer_overflow_check(const exprt &expr, const guardt &guard) | goto_checkt | protected |
| invalidate(const exprt &lhs) | goto_checkt | protected |
| local_bitvector_analysis | goto_checkt | protected |
| mod_by_zero_check(const mod_exprt &expr, const guardt &guard) | goto_checkt | protected |
| nan_check(const exprt &expr, const guardt &guard) | goto_checkt | protected |
| new_code | goto_checkt | protected |
| ns | goto_checkt | protected |
| pointer_overflow_check(const exprt &expr, const guardt &guard) | goto_checkt | protected |
| pointer_rel_check(const exprt &expr, const guardt &guard) | goto_checkt | protected |
| pointer_validity_check(const dereference_exprt &expr, const guardt &guard, const exprt &access_lb, const exprt &access_ub, const irep_idt &mode) | goto_checkt | protected |
| retain_trivial | goto_checkt | protected |
| t | goto_checkt | protected |
| undefined_shift_check(const shift_exprt &expr, const guardt &guard) | goto_checkt | protected |