cprover
Loading...
Searching...
No Matches
havoc_assigns_clause_targetst Member List

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

check_inclusion_assignment(const exprt &lhs, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)instrument_spec_assignst
check_inclusion_heap_allocated_and_invalidate_aliases(const exprt &expr, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest)instrument_spec_assignst
cond_target_exprt_to_car_mapt 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_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location) constinstrument_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
function_idinstrument_spec_assignstprotected
functionsinstrument_spec_assignstprotected
get_instructions(goto_programt &dest)havoc_assigns_clause_targetst
havoc_assigns_clause_targetst(const irep_idt &_function_id, const std::vector< exprt > &_targets, const goto_functionst &_functions, const source_locationt &_source_location, symbol_tablet &_st, message_handlert &_message_handler)havoc_assigns_clause_targetstinline
havoc_if_valid(car_exprt car, goto_programt &dest)havoc_assigns_clause_targetstprivate
inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) constinstrument_spec_assignstprotected
inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt) constinstrument_spec_assignstprotected
inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) constinstrument_spec_assignstprotected
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, symbol_tablet &_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
nsinstrument_spec_assignstprotected
source_locationhavoc_assigns_clause_targetstprivate
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
targetshavoc_assigns_clause_targetstprivate
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