cprover
interval_analysis.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Interval Analysis
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "interval_analysis.h"
13 
14 #include <util/find_symbols.h>
15 
16 #include "interval_domain.h"
17 
20  goto_functionst::goto_functiont &goto_function)
21 {
22  std::set<symbol_exprt> symbols;
23 
24  forall_goto_program_instructions(i_it, goto_function.body)
25  {
26  find_symbols(i_it->code, symbols);
27  find_symbols(i_it->guard, symbols);
28  }
29 
30  Forall_goto_program_instructions(i_it, goto_function.body)
31  {
32  if(i_it==goto_function.body.instructions.begin())
33  {
34  // first instruction, we instrument
35  }
36  else
37  {
38  goto_programt::const_targett previous=i_it;
39  previous--;
40  if(previous->is_goto() && !previous->guard.is_true())
41  {
42  // we follow a branch, instrument
43  }
44  else if(previous->is_function_call() && !previous->guard.is_true())
45  {
46  // we follow a function call, instrument
47  }
48  else if(i_it->is_target() || i_it->is_function_call())
49  {
50  // we are a target or a function call, instrument
51  }
52  else
53  continue; // don't instrument
54  }
55 
56  const interval_domaint &d=interval_analysis[i_it];
57 
58  exprt::operandst assertion;
59 
60  for(const auto &symbol_expr : symbols)
61  {
62  exprt tmp=d.make_expression(symbol_expr);
63  if(!tmp.is_true())
64  assertion.push_back(tmp);
65  }
66 
67  if(!assertion.empty())
68  {
70  goto_function.body.insert_before_swap(i_it);
71  t->make_assumption(conjunction(assertion));
72  i_it++; // goes to original instruction
73  t->source_location=i_it->source_location;
74  t->function=i_it->function;
75  }
76  }
77 }
78 
79 void interval_analysis(goto_modelt &goto_model)
80 {
82 
83  const namespacet ns(goto_model.symbol_table);
84  interval_analysis(goto_model.goto_functions, ns);
85 
86  Forall_goto_functions(f_it, goto_model.goto_functions)
88 }
Interval Analysis.
Definition: ai.h:294
bool is_true() const
Definition: expr.cpp:124
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
instructionst::iterator targett
Definition: goto_program.h:397
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
::goto_functiont goto_functiont
exprt make_expression(const symbol_exprt &) const
std::vector< exprt > operandst
Definition: expr.h:45
Interval Domain.
void instrument_intervals(const ait< interval_domaint > &interval_analysis, goto_functionst::goto_functiont &goto_function)
Base class for all expressions.
Definition: expr.h:42
#define Forall_goto_functions(it, functions)
const source_locationt & source_location() const
Definition: expr.h:125
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
void interval_analysis(goto_modelt &goto_model)
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:735
void find_symbols(const exprt &src, find_symbols_sett &dest)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32