CBMC
instrument_spec_assignst Member List

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

car_expr_listt typedefinstrument_spec_assignstprotected
cfg_infoinstrument_spec_assignstprotected
check_inclusion_assignment(const exprt &lhs, goto_programt &dest) constinstrument_spec_assignst
check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, goto_programt &dest)instrument_spec_assignst
collect_static_symbols(covered_locationst &covered_locations, std::unordered_set< symbol_exprt, irep_hash > &dest)instrument_spec_assignstprotected
cond_target_exprt_to_car_mapt typedefinstrument_spec_assignstprotected
covered_locationst typedefinstrument_spec_assignstprotected
create_car_expr(const exprt &condition, const exprt &target) constinstrument_spec_assignstprotected
create_car_from_heap_alloc(const exprt &target)instrument_spec_assignstprotected
create_car_from_spec_assigns(const exprt &condition, const exprt &target)instrument_spec_assignstprotected
create_car_from_stack_alloc(const symbol_exprt &target)instrument_spec_assignstprotected
create_car_from_static_local(const symbol_exprt &target)instrument_spec_assignstprotected
create_snapshot(const car_exprt &car, goto_programt &dest) constinstrument_spec_assignstprotected
exprt_to_car_mapt typedefinstrument_spec_assignstprotected
from_heap_allocinstrument_spec_assignstprotected
from_spec_assignsinstrument_spec_assignstprotected
from_stack_allocinstrument_spec_assignstprotected
from_static_localinstrument_spec_assignstprotected
function_idinstrument_spec_assignstprotected
functionsinstrument_spec_assignstprotected
get_static_locals(std::insert_iterator< C > inserter) constinstrument_spec_assignstinline
inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, goto_programt &dest) constinstrument_spec_assignstprotected
inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated) constinstrument_spec_assignstprotected
inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) constinstrument_spec_assignstprotected
instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &body) constinstrument_spec_assignstprotected
instrument_call_statement(goto_programt::targett &instruction_it, goto_programt &body)instrument_spec_assignstprotected
instrument_instructions(goto_programt &body, goto_programt::targett instruction_it, const goto_programt::targett &instruction_end, const std::function< bool(const goto_programt::targett &)> &pred={})instrument_spec_assignst
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, cfg_infot &_cfg_info, symbol_table_baset &_st, message_handlert &_message_handler)instrument_spec_assignstinline
invalidate_car(const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) constinstrument_spec_assignstprotected
invalidate_heap_and_spec_aliases(const car_exprt &freed_car, goto_programt &dest) constinstrument_spec_assignstprotected
invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)instrument_spec_assignst
loginstrument_spec_assignstprotected
modeinstrument_spec_assignstprotected
must_check_assign(const goto_programt::const_targett &target)instrument_spec_assignstprotected
must_track_dead(const goto_programt::const_targett &target) constinstrument_spec_assignstprotected
must_track_decl(const goto_programt::const_targett &target) constinstrument_spec_assignstprotected
must_track_decl_or_dead(const irep_idt &ident) constinstrument_spec_assignstprotected
nsinstrument_spec_assignstprotected
propagated_static_localst typedefinstrument_spec_assignstprotected
stinstrument_spec_assignstprotected
stack_allocated_is_tracked(const symbol_exprt &symbol_expr) constinstrument_spec_assignst
symbol_exprt_to_car_mapt typedefinstrument_spec_assignstprotected
target_validity_assertion(const car_exprt &car, bool allow_null_target, goto_programt &dest) constinstrument_spec_assignstprotected
target_validity_expr(const car_exprt &car, bool allow_null_target) constinstrument_spec_assignstprotected
track_heap_allocated(const exprt &expr, goto_programt &dest)instrument_spec_assignst
track_plain_spec_target(const exprt &expr, goto_programt &dest)instrument_spec_assignstprotected
track_spec_target(const exprt &expr, goto_programt &dest)instrument_spec_assignst
track_spec_target_group(const conditional_target_group_exprt &group, goto_programt &dest)instrument_spec_assignstprotected
track_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest)instrument_spec_assignst
track_static_locals(goto_programt &dest)instrument_spec_assignst
track_static_locals_between(goto_programt::const_targett it, const goto_programt::const_targett end, goto_programt &dest)instrument_spec_assignst
traverse_instructions(const irep_idt ambient_function_id, goto_programt::const_targett it, const goto_programt::const_targett end, covered_locationst &covered_locations, propagated_static_localst &propagated) constinstrument_spec_assignstprotected