25 <<
"Program constraints:" 28 for(
const auto &step : equation.
SSA_steps)
30 std::cout <<
"// " << step.source.pc->location_number <<
" ";
31 std::cout << step.source.pc->source_location.as_string() <<
"\n";
32 const irep_idt &
function = step.source.function;
34 if(step.is_assignment())
36 std::string string_value =
from_expr(ns,
function, step.cond_expr);
37 std::cout <<
"(" << count <<
") " << string_value <<
"\n";
39 if(!step.guard.is_true())
41 std::string string_value =
from_expr(ns,
function, step.guard);
43 std::cout <<
"guard: " << string_value <<
"\n";
48 else if(step.is_assert())
50 std::string string_value =
from_expr(ns,
function, step.cond_expr);
51 std::cout <<
"(" << count <<
") ASSERT(" << string_value <<
") " 54 if(!step.guard.is_true())
56 std::string string_value =
from_expr(ns,
function, step.guard);
58 std::cout <<
"guard: " << string_value <<
"\n";
63 else if(step.is_assume())
65 std::string string_value =
from_expr(ns,
function, step.cond_expr);
66 std::cout <<
"(" << count <<
") ASSUME(" << string_value <<
") " 69 if(!step.guard.is_true())
71 std::string string_value =
from_expr(ns,
function, step.guard);
73 std::cout <<
"guard: " << string_value <<
"\n";
78 else if(step.is_constraint())
80 std::string string_value =
from_expr(ns,
function, step.cond_expr);
81 std::cout <<
"(" << count <<
") CONSTRAINT(" << string_value <<
") " 86 else if(step.is_shared_read() || step.is_shared_write())
88 std::string string_value =
from_expr(ns,
function, step.ssa_lhs);
89 std::cout <<
"(" << count <<
") SHARED_" 90 << (step.is_shared_write() ?
"WRITE" :
"READ") <<
"(" 91 << string_value <<
")\n";
93 if(!step.guard.is_true())
95 std::string string_value =
from_expr(ns,
function, step.guard);
97 std::cout <<
"guard: " << string_value <<
"\n";
Generate Equation using Symbolic Execution.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void show_program(const namespacet &ns, const symex_target_equationt &equation)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Output of the program (SSA) constraints.