12 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
13 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_HAVOC_ASSIGNS_CLAUSE_TARGETS_H
59 const std::vector<exprt> &_targets,
Class that represents a normalized conditional address range, with:
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,...
void get_instructions(goto_programt &dest)
Generates the assigns clause replacement instructions in dest.
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)
const source_locationt & source_location
A class that generates instrumentation for assigns clause checking.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Specify write set in function contracts.