cprover
Loading...
Searching...
No Matches
instrument_given_invariants.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Instrument Given Invariants
4
5Author: Daniel Kroening, dkr@amazon.com
6
7\*******************************************************************/
8
11
13
15
16void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
17{
18 auto &body = f.second.body;
19
20 for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
21 {
22 // annotated invariants -- these are stuck to the condition
23 // of the (backwards) goto
24 if(it->is_backwards_goto())
25 {
26 const auto &invariants = static_cast<const exprt &>(
27 it->condition().find(ID_C_spec_loop_invariant));
28
29 for(const auto &invariant : invariants.operands())
30 {
31 auto source_location = invariant.source_location(); // copy
32 source_location.set_property_class("invariant");
33 source_location.set_comment("loop invariant");
34
35 auto assertion =
36 goto_programt::make_assertion(invariant, source_location);
37
38 body.insert_before_swap(it->get_target(), assertion);
39 }
40 }
41 }
42}
43
45{
46 for(auto &f : goto_model.goto_functions.function_map)
48}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
Base class for all expressions.
Definition expr.h:56
const source_locationt & source_location() const
Definition expr.h:223
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition goto_model.h:34
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Symbol Table + CFG.
void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
Instrument Given Invariants.