Go to the documentation of this file.
75 assert(!loop.
empty());
83 if((*it)->is_goto() &&
84 (*it)->get_target()==loop_head &&
85 (*it)->location_number>loop_end->location_number)
90 loop_end->get_condition().find(ID_C_spec_loop_invariant));
116 a->source_location.set_comment(
"Loop invariant violated before entry");
127 if(!loop_head->is_goto())
136 goto_function.body.insert_before_swap(loop_head, havoc_code);
143 goto_function.body.insert_before_swap(loop_end, a);
148 loop_end->targets.clear();
150 if(loop_head->is_goto())
153 loop_end->set_condition(
boolean_negate(loop_end->get_condition()));
172 static_cast<const exprt&
>(type.
find(ID_C_spec_requires));
174 static_cast<const exprt&
>(type.
find(ID_C_spec_ensures));
191 code_function_callt::argumentst::const_iterator a_it=
193 for(code_typet::parameterst::const_iterator
198 if(!p_it->get_identifier().empty())
229 for(natural_loops_mutablet::loop_mapt::const_iterator
230 l_it=natural_loops.
loop_map.begin();
241 if(it->is_function_call())
266 goto_functionst::function_mapt::iterator f_it=
272 const exprt &requires=
273 static_cast<const exprt&
>(gf.type.find(ID_C_spec_requires));
274 const exprt &ensures=
275 static_cast<const exprt&
>(gf.type.find(ID_C_spec_ensures));
310 gf.type.return_type(),
311 skip->source_location,
313 function_symbol.
mode)
324 for(
const auto ¶meter : gf.parameter_identifiers)
330 parameter_symbol.
type,
333 parameter_symbol.
mode)
346 exprt requires_cond = requires;
357 exprt ensures_cond = ensures;
378 goto_functionst::function_mapt::iterator i_it=
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void code_contracts(goto_functionst::goto_functiont &goto_function)
source_locationt source_location
The location of the instruction in the source file.
void set_comment(const irep_idt &comment)
The type of an expression, extends irept.
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
const irept & find(const irep_namet &name) const
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
targett add(instructiont &&instruction)
Adds a given instruction at the end.
const_iterator end() const
Iterator over this loop's instructions.
Base class for all expressions.
function_mapt function_map
Expression to hold a symbol (variable)
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static void check_apply_invariants(goto_functionst::goto_functiont &goto_function, const local_may_aliast &local_may_alias, const goto_programt::targett loop_head, const loopt &loop)
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const_iterator begin() const
Iterator over this loop's instructions.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
std::set< exprt > modifiest
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
irep_idt mode
Language mode.
loop_instructionst::const_iterator const_iterator
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const std::string & id2string(const irep_idt &d)
unsigned temporary_counter
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
#define PRECONDITION(CONDITION)
const source_locationt & source_location() const
const irep_idt & get_identifier() const
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
#define INITIALIZE_FUNCTION
A loop, specified as a set of instructions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
void add_contract_check(const irep_idt &function, goto_programt &dest)
const irep_idt & id() const
The Boolean constant false.
void code_contracts(goto_modelt &goto_model)
const parameterst & parameters() const
#define Forall_goto_functions(it, functions)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
A side_effect_exprt that returns a non-deterministically chosen value.
::goto_functiont goto_functiont
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location, const irep_idt &function_id, const irep_idt &mode)
instructionst instructions
The list of instructions in the goto program.
Deprecated expression utility functions.
A collection of goto functions.
goto_functionst & goto_functions
goto_functionst goto_functions
GOTO functions.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
A generic container class for the GOTO intermediate representation of one function.
std::unordered_set< irep_idt > summarized
bool empty() const
Returns true if this loop contains no instructions.
const typet & return_type() const
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
This class represents an instruction in the GOTO intermediate representation.
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
instructionst::iterator targett
symbol_tablet & symbol_table
Replace expression or type symbols by an expression or type, respectively.