cprover
frame.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Symbolic Execution
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_SYMEX_FRAME_H
13 #define CPROVER_GOTO_SYMEX_FRAME_H
14 
15 #include "goto_state.h"
16 #include "symex_target.h"
17 
18 #include <analyses/lexical_loops.h>
19 
21 struct framet
22 {
23  // gotos
25  std::list<std::pair<symex_targett::sourcet, goto_statet>>;
26 
27  // function calls
29  std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
31  std::vector<irep_idt> parameter_names;
34  exprt call_lhs = nil_exprt(); // cleaned, but not renamed
36  bool hidden_function = false;
37 
39 
40  std::set<irep_idt> local_objects;
41 
42  // exceptions
43  std::map<irep_idt, goto_programt::targett> catch_map;
44 
45  // loop and recursion unwinding
46  struct loop_infot
47  {
48  unsigned count = 0;
49  bool is_recursion = false;
50  };
51 
53  {
54  public:
55  explicit active_loop_infot(lexical_loopst::loopt &_loop) : loop(_loop)
56  {
57  }
58 
60  std::size_t children_too_complex = 0;
61 
63  std::vector<std::reference_wrapper<lexical_loopst::loopt>>
65 
66  // Loop information.
68  };
69 
70  std::shared_ptr<lexical_loopst> loops_info;
71  std::vector<active_loop_infot> active_loops;
72 
73  std::unordered_map<irep_idt, loop_infot> loop_iterations;
74 
75  framet(symex_targett::sourcet _calling_location, const guardt &state_guard)
76  : calling_location(std::move(_calling_location)),
77  guard_at_function_start(state_guard)
78  {
79  }
80 };
81 
82 #endif // CPROVER_GOTO_SYMEX_FRAME_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
active_loop_infot(lexical_loopst::loopt &_loop)
Definition: frame.h:55
std::size_t children_too_complex
Incremental counter on how many branches this loop has had killed.
Definition: frame.h:60
lexical_loopst::loopt & loop
Definition: frame.h:67
std::vector< std::reference_wrapper< lexical_loopst::loopt > > blacklisted_loops
Set of loop ID's that have been blacklisted.
Definition: frame.h:64
instructionst::const_iterator const_targett
Definition: goto_program.h:593
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
The NIL expression.
Definition: std_expr.h:2874
goto_statet class definition
Compute lexical loops in a goto_function.
nonstd::optional< T > optionalt
Definition: optional.h:35
unsigned count
Definition: frame.h:48
bool is_recursion
Definition: frame.h:49
Stack frames – these are used for function calls and for exceptions.
Definition: frame.h:22
std::map< irep_idt, goto_programt::targett > catch_map
Definition: frame.h:43
std::vector< active_loop_infot > active_loops
Definition: frame.h:71
guardt guard_at_function_start
Definition: frame.h:32
std::list< std::pair< symex_targett::sourcet, goto_statet > > goto_state_listt
Definition: frame.h:25
exprt call_lhs
Definition: frame.h:34
symex_targett::sourcet calling_location
Definition: frame.h:30
std::unordered_map< irep_idt, loop_infot > loop_iterations
Definition: frame.h:73
bool hidden_function
Definition: frame.h:36
std::vector< irep_idt > parameter_names
Definition: frame.h:31
symex_level1t old_level1
Definition: frame.h:38
goto_programt::const_targett end_of_function
Definition: frame.h:33
optionalt< symbol_exprt > return_value_symbol
Definition: frame.h:35
std::set< irep_idt > local_objects
Definition: frame.h:40
framet(symex_targett::sourcet _calling_location, const guardt &state_guard)
Definition: frame.h:75
irep_idt function_identifier
Definition: frame.h:28
std::shared_ptr< lexical_loopst > loops_info
Definition: frame.h:70
std::map< goto_programt::const_targett, goto_state_listt > goto_state_map
Definition: frame.h:29
Functor to set the level 1 renaming of SSA expressions.
Identifies source in the context of symbolic execution.
Definition: symex_target.h:37
Generate Equation using Symbolic Execution.