37 for(
const auto &target :
targets)
88 const auto &target_type =
car.target().type();
API to expression classes that are internal to the C frontend.
pointer_typet pointer_type(const typet &subtype)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Class that represents a normalized conditional address range, with:
Data structure for representing an arbitrary statement in a program.
Operator to dereference a pointer.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
static instructiont make_other(const codet &_code, const source_locationt &l=source_locationt::nil())
const std::vector< exprt > & targets
void havoc_if_valid(car_exprt car, goto_programt &dest)
Generates instructions to conditionally havoc the given conditional address range expression car,...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
const source_locationt & source_location
void track_spec_target(const exprt &expr, goto_programt &dest)
Track an assigns clause target and generate snaphsot instructions and well-definedness assertions in ...
symbol_exprt_to_car_mapt from_stack_alloc
Map to from DECL symbols to corresponding conditional address ranges.
cond_target_exprt_to_car_mapt from_spec_assigns
Map to from conditional target expressions of assigns clauses to corresponding conditional address ra...
exprt_to_car_mapt from_heap_alloc
Map to from malloc'd symbols to corresponding conditional address ranges.
void track_static_locals(goto_programt &dest)
Search the call graph reachable from the instrumented function to identify local static variables use...
const namespacet ns
Program namespace.
const irep_idt & function_id
Name of the instrumented function.
A side_effect_exprt that returns a non-deterministically chosen value.
static exprt conditional_cast(const exprt &expr, const typet &type)
Havoc function assigns clauses.
Specify write set in function contracts.
API to expression classes for Pointers.
Various predicates over pointers in programs.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
irep_idt make_assigns_clause_replacement_tracking_comment(const exprt &target, const irep_idt &function_id, const namespacet &ns)
Returns an irep_idt that essentially says that target was assigned by the contract of function_id.