cprover
Loading...
Searching...
No Matches
frame.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Symbolic Execution
4
5Author: 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
19
21struct 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
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.
67 lexical_loopst::loopt &loop;
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
80};
81
82#endif // CPROVER_GOTO_SYMEX_FRAME_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
The NIL expression.
Definition std_expr.h:2874
goto_statet class definition
Compute lexical loops in a goto_function.
STL namespace.
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.
Generate Equation using Symbolic Execution.