Go to the documentation of this file.
12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
44 :
log(message_handler)
54 unsigned atomic_section_id,
61 unsigned atomic_section_id,
68 const exprt &ssa_full_lhs,
69 const exprt &original_full_lhs,
78 const exprt &initializer,
121 const std::list<exprt> &args);
128 const std::list<exprt> &args);
140 const std::string &msg,
152 const std::string &msg,
168 unsigned atomic_section_id,
174 unsigned atomic_section_id,
213 bool optimized_for_single_assertions =
true);
242 return narrow_cast<std::size_t>(std::count_if(
244 return step.is_assert() && !step.ignore && !step.converted;
250 return narrow_cast<std::size_t>(std::count_if(
261 SSA_stepst::iterator it=
SSA_steps.begin();
270 void output(std::ostream &out)
const;
281 return step.source.thread_nr != 0;
288 step.validate(ns, vm);
306 const symex_target_equationt::SSA_stepst::const_iterator a,
307 const symex_target_equationt::SSA_stepst::const_iterator b)
312 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
Class that provides messages with a built-in verbosity 'level'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
SSA_stepst::iterator get_SSA_step(std::size_t s)
std::list< SSA_stept > SSA_stepst
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
Single SSA step in the equation.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
symex_target_equationt(message_handlert &message_handler)
Base class for all expressions.
std::size_t argument_count
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
Expression providing an SSA-renamed symbol of expressions.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
std::size_t count_assertions() const
#define PRECONDITION(CONDITION)
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
virtual void shared_write(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible b...
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
std::size_t count_ignored_SSA_steps() const
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
virtual void output_fmt(const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)
Record formatted output.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
A structure that facilitates collecting the complexity statistics from a decision procedure.
virtual void function_call(const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)
Record a function call.
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
void validate(const namespacet &ns, const validation_modet vm) const
virtual void shared_read(const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment...
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
exprt make_expression() const
Identifies source in the context of symbolic execution.
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
virtual ~symex_target_equationt()=default
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Generate Equation using Symbolic Execution.
The interface of the target container for symbolic execution to record its symbolic steps into.
Wrapper for expressions or types which have been renamed up to a given level.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
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 local variable.