17 if(
source.
pc->source_location().is_not_nil())
18 out <<
" " <<
source.
pc->source_location() <<
'\n';
31 out <<
"LOCATION" <<
'\n';
34 out <<
"INPUT" <<
'\n';
37 out <<
"OUTPUT" <<
'\n';
41 out <<
"DECL" <<
'\n';
46 out <<
"ASSIGNMENT (";
56 out <<
"VISIBLE_ACTUAL_PARAMETER";
59 out <<
"HIDDEN_ACTUAL_PARAMETER";
79 out <<
"FUNCTION_CALL\n";
82 out <<
"FUNCTION_RETURN\n";
85 out <<
"CONSTRAINT\n";
88 out <<
"SHARED READ\n";
91 out <<
"SHARED WRITE\n";
94 out <<
"ATOMIC_BEGIN\n";
97 out <<
"AUTOMIC_END\n";
103 out <<
"MEMORY_BARRIER\n";
153 "Type inequality in SSA assignment\nlhs-type: " +
159 for(
const auto &expr :
io_args)
195 property_id =
source.
pc->source_location().get_property_id();
203 else if(
source.
pc->is_function_call())
222 exprt _original_full_lhs,
227 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)
Single SSA step in the equation.
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
std::vector< exprt > ssa_function_arguments
irep_idt get_property_id() const
Returns the property ID if this is a step resulting from an ASSERT, or builds a unique name for an un...
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
bool is_assignment() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
typet & type()
Return the type of the expression.
Step of the trace of a GOTO program.
const std::string & id_string() const
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.
const exprt & get_original_expr() const
@ 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.
#define PRECONDITION(CONDITION)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
#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...