cprover
path_symex_history.cpp
Go to the documentation of this file.
1
/*******************************************************************\
2
3
Module: History of path-based symbolic simulator
4
5
Author: Daniel Kroening, kroening@kroening.com
6
7
\*******************************************************************/
8
11
12
#include "
path_symex_history.h
"
13
14
#include <algorithm>
15
16
#include <
util/decision_procedure.h
>
17
18
#include <
langapi/language_util.h
>
19
20
void
path_symex_stept::output
(std::ostream &out)
const
21
{
22
out <<
"PCs:"
;
23
24
/*
25
for(pc_vectort::const_iterator p_it=s_it->pc_vector.begin();
26
p_it!=pc_vector.end();
27
p_it++)
28
out << " " << *p_it;
29
*/
30
out <<
"\n"
;
31
32
out <<
"Guard: "
<<
from_expr
(
guard
) <<
"\n"
;
33
out <<
"Full LHS: "
<<
from_expr
(
full_lhs
) <<
"\n"
;
34
out <<
"SSA LHS: "
<<
from_expr
(
ssa_lhs
) <<
"\n"
;
35
out <<
"SSA RHS: "
<<
from_expr
(
ssa_rhs
) <<
"\n"
;
36
out <<
"\n"
;
37
}
38
39
void
path_symex_stept::convert
(
decision_proceduret
&dest)
const
40
{
41
if
(
ssa_rhs
.
is_not_nil
())
42
dest <<
equal_exprt
(
ssa_lhs
,
ssa_rhs
);
43
44
if
(
guard
.
is_not_nil
())
45
dest <<
guard
;
46
}
47
48
void
path_symex_step_reft::build_history
(
49
std::vector<path_symex_step_reft> &dest)
const
50
{
51
dest.clear();
52
53
path_symex_step_reft
s=*
this
;
54
while
(!s.
is_nil
())
55
{
56
dest.push_back(s);
57
--s;
58
}
59
60
// the above goes backwards: now need to reverse
61
std::reverse(dest.begin(), dest.end());
62
}
path_symex_history.h
History for path-based symbolic simulator.
irept::is_not_nil
bool is_not_nil() const
Definition:
irep.h:104
path_symex_step_reft
Definition:
path_symex_history.h:28
path_symex_step_reft::build_history
void build_history(std::vector< path_symex_step_reft > &dest) const
Definition:
path_symex_history.cpp:48
language_util.h
from_expr
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Definition:
language_util.cpp:40
path_symex_stept::ssa_rhs
exprt ssa_rhs
Definition:
path_symex_history.h:108
decision_procedure.h
Decision Procedure Interface.
path_symex_stept::convert
void convert(decision_proceduret &dest) const
Definition:
path_symex_history.cpp:39
path_symex_stept::full_lhs
exprt full_lhs
Definition:
path_symex_history.h:109
equal_exprt
equality
Definition:
std_expr.h:1082
path_symex_step_reft::is_nil
bool is_nil() const
Definition:
path_symex_history.h:43
path_symex_stept::output
void output(std::ostream &) const
Definition:
path_symex_history.cpp:20
decision_proceduret
Definition:
decision_procedure.h:20
path_symex_stept::guard
exprt guard
Definition:
path_symex_history.h:108
path_symex_stept::ssa_lhs
symbol_exprt ssa_lhs
Definition:
path_symex_history.h:110
path-symex
path_symex_history.cpp
Generated by
1.8.12