cprover
|
This is the complete list of members for instrument_spec_assignst, 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 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_fresh_symbol(const std::string &suffix, const typet &type, const source_locationt &location) const | 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 |
function_id | instrument_spec_assignst | protected |
functions | instrument_spec_assignst | protected |
inclusion_check_assertion(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt, goto_programt &dest) const | instrument_spec_assignst | protected |
inclusion_check_full(const car_exprt &lhs, bool allow_null_lhs, bool include_stack_allocated, optionalt< cfg_infot > &cfg_info_opt) const | instrument_spec_assignst | protected |
inclusion_check_single(const car_exprt &lhs, const car_exprt &candidate_car) const | instrument_spec_assignst | protected |
instrument_spec_assignst(const irep_idt &_function_id, const goto_functionst &_functions, symbol_tablet &_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 |
ns | 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 |