CBMC
goto_check_ct Member List

This is the complete list of members for goto_check_ct, including all inherited members.

add_active_named_check_pragmas(source_locationt &source_location) constgoto_check_ctprotected
add_all_checked_named_check_pragmas(source_locationt &source_location) constgoto_check_ctprotected
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_ctprotected
allocationsgoto_check_ctprotected
allocationst typedefgoto_check_ctprotected
allocationt typedefgoto_check_ctprotected
array_name(const exprt &)goto_check_ctprotected
assertionsgoto_check_ctprotected
assertionst typedefgoto_check_ctprotected
bounds_check(const exprt &, const guardt &)goto_check_ctprotected
bounds_check_bit_count(const unary_exprt &, const guardt &)goto_check_ctprotected
bounds_check_index(const index_exprt &, const guardt &)goto_check_ctprotected
check(const exprt &expr)goto_check_ctprotected
check_rec(const exprt &expr, const guardt &guard)goto_check_ctprotected
check_rec_address(const exprt &expr, const guardt &guard)goto_check_ctprotected
check_rec_arithmetic_op(const exprt &expr, const guardt &guard)goto_check_ctprotected
check_rec_div(const div_exprt &div_expr, const guardt &guard)goto_check_ctprotected
check_rec_if(const if_exprt &if_expr, const guardt &guard)goto_check_ctprotected
check_rec_logical_op(const exprt &expr, const guardt &guard)goto_check_ctprotected
check_rec_member(const member_exprt &member, const guardt &guard)goto_check_ctprotected
check_shadow_memory_api_calls(const goto_programt::instructiont &)goto_check_ctprotected
check_statust enum namegoto_check_ctprotected
CHECKED enum valuegoto_check_ctprotected
collect_allocations(const goto_functionst &goto_functions)goto_check_ct
conditionst typedefgoto_check_ctprotected
conversion_check(const exprt &, const guardt &)goto_check_ctprotected
current_targetgoto_check_ctprotected
DISABLE enum valuegoto_check_ctprotected
div_by_zero_check(const div_exprt &, const guardt &)goto_check_ctprotected
ENABLE enum valuegoto_check_ctprotected
enable_assert_to_assumegoto_check_ctprotected
enable_bounds_checkgoto_check_ctprotected
enable_conversion_checkgoto_check_ctprotected
enable_div_by_zero_checkgoto_check_ctprotected
enable_enum_range_checkgoto_check_ctprotected
enable_float_div_by_zero_checkgoto_check_ctprotected
enable_float_overflow_checkgoto_check_ctprotected
enable_memory_cleanup_checkgoto_check_ctprotected
enable_memory_leak_checkgoto_check_ctprotected
enable_nan_checkgoto_check_ctprotected
enable_pointer_checkgoto_check_ctprotected
enable_pointer_overflow_checkgoto_check_ctprotected
enable_pointer_primitive_checkgoto_check_ctprotected
enable_signed_overflow_checkgoto_check_ctprotected
enable_simplifygoto_check_ctprotected
enable_undefined_shift_checkgoto_check_ctprotected
enable_unsigned_overflow_checkgoto_check_ctprotected
enum_range_check(const exprt &, const guardt &)goto_check_ctprotected
error_labelsgoto_check_ctprotected
error_labelst typedefgoto_check_ctprotected
float_div_by_zero_check(const div_exprt &, const guardt &)goto_check_ctprotected
float_overflow_check(const exprt &, const guardt &)goto_check_ctprotected
get_pointer_dereferenceable_conditions(const exprt &address, const exprt &size)goto_check_ctprotected
get_pointer_is_null_condition(const exprt &address, const exprt &size)goto_check_ctprotected
get_pointer_points_to_valid_memory_conditions(const exprt &address, const exprt &size)goto_check_ctprotected
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_ctinline
goto_functiont typedefgoto_check_ct
guardt typedefgoto_check_ctprotected
identitygoto_check_ctprotected
integer_overflow_check(const exprt &, const guardt &)goto_check_ctprotected
invalidate(const exprt &lhs)goto_check_ctprotected
is_in_bounds_of_some_explicit_allocation(const exprt &pointer, const exprt &size)goto_check_ctprotected
local_bitvector_analysisgoto_check_ctprotected
loggoto_check_ctprotected
match_named_check(const irep_idt &named_check) constgoto_check_ctprotected
memory_leak_check(const irep_idt &function_id)goto_check_ctprotected
mod_by_zero_check(const mod_exprt &, const guardt &)goto_check_ctprotected
mod_overflow_check(const mod_exprt &, const guardt &)goto_check_ctprotected
modegoto_check_ctprotected
name_to_flaggoto_check_ctprotected
named_check_statust typedefgoto_check_ctprotected
nan_check(const exprt &, const guardt &)goto_check_ctprotected
new_codegoto_check_ctprotected
nsgoto_check_ctprotected
pointer_overflow_check(const exprt &, const guardt &)goto_check_ctprotected
pointer_primitive_check(const exprt &expr, const guardt &guard)goto_check_ctprotected
pointer_rel_check(const binary_exprt &, const guardt &)goto_check_ctprotected
pointer_validity_check(const dereference_exprt &expr, const exprt &src_expr, const guardt &guard)goto_check_ctprotected
requires_pointer_primitive_check(const exprt &expr)goto_check_ctprotected
retain_trivialgoto_check_ctprotected
undefined_shift_check(const shift_exprt &, const guardt &)goto_check_ctprotected