73 assert(!loop.empty());
77 for(loopt::const_iterator
81 if((*it)->is_goto() &&
82 (*it)->get_target()==loop_head &&
83 (*it)->location_number>loop_end->location_number)
88 static_cast<const exprt&>(
89 loop_end->guard.find(ID_C_spec_loop_invariant));
115 a->function=loop_head->function;
117 a->source_location.
set_comment(
"Loop invariant violated before entry");
126 assume->guard=invariant;
127 assume->function=loop_head->function;
132 if(!loop_head->is_goto())
137 jump->targets.push_back(loop_end);
138 jump->function=loop_head->function;
143 goto_function.body.insert_before_swap(loop_head, havoc_code);
152 goto_function.body.insert_before_swap(loop_end, a);
157 loop_end->targets.clear();
159 if(loop_head->is_goto())
180 static_cast<const exprt&>(type.
find(ID_C_spec_requires));
182 static_cast<const exprt&>(type.
find(ID_C_spec_ensures));
199 code_function_callt::argumentst::const_iterator a_it=
201 for(code_typet::parameterst::const_iterator
206 if(!p_it->get_identifier().empty())
226 target->make_assumption(ensures);
238 for(natural_loops_mutablet::loop_mapt::const_iterator
239 l_it=natural_loops.
loop_map.begin();
250 if(it->is_function_call())
273 goto_functionst::function_mapt::iterator f_it=
279 const exprt &requires=
280 static_cast<const exprt&>(gf.type.find(ID_C_spec_requires));
281 const exprt &ensures=
282 static_cast<const exprt&>(gf.type.find(ID_C_spec_ensures));
283 assert(ensures.is_not_nil());
299 skip->source_location=ensures.source_location();
307 g->function=skip->function;
308 g->source_location=skip->source_location;
318 d->function=skip->function;
319 d->source_location=skip->source_location;
323 d->source_location).symbol_expr();
333 for(code_typet::parameterst::const_iterator
334 p_it=gf.type.parameters().begin();
335 p_it!=gf.type.parameters().end();
339 d->function=skip->function;
340 d->source_location=skip->source_location;
344 d->source_location).symbol_expr();
347 call.arguments().push_back(p);
349 if(!p_it->get_identifier().empty())
351 symbol_exprt cur_p(p_it->get_identifier(), p_it->type());
360 a->make_assumption(requires);
361 a->function=skip->function;
370 f->make_function_call(call);
371 f->function=skip->function;
372 f->source_location=skip->source_location;
376 a->make_assertion(ensures);
377 a->function=skip->function;
378 a->source_location=ensures.source_location();
386 af->function=skip->function;
387 af->source_location=ensures.source_location();
399 goto_functionst::function_mapt::iterator i_it=
exprt guard
Guard for gotos, assume, assert.
irep_idt function
The function this instruction belongs to.
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
goto_functionst & goto_functions
void add_contract_check(const irep_idt &function, goto_programt &dest)
Deprecated expression utility functions.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
void set_comment(const irep_idt &comment)
const irep_idt & get_function() const
std::unordered_set< irep_idt > summarized
Fresh auxiliary symbol creation.
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
const natural_loops_mutablet::natural_loopt loopt
function_mapt function_map
typet & type()
Return the type of the expression.
symbol_tablet symbol_table
Symbol table.
symbol_tablet & symbol_table
This class represents an instruction in the GOTO intermediate representation.
void code_contracts(goto_functionst::goto_functiont &goto_function)
const irep_idt & id() const
instructionst::iterator targett
Replace expression or type symbols by an expression or type, respectively.
A codet representing the declaration of a local variable.
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
#define INITIALIZE_FUNCTION
instructionst instructions
The list of instructions in the goto program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
::goto_functiont goto_functiont
std::set< exprt > modifiest
A side_effect_exprt that returns a non-deterministically chosen value.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
codet representation of a function call statement.
A collection of goto functions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Helper functions for k-induction and loop invariants.
The Boolean constant false.
const source_locationt & source_location() const
A generic container class for the GOTO intermediate representation of one function.
Verify and use annotated invariants and pre/post-conditions.
typet type
Type of symbol.
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
source_locationt source_location
The location of the instruction in the source file.
targett add_instruction()
Adds an instruction at the end.
Base class for all expressions.
const parameterst & parameters() const
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
unsigned temporary_counter
#define Forall_goto_program_instructions(it, program)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
Expression to hold a symbol (variable)
void code_contracts(goto_modelt &goto_model)
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
const irept & find(const irep_namet &name) const
goto_functionst goto_functions
GOTO functions.
const typet & return_type() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
const symbolt & new_tmp_symbol(const typet &type, const source_locationt &source_location)
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)
Field-insensitive, location-sensitive may-alias analysis.
const code_function_callt & to_code_function_call(const codet &code)