runtime_encoded_equationt Class Reference

#include <symex_target_equation.h>

Inheritance diagram for runtime_encoded_equationt:

Classes
class	dual_unsat_exception
struct	solver_statet

Public Member Functions
	runtime_encoded_equationt (const namespacet &_ns, smt_convt &conv)
	~runtime_encoded_equationt () override
void	push_ctx () override
void	pop_ctx () override
std::shared_ptr< symex_targett >	clone () const override
void	convert (smt_convt &smt_conv, assertion_modet mode=assertion_modet::Violated) override
void	flush_latest_instructions ()
tvt	ask_solver_question (const expr2tc &question)
Public Member Functions inherited from symex_target_equationt
	symex_target_equationt (const namespacet &_ns)
void	assignment (const expr2tc &guard, const expr2tc &lhs, const expr2tc &original_lhs, const expr2tc &rhs, const expr2tc &original_rhs, const sourcet &source, std::vector< stack_framet > stack_trace, const bool hidden, unsigned loop_number) override
void	output (const expr2tc &guard, const sourcet &source, const std::string &fmt, const std::list< expr2tc > &args) override
void	branching (const expr2tc &guard, const expr2tc &cond, const sourcet &source, const bool hidden, unsigned loop_number) override
void	assumption (const expr2tc &guard, const expr2tc &cond, const sourcet &source, unsigned loop_number) override
void	assertion (const expr2tc &guard, const expr2tc &cond, const expr2tc &cond_neg, const std::string &msg, std::vector< stack_framet > stack_trace, const sourcet &source, unsigned loop_number) override
	cond_neg is cond with the claim negated under the same guards, so a probe can ask whether the claim holds on this path using the same encoding the violation query uses (issue #7585).
void	renumber (const expr2tc &guard, const expr2tc &symbol, const expr2tc &size, const sourcet &source) override
void	reconstruct_symbolic_expression (expr2tc &expr, bool keep_local_variables) const override
	Replaces trace symbols from expression with their values.
void	replace_rec (const SSA_stept &step, expr2tc &e, bool keep_local) const
unsigned	count_ignored_SSA_steps () const
SSA_stepst::iterator	get_SSA_step (unsigned s)
void	output (std::ostream &out) const
void	short_output (std::ostream &out, bool show_ignored=false) const
bool	check_for_duplicate_assigns () const
	I10: no SSA name is defined twice.
void	clear ()
unsigned int	clear_assertions ()
std::shared_ptr< symex_targett >	clone () const override
void	push_ctx () override
void	pop_ctx () override
Public Member Functions inherited from symex_targett
virtual	~symex_targett ()=default

Public Attributes
smt_convt &	conv
std::unique_ptr< solver_statet >	solver_state
std::list< SSA_stepst::iterator >	scoped_end_points
SSA_stepst::iterator	cvt_progress
Public Attributes inherited from symex_target_equationt
SSA_stepst	SSA_steps

Additional Inherited Members
Public Types inherited from symex_target_equationt
enum class	assertion_modet { Violated , PathReachable , Satisfiable }
	How an assertion is encoded. More...
typedef std::list< SSA_stept >	SSA_stepst
Public Types inherited from symex_targett
enum	step_typet {   ASSIGNMENT , ASSUME , ASSERT , OUTPUT ,   SKIP , RENUMBER , BREANCHING }
Protected Attributes inherited from symex_target_equationt
const namespacet &	ns
bool	debug_print
bool	ssa_trace
bool	ssa_smt_trace
unsigned	output_count

Constructor & Destructor Documentation

runtime_encoded_equationt()

runtime_encoded_equationt::runtime_encoded_equationt	(	const namespacet &	_ns,
		smt_convt &	conv )

~runtime_encoded_equationt()

runtime_encoded_equationt::~runtime_encoded_equationt ( )

overridedefault

Member Function Documentation

ask_solver_question()

tvt runtime_encoded_equationt::ask_solver_question

(

const expr2tc &

question

)

clone()

std::shared_ptr< symex_targett > runtime_encoded_equationt::clone ( ) const

overridevirtual

Implements symex_targett.

convert()

void runtime_encoded_equationt::convert ( smt_convt & smt_conv, assertion_modet mode = assertion_modet::Violated )

overridevirtual

Reimplemented from symex_target_equationt.

flush_latest_instructions()

void runtime_encoded_equationt::flush_latest_instructions

(

)

pop_ctx()

void runtime_encoded_equationt::pop_ctx ( )

overridevirtual

Implements symex_targett.

push_ctx()

void runtime_encoded_equationt::push_ctx ( )

overridevirtual

Implements symex_targett.

Member Data Documentation

conv

smt_convt& runtime_encoded_equationt::conv

cvt_progress

SSA_stepst::iterator runtime_encoded_equationt::cvt_progress

scoped_end_points

std::list<SSA_stepst::iterator> runtime_encoded_equationt::scoped_end_points

solver_state

std::unique_ptr<solver_statet> runtime_encoded_equationt::solver_state

---

The documentation for this class was generated from the following files:

• src/goto-symex/equation/symex_target_equation.h
• src/goto-symex/equation/symex_target_equation.cpp