38 unsigned atomic_section_id,
57 unsigned atomic_section_id,
102 unsigned atomic_section_id,
107 SSA_step.
guard=guard;
118 unsigned atomic_section_id,
123 SSA_step.
guard=guard;
135 const exprt &ssa_full_lhs,
136 const exprt &original_full_lhs,
137 const exprt &ssa_rhs,
146 SSA_step.
guard=guard;
174 SSA_step.
guard=guard;
206 SSA_step.
guard=guard;
222 SSA_step.
guard=guard;
239 SSA_step.
guard=guard;
252 const std::list<exprt> &args)
257 SSA_step.
guard=guard;
261 SSA_step.
io_id=output_id;
272 const std::list<exprt> &args)
277 SSA_step.
guard=guard;
281 SSA_step.
io_id=output_id;
293 const std::list<exprt> &args)
298 SSA_step.
guard=guard;
302 SSA_step.
io_id=input_id;
316 SSA_step.
guard=guard;
328 const std::string &msg,
334 SSA_step.
guard=guard;
352 SSA_step.
guard=guard;
363 const std::string &msg,
400 if(step.is_assignment() && !step.ignore)
412 if(step.is_decl() && !step.ignore)
416 prop_conv.
convert(step.cond_expr);
431 step.guard_literal=prop_conv.
convert(step.guard);
447 step.cond_literal=prop_conv.
convert(step.cond_expr);
464 step.cond_literal=prop_conv.
convert(step.cond_expr);
477 if(step.is_constraint())
497 if(number_of_assertions==0)
500 if(number_of_assertions==1)
510 else if(step.is_assume())
520 disjuncts.reserve(number_of_assertions);
533 step.cond_literal=prop_conv.
convert(implication);
538 else if(step.is_assume())
565 for(
const auto &arg : step.io_args)
567 if(arg.is_constant() ||
568 arg.id()==ID_string_constant)
569 step.converted_io_args.push_back(arg);
573 symbol.
type()=arg.type();
579 dec_proc.
set_to(eq,
true);
580 step.converted_io_args.push_back(symbol);
598 for(
auto &step : SSA_step.
io_args)
608 step.output(
ns, out);
609 out <<
"--------------\n";
615 std::ostream &out)
const 619 out <<
"Thread " <<
source.thread_nr;
621 if(
source.pc->source_location.is_not_nil())
622 out <<
" " <<
source.pc->source_location <<
'\n';
634 out <<
"LOCATION" <<
'\n';
break;
636 out <<
"INPUT" <<
'\n';
break;
638 out <<
"OUTPUT" <<
'\n';
break;
641 out <<
"DECL" <<
'\n';
646 out <<
"ASSIGNMENT (";
656 out <<
"VISIBLE_ACTUAL_PARAMETER";
659 out <<
"HIDDEN_ACTUAL_PARAMETER";
676 out <<
"DEAD\n";
break;
678 out <<
"FUNCTION_CALL\n";
break;
680 out <<
"FUNCTION_RETURN\n";
break;
682 out <<
"CONSTRAINT\n";
break;
684 out <<
"SHARED READ\n";
break;
686 out <<
"SHARED WRITE\n";
break;
688 out <<
"ATOMIC_BEGIN\n";
break;
690 out <<
"AUTOMIC_END\n";
break;
692 out <<
"SPAWN\n";
break;
694 out <<
"MEMORY_BARRIER\n";
break;
698 default: assert(
false);
virtual void spawn(const exprt &guard, const sourcet &source)
spawn a new thread
virtual void function_call(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Generate Equation using Symbolic Execution.
void convert(prop_convt &prop_conv)
unsigned atomic_section_id
void convert_assumptions(prop_convt &prop_conv)
converts assumptions
bool is_shared_read() const
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
record an assumption
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
just record input
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
record a goto instruction
bool is_constraint() const
assignment_typet assignment_type
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
start an atomic section
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
end an atomic section
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
write to a sharedvariable
bool is_shared_write() const
The boolean constant true.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
record a constraint
symex_target_equationt(const namespacet &_ns)
void convert_constraints(decision_proceduret &decision_procedure) const
converts constraints
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
declare a fresh variable
API to expression classes.
virtual ~symex_target_equationt()
virtual void assignment(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)
write to a variable
virtual literalt convert(const exprt &expr)=0
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
just record formatted output
virtual void set_to(const exprt &expr, bool value)=0
bool is_assignment() const
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args)
just record output
std::list< exprt > io_args
exprt disjunction(const exprt::operandst &op)
std::vector< exprt > operandst
void convert_goto_instructions(prop_convt &prop_conv)
converts goto instructions
literalt const_literal(bool value)
void convert_assignments(decision_proceduret &decision_procedure) const
converts assignments
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
read from a shared variable
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
record an assertion
void convert_assertions(prop_convt &prop_conv)
converts assertions
void set_to_false(const exprt &expr)
void convert_decls(prop_convt &prop_conv) const
converts declarations
Base class for all expressions.
virtual void function_return(const exprt &guard, const irep_idt &identifier, const sourcet &source)
just record a location
void set_to_true(const exprt &expr)
const exprt & get_original_expr() const
virtual void location(const exprt &guard, const sourcet &source)
just record a location
void set_identifier(const irep_idt &identifier)
Expression to hold a symbol (variable)
std::ostream & operator<<(std::ostream &out, const symex_target_equationt &equation)
void output(const namespacet &ns, std::ostream &out) const
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
declare a fresh variable
void merge_ireps(SSA_stept &SSA_step)
goto_trace_stept::typet type
unsigned count_assertions() const
Expression providing an SSA-renamed symbol of expressions.
void convert_guards(prop_convt &prop_conv)
converts guards
void convert_io(decision_proceduret &decision_procedure)
converts I/O