havoc_assigns_clause_targetst Member List

This is the complete list of members for havoc_assigns_clause_targetst, 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_instructions(goto_programt &dest)	havoc_assigns_clause_targetst
get_static_locals(std::insert_iterator< C > inserter) const	instrument_spec_assignst	inline
havoc_assigns_clause_targetst(const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, cfg_infot &_cfg_info, const source_locationt &_source_location, symbol_table_baset &_st, message_handlert &_message_handler)	havoc_assigns_clause_targetst	inline
havoc_if_valid(car_exprt car, goto_programt &dest)	havoc_assigns_clause_targetst	private
havoc_static_local(car_exprt car, goto_programt &dest)	havoc_assigns_clause_targetst	private
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
source_location	havoc_assigns_clause_targetst	private
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
targets	havoc_assigns_clause_targetst	private
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