12 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
13 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
56 const std::vector<exprt> &_targets,
Class that represents a normalized conditional address range, with:
Stores information about a goto function computed from its CFG.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Class to generate havocking instructions for target expressions of a function contract's assign claus...
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,...
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)
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
A class that generates instrumentation for assigns clause checking.
The symbol table base class interface.
Specify write set in function contracts.