31 for(
const auto &target :
targets)
67 const auto skip_target =
106 annotated_location));
141 const auto skip_target =
147 const auto &target_type = car.
target().
type();
pointer_typet pointer_type(const typet &subtype)
Class that represents a normalized conditional address range, with:
const car_havoc_methodt havoc_method
Method to use to havod the target.
const exprt & target_size() const
Size of the target in bytes.
const symbol_exprt & upper_bound_var() const
Identifier of the upper address bound snapshot variable.
const symbol_exprt & valid_var() const
Identifier of the validity snapshot variable.
const exprt & target() const
The target expression.
const symbol_exprt & lower_bound_var() const
Identifier of the lower address bound snapshot variable.
Class that allows to clean expressions of side effects and to generate havoc_slice expressions.
void do_havoc_slice(const symbol_exprt &function, const exprt::operandst &arguments, goto_programt &dest, const irep_idt &mode)
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.
std::vector< exprt > operandst
typet & type()
Return the type of the expression.
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())
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
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_other(const goto_instruction_codet &_code, const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_goto(targett _target, 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.
void havoc_static_local(car_exprt car, goto_programt &dest)
Havoc a static local expression.
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 from DECL symbols to corresponding conditional address ranges.
cond_target_exprt_to_car_mapt from_spec_assigns
Map from conditional target expressions of assigns clauses to corresponding conditional address range...
symbol_table_baset & st
Program symbol table.
symbol_exprt_to_car_mapt from_static_local
Map to from detected or propagated static local symbols to corresponding conditional address ranges.
const irep_idt & mode
Language mode.
car_expr_listt from_heap_alloc
void track_static_locals(goto_programt &dest)
Searches the goto instructions reachable from the start to the end of the instrumented function's ins...
const namespacet ns
Program namespace.
const irep_idt & function_id
Name of the instrumented function.
message_handlert & get_message_handler()
A side_effect_exprt that returns a non-deterministically chosen value.
void set_comment(const irep_idt &comment)
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
irep_idt mode
Language mode.
static exprt conditional_cast(const exprt &expr, const typet &type)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Havoc function assigns clauses.
void add_pragma_disable_pointer_checks(source_locationt &location)
Adds a pragma on a source location disable all pointer checks.
void add_propagate_static_local_pragma(source_locationt &source_location)
Sets a pragma to mark assignments to static local variables that need to be propagated upwards in the...
Specify write set in function contracts.
API to expression classes for Pointers.
#define UNREACHABLE
This should be used to mark dead code.
side_effect_expr_function_callt & to_side_effect_expr_function_call(exprt &expr)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.