CBMC
|
This is the complete list of members for instrument_spec_assignst, including all inherited members.
car_expr_listt typedef | instrument_spec_assignst | protected |
cfg_info | instrument_spec_assignst | protected |
check_inclusion_assignment(const exprt &lhs, goto_programt &dest) const | instrument_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_assignst | protected |
cond_target_exprt_to_car_mapt typedef | instrument_spec_assignst | protected |
covered_locationst typedef | instrument_spec_assignst | protected |
create_car_expr(const exprt &condition, const exprt &target) const | instrument_spec_assignst | protected |
create_car_from_heap_alloc(const exprt &target) | instrument_spec_assignst | protected |
create_car_from_spec_assigns(const exprt &condition, const exprt &target) | instrument_spec_assignst | protected |
create_car_from_stack_alloc(const symbol_exprt &target) | instrument_spec_assignst | protected |
create_car_from_static_local(const symbol_exprt &target) | instrument_spec_assignst | protected |
create_snapshot(const car_exprt &car, goto_programt &dest) const | instrument_spec_assignst | protected |
exprt_to_car_mapt typedef | instrument_spec_assignst | protected |
from_heap_alloc | instrument_spec_assignst | protected |
from_spec_assigns | instrument_spec_assignst | protected |
from_stack_alloc | instrument_spec_assignst | protected |
from_static_local | instrument_spec_assignst | protected |
function_id | instrument_spec_assignst | protected |
functions | instrument_spec_assignst | protected |
get_static_locals(std::insert_iterator< C > inserter) const | instrument_spec_assignst | inline |
inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, goto_programt &dest) const | instrument_spec_assignst | protected |
inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated) const | instrument_spec_assignst | protected |
inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) const | instrument_spec_assignst | protected |
instrument_assign_statement(goto_programt::targett &instruction_it, goto_programt &body) const | instrument_spec_assignst | protected |
instrument_call_statement(goto_programt::targett &instruction_it, goto_programt &body) | instrument_spec_assignst | protected |
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_assignst | inline |
invalidate_car(const car_exprt &tracked_car, const car_exprt &freed_car, goto_programt &result) const | instrument_spec_assignst | protected |
invalidate_heap_and_spec_aliases(const car_exprt &freed_car, goto_programt &dest) const | instrument_spec_assignst | protected |
invalidate_stack_allocated(const symbol_exprt &symbol_expr, goto_programt &dest) | instrument_spec_assignst | |
log | instrument_spec_assignst | protected |
mode | instrument_spec_assignst | protected |
must_check_assign(const goto_programt::const_targett &target) | instrument_spec_assignst | protected |
must_track_dead(const goto_programt::const_targett &target) const | instrument_spec_assignst | protected |
must_track_decl(const goto_programt::const_targett &target) const | instrument_spec_assignst | protected |
must_track_decl_or_dead(const irep_idt &ident) const | instrument_spec_assignst | protected |
ns | instrument_spec_assignst | protected |
propagated_static_localst typedef | instrument_spec_assignst | protected |
st | instrument_spec_assignst | protected |
stack_allocated_is_tracked(const symbol_exprt &symbol_expr) const | instrument_spec_assignst | |
symbol_exprt_to_car_mapt typedef | instrument_spec_assignst | protected |
target_validity_assertion(const car_exprt &car, bool allow_null_target, goto_programt &dest) const | instrument_spec_assignst | protected |
target_validity_expr(const car_exprt &car, bool allow_null_target) const | instrument_spec_assignst | protected |
track_heap_allocated(const exprt &expr, goto_programt &dest) | instrument_spec_assignst | |
track_plain_spec_target(const exprt &expr, goto_programt &dest) | instrument_spec_assignst | protected |
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_assignst | protected |
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) const | instrument_spec_assignst | protected |