Go to the documentation of this file.
28 const std::string &annotation,
36 std::cout <<
'(' << count <<
") ";
37 if(annotation.empty())
38 std::cout << string_value;
40 std::cout << annotation <<
'(' << string_value <<
')';
45 const std::string guard_string =
from_expr(ns, function_id, step.
guard);
47 std::cout <<
"guard: " << guard_string <<
'\n';
55 std::size_t count = 1;
57 std::cout <<
'\n' <<
"Program constraints:" <<
'\n';
59 for(
const auto &step : equation.
SSA_steps)
61 std::cout <<
"// " << step.source.pc->location_number <<
" ";
62 std::cout << step.source.pc->source_location.as_string() <<
"\n";
64 if(step.is_assignment())
66 else if(step.is_assert())
68 else if(step.is_assume())
70 else if(step.is_constraint())
75 else if(step.is_shared_read())
76 show_step(ns, step,
"SHARED_READ", count);
77 else if(step.is_shared_write())
78 show_step(ns, step,
"SHARED_WRITE", count);
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
void show_program(const namespacet &ns, const symex_target_equationt &equation)
Print the steps of equation on the standard output.
static void show_step(const namespacet &ns, const SSA_stept &step, const std::string &annotation, std::size_t &count)
Output a single SSA step.
Single SSA step in the equation.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
bool is_true() const
Return whether the expression is a constant representing true.
symex_targett::sourcet source
bool is_shared_write() const
bool is_shared_read() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)