48 typedef std::unordered_set<irep_idt, irep_id_hash>
id_sett;
72 assert(!loop.empty());
76 for(loopt::const_iterator
80 if((*it)->is_goto() &&
81 (*it)->get_target()==loop_head &&
82 (*it)->location_number>loop_end->location_number)
87 static_cast<const exprt&
>(
88 loop_end->guard.find(ID_C_spec_loop_invariant));
114 a->function=loop_head->function;
116 a->source_location.
set_comment(
"Loop invariant violated before entry");
125 assume->guard=invariant;
126 assume->function=loop_head->function;
131 if(!loop_head->is_goto())
135 jump->targets.push_back(loop_end);
136 jump->function=loop_head->function;
137 jump->source_location=loop_head->source_location;
142 goto_function.body.insert_before_swap(loop_head, havoc_code);
146 goto_programt::instructiont a(
ASSERT);
148 a.function=loop_end->function;
150 a.source_location.
set_comment(
"Loop invariant not preserved");
151 goto_function.body.insert_before_swap(loop_end, a);
156 loop_end->targets.clear();
158 if(loop_head->is_goto())
159 loop_end->guard.make_false();
161 loop_end->guard.make_not();
179 static_cast<const exprt&
>(type.
find(ID_C_spec_requires));
181 static_cast<const exprt&
>(type.
find(ID_C_spec_ensures));
192 replace.
insert(
"__CPROVER_return_value", call.
lhs());
195 code_function_callt::argumentst::const_iterator a_it=
197 for(code_typet::parameterst::const_iterator
202 if(!p_it->get_identifier().empty())
203 replace.
insert(p_it->get_identifier(), *a_it);
210 goto_programt::instructiont a(
ASSERT);
212 a.function=target->function;
219 target->make_assumption(ensures);
231 for(natural_loops_mutablet::loop_mapt::const_iterator
232 l_it=natural_loops.
loop_map.begin();
243 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));
299 g->function=skip->function;
300 g->source_location=skip->source_location;
311 d->function=skip->function;
312 d->source_location=skip->source_location;
316 d->source_location).symbol_expr();
321 replace.
insert(
"__CPROVER_return_value",
r);
325 for(code_typet::parameterst::const_iterator
326 p_it=gf.type.parameters().begin();
327 p_it!=gf.type.parameters().end();
331 d->function=skip->function;
332 d->source_location=skip->source_location;
336 d->source_location).symbol_expr();
341 if(!p_it->get_identifier().empty())
342 replace.
insert(p_it->get_identifier(), p);
349 a->make_assumption(requires);
350 a->function=skip->function;
359 f->make_function_call(call);
360 f->function=skip->function;
361 f->source_location=skip->source_location;
365 a->make_assertion(ensures);
366 a->function=skip->function;
375 af->function=skip->function;
388 goto_functionst::function_mapt::iterator i_it=
392 for(id_sett::const_iterator it=
summarized.begin();
The type of an expression.
std::unordered_set< irep_idt, irep_id_hash > id_sett
virtual bool lookup(const irep_idt &name, const symbolt *&symbol) const
targett add_instruction()
Adds an instruction at the end.
goto_functionst & goto_functions
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
void add_contract_check(const irep_idt &function, goto_programt &dest)
instructionst instructions
The list of instructions in the goto program.
void set_comment(const irep_idt &comment)
Fresh auxiliary symbol creation.
void apply_contract(goto_programt &goto_program, goto_programt::targett target)
const natural_loops_mutablet::natural_loopt loopt
void code_contracts(symbol_tablet &symbol_table, goto_functionst &goto_functions)
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
symbol_tablet & symbol_table
void code_contracts(goto_functionst::goto_functiont &goto_function)
const irep_idt & id() const
A declaration of a local variable.
code_contractst(symbol_tablet &_symbol_table, goto_functionst &_goto_functions)
std::set< exprt > modifiest
A side effect that returns a non-deterministically chosen value.
goto_function_templatet< goto_programt > goto_functiont
Helper functions for k-induction and loop invariants.
function_mapt function_map
The boolean constant false.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Verify and use annotated invariants and pre/post-conditions.
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
void get_modifies(const local_may_aliast &local_may_alias, const loopt &loop, modifiest &modifies)
Base class for all expressions.
const parameterst & parameters() const
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
unsigned temporary_counter
void insert(const irep_idt &identifier, const exprt &expr)
#define Forall_goto_program_instructions(it, program)
void build_havoc_code(const goto_programt::targett loop_head, const modifiest &modifies, goto_programt &dest)
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
const irept & find(const irep_namet &name) const
const typet & return_type() const
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)
instructionst::iterator targett