16 out <<
"Thread " <<
source.thread_nr;
18 if(
source.pc->source_location().is_not_nil())
19 out <<
" " <<
source.pc->source_location() <<
'\n';
32 out <<
"LOCATION" <<
'\n';
35 out <<
"INPUT" <<
'\n';
38 out <<
"OUTPUT" <<
'\n';
42 out <<
"DECL" <<
'\n';
47 out <<
"ASSIGNMENT (";
57 out <<
"VISIBLE_ACTUAL_PARAMETER";
60 out <<
"HIDDEN_ACTUAL_PARAMETER";
80 out <<
"FUNCTION_CALL\n";
83 out <<
"FUNCTION_RETURN\n";
86 out <<
"CONSTRAINT\n";
89 out <<
"SHARED READ\n";
92 out <<
"SHARED WRITE\n";
95 out <<
"ATOMIC_BEGIN\n";
98 out <<
"AUTOMIC_END\n";
104 out <<
"MEMORY_BARRIER\n";
155 "Type inequality in SSA assignment\nlhs-type: " +
156 ssa_lhs.get_original_expr().type().id_string() +
157 "\nrhs-type: " +
ssa_rhs.type().id_string());
161 for(
const auto &expr :
io_args)
194 exprt _original_full_lhs,
199 guard = std::move(_guard);
SSA_assignment_stept(symex_targett::sourcet source, exprt guard, ssa_exprt ssa_lhs, exprt ssa_full_lhs, exprt original_full_lhs, exprt ssa_rhs, symex_targett::assignment_typet assignment_type)
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
std::vector< exprt > ssa_function_arguments
symex_targett::assignment_typet assignment_type
goto_trace_stept::typet type
bool is_constraint() const
bool is_shared_write() const
symex_targett::sourcet source
bool is_shared_read() const
std::list< exprt > io_args
void output(std::ostream &out) const
SSA_stept(const symex_targett::sourcet &_source, goto_trace_stept::typet _type)
bool is_assignment() const
Base class for all expressions.
Step of the trace of a GOTO program.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression providing an SSA-renamed symbol of expressions.
@ VISIBLE_ACTUAL_PARAMETER
@ HIDDEN_ACTUAL_PARAMETER
The type of an expression, extends irept.
const std::string & id2string(const irep_idt &d)
#define UNREACHABLE
This should be used to mark dead code.
Identifies source in the context of symbolic execution.
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...