CBMC
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
14#include <util/expr_util.h>
15
17
18void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
19{
20 auto &body = f.second.body;
21
22 for(auto it = body.instructions.begin(); it != body.instructions.end(); it++)
23 {
24 // annotated invariants -- these are stuck to the condition
25 // of the (backwards) goto
26 if(it->is_backwards_goto())
27 {
28 const auto &invariants = static_cast<const exprt &>(
29 it->condition().find(ID_C_spec_loop_invariant));
30 if(!invariants.is_nil())
31 {
32 if(has_subexpr(invariants, ID_side_effect))
33 {
35 "Loop invariant is not side-effect free.",
36 it->condition().find_source_location());
37 }
38 }
39
40 for(const auto &invariant : invariants.operands())
41 {
42 auto source_location = invariant.source_location(); // copy
43 source_location.set_property_class("invariant");
44 source_location.set_comment("loop invariant");
45
46 auto assertion =
47 goto_programt::make_assertion(invariant, source_location);
48
49 body.insert_before_swap(it->get_target(), assertion);
50 }
51 }
52 }
53}
54
56{
57 for(auto &f : goto_model.goto_functions.function_map)
59}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
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())
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
Deprecated expression utility functions.
Symbol Table + CFG.
void instrument_given_invariants(goto_functionst::function_mapt::value_type &f)
Instrument Given Invariants.