Skip to content

Commit 924f738

Browse files
Move framet class to its own file
Having one class per file makes it easier to navigate the code and find what you want.
1 parent d06b2ab commit 924f738

File tree

2 files changed

+53
-37
lines changed

2 files changed

+53
-37
lines changed

src/goto-symex/frame.h

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,52 @@
1+
/*******************************************************************\
2+
3+
Module: Symbolic Execution
4+
5+
Author: Romain Brenguier, [email protected]
6+
7+
\*******************************************************************/
8+
9+
/// \file
10+
/// Class for stack frames
11+
12+
#ifndef CPROVER_GOTO_SYMEX_FRAME_H
13+
#define CPROVER_GOTO_SYMEX_FRAME_H
14+
15+
/// Stack frames -- these are used for function calls and for exceptions
16+
struct framet
17+
{
18+
// gotos
19+
using goto_state_listt = std::list<goto_statet>;
20+
21+
// function calls
22+
irep_idt function_identifier;
23+
std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
24+
symex_targett::sourcet calling_location;
25+
26+
goto_programt::const_targett end_of_function;
27+
exprt return_value = nil_exprt();
28+
bool hidden_function = false;
29+
30+
symex_renaming_levelt::current_namest old_level1;
31+
32+
std::set<irep_idt> local_objects;
33+
34+
// exceptions
35+
std::map<irep_idt, goto_programt::targett> catch_map;
36+
37+
// loop and recursion unwinding
38+
struct loop_infot
39+
{
40+
unsigned count = 0;
41+
bool is_recursion = false;
42+
};
43+
44+
std::unordered_map<irep_idt, loop_infot> loop_iterations;
45+
46+
explicit framet(symex_targett::sourcet _calling_location)
47+
: calling_location(std::move(_calling_location))
48+
{
49+
}
50+
};
51+
52+
#endif // CPROVER_GOTO_SYMEX_FRAME_H

src/goto-symex/goto_symex_state.h

Lines changed: 1 addition & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -24,47 +24,11 @@ Author: Daniel Kroening, [email protected]
2424
#include <util/make_unique.h>
2525
#include <goto-programs/goto_function.h>
2626

27+
#include "frame.h"
2728
#include "goto_state.h"
2829
#include "renaming_level.h"
2930
#include "symex_target_equation.h"
3031

31-
// stack frames -- these are used for function calls and
32-
// for exceptions
33-
struct framet
34-
{
35-
// gotos
36-
using goto_state_listt = std::list<goto_statet>;
37-
38-
// function calls
39-
irep_idt function_identifier;
40-
std::map<goto_programt::const_targett, goto_state_listt> goto_state_map;
41-
symex_targett::sourcet calling_location;
42-
43-
goto_programt::const_targett end_of_function;
44-
exprt return_value = nil_exprt();
45-
bool hidden_function = false;
46-
47-
symex_renaming_levelt::current_namest old_level1;
48-
49-
std::set<irep_idt> local_objects;
50-
51-
// exceptions
52-
std::map<irep_idt, goto_programt::targett> catch_map;
53-
54-
// loop and recursion unwinding
55-
struct loop_infot
56-
{
57-
unsigned count = 0;
58-
bool is_recursion = false;
59-
};
60-
std::unordered_map<irep_idt, loop_infot> loop_iterations;
61-
62-
explicit framet(symex_targett::sourcet _calling_location)
63-
: calling_location(std::move(_calling_location))
64-
{
65-
}
66-
};
67-
6832
/// Central data structure: state.
6933

7034
/// The state is a persistent data structure that symex maintains as it

0 commit comments

Comments
 (0)