CBMC
|
This is the complete list of members for goto_check_ct, including all inherited members.
add_active_named_check_pragmas(source_locationt &source_location) const | goto_check_ct | protected |
add_all_checked_named_check_pragmas(source_locationt &source_location) const | goto_check_ct | protected |
add_guarded_property(const exprt &asserted_expr, const std::string &comment, const std::string &property_class, bool is_fatal, const source_locationt &source_location, const exprt &src_expr, const guardt &guard) | goto_check_ct | protected |
allocations | goto_check_ct | protected |
allocationst typedef | goto_check_ct | protected |
allocationt typedef | goto_check_ct | protected |
array_name(const exprt &) | goto_check_ct | protected |
assertions | goto_check_ct | protected |
assertionst typedef | goto_check_ct | protected |
bounds_check(const exprt &, const guardt &) | goto_check_ct | protected |
bounds_check_bit_count(const unary_exprt &, const guardt &) | goto_check_ct | protected |
bounds_check_index(const index_exprt &, const guardt &) | goto_check_ct | protected |
check(const exprt &expr) | goto_check_ct | protected |
check_rec(const exprt &expr, const guardt &guard) | goto_check_ct | protected |
check_rec_address(const exprt &expr, const guardt &guard) | goto_check_ct | protected |
check_rec_arithmetic_op(const exprt &expr, const guardt &guard) | goto_check_ct | protected |
check_rec_div(const div_exprt &div_expr, const guardt &guard) | goto_check_ct | protected |
check_rec_if(const if_exprt &if_expr, const guardt &guard) | goto_check_ct | protected |
check_rec_logical_op(const exprt &expr, const guardt &guard) | goto_check_ct | protected |
check_rec_member(const member_exprt &member, const guardt &guard) | goto_check_ct | protected |
check_shadow_memory_api_calls(const goto_programt::instructiont &) | goto_check_ct | protected |
check_statust enum name | goto_check_ct | protected |
CHECKED enum value | goto_check_ct | protected |
collect_allocations(const goto_functionst &goto_functions) | goto_check_ct | |
conditionst typedef | goto_check_ct | protected |
conversion_check(const exprt &, const guardt &) | goto_check_ct | protected |
current_target | goto_check_ct | protected |
DISABLE enum value | goto_check_ct | protected |
div_by_zero_check(const div_exprt &, const guardt &) | goto_check_ct | protected |
ENABLE enum value | goto_check_ct | protected |
enable_assert_to_assume | goto_check_ct | protected |
enable_bounds_check | goto_check_ct | protected |
enable_conversion_check | goto_check_ct | protected |
enable_div_by_zero_check | goto_check_ct | protected |
enable_enum_range_check | goto_check_ct | protected |
enable_float_div_by_zero_check | goto_check_ct | protected |
enable_float_overflow_check | goto_check_ct | protected |
enable_memory_cleanup_check | goto_check_ct | protected |
enable_memory_leak_check | goto_check_ct | protected |
enable_nan_check | goto_check_ct | protected |
enable_pointer_check | goto_check_ct | protected |
enable_pointer_overflow_check | goto_check_ct | protected |
enable_pointer_primitive_check | goto_check_ct | protected |
enable_signed_overflow_check | goto_check_ct | protected |
enable_simplify | goto_check_ct | protected |
enable_undefined_shift_check | goto_check_ct | protected |
enable_unsigned_overflow_check | goto_check_ct | protected |
enum_range_check(const exprt &, const guardt &) | goto_check_ct | protected |
error_labels | goto_check_ct | protected |
error_labelst typedef | goto_check_ct | protected |
float_div_by_zero_check(const div_exprt &, const guardt &) | goto_check_ct | protected |
float_overflow_check(const exprt &, const guardt &) | goto_check_ct | protected |
get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size) | goto_check_ct | protected |
get_pointer_is_null_condition(const exprt &address, const exprt &size) | goto_check_ct | protected |
get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size) | goto_check_ct | protected |
goto_check(const irep_idt &function_identifier, goto_functiont &goto_function) | goto_check_ct | |
goto_check_ct(const namespacet &_ns, const optionst &_options, message_handlert &_message_handler) | goto_check_ct | inline |
goto_functiont typedef | goto_check_ct | |
guardt typedef | goto_check_ct | protected |
identity | goto_check_ct | protected |
integer_overflow_check(const exprt &, const guardt &) | goto_check_ct | protected |
invalidate(const exprt &lhs) | goto_check_ct | protected |
is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size) | goto_check_ct | protected |
local_bitvector_analysis | goto_check_ct | protected |
log | goto_check_ct | protected |
match_named_check(const irep_idt &named_check) const | goto_check_ct | protected |
memory_leak_check(const irep_idt &function_id) | goto_check_ct | protected |
mod_by_zero_check(const mod_exprt &, const guardt &) | goto_check_ct | protected |
mod_overflow_check(const mod_exprt &, const guardt &) | goto_check_ct | protected |
mode | goto_check_ct | protected |
name_to_flag | goto_check_ct | protected |
named_check_statust typedef | goto_check_ct | protected |
nan_check(const exprt &, const guardt &) | goto_check_ct | protected |
new_code | goto_check_ct | protected |
ns | goto_check_ct | protected |
pointer_overflow_check(const exprt &, const guardt &) | goto_check_ct | protected |
pointer_primitive_check(const exprt &expr, const guardt &guard) | goto_check_ct | protected |
pointer_rel_check(const binary_exprt &, const guardt &) | goto_check_ct | protected |
pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard) | goto_check_ct | protected |
requires_pointer_primitive_check(const exprt &expr) | goto_check_ct | protected |
retain_trivial | goto_check_ct | protected |
undefined_shift_check(const shift_exprt &, const guardt &) | goto_check_ct | protected |