#include <symex_target_equation.h>

Inheritance diagram for symex_target_equationt:

Classes
class	SSA_stept

Public Types
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 }

Public Member Functions
	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
virtual void	convert (smt_convt &smt_conv, assertion_modet mode=assertion_modet::Violated)
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
SSA_stepst	SSA_steps

Protected Attributes
const namespacet &	ns
bool	debug_print
bool	ssa_trace
bool	ssa_smt_trace
unsigned	output_count

Member Typedef Documentation

◆ SSA_stepst

typedef std::list<SSA_stept> symex_target_equationt::SSA_stepst

Member Enumeration Documentation

◆ assertion_modet

enum class symex_target_equationt::assertion_modet

strong

How an assertion is encoded.

Violated – not(assumpt -> cond): can the claim be violated? PathReachable – assumpt: is the path to it feasible at all? Satisfiable – not(assumpt -> cond_neg): can the claim hold? UNSAT means no feasible path satisfies it, so a violation found against an over-approximation is one the approximation's own constraints force (issue #7585).

Enumerator
Violated
PathReachable
Satisfiable

Constructor & Destructor Documentation

◆ symex_target_equationt()

symex_target_equationt::symex_target_equationt ( const namespacet & _ns )

inline

Member Function Documentation

◆ assertion()

void symex_target_equationt::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 )

overridevirtual

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).

Implements symex_targett.

◆ assignment()

void symex_target_equationt::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 )

overridevirtual

Implements symex_targett.

◆ assumption()

void symex_target_equationt::assumption	(	const expr2tc &	guard,
		const expr2tc &	cond,
		const sourcet &	source,
		unsigned	loop_number )

overridevirtual

Implements symex_targett.

◆ branching()

void symex_target_equationt::branching	(	const expr2tc &	guard,
		const expr2tc &	cond,
		const sourcet &	source,
		const bool	hidden,
		unsigned	loop_number )

overridevirtual

Implements symex_targett.

◆ check_for_duplicate_assigns()

bool symex_target_equationt::check_for_duplicate_assigns ( ) const

I10: no SSA name is defined twice.

Returns false, with one error per offender, when the equation is malformed. Opt-in via --double-assign-check; aborts if an assignment step's lhs is not a symbol, which is assignment()'s precondition.

◆ clear()

void symex_target_equationt::clear ( )

inline

◆ clear_assertions()

unsigned int symex_target_equationt::clear_assertions ( )

◆ clone()

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

inlineoverridevirtual

Implements symex_targett.

◆ convert()

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

virtual

Reimplemented in runtime_encoded_equationt.

◆ count_ignored_SSA_steps()

unsigned symex_target_equationt::count_ignored_SSA_steps ( ) const

inline

◆ get_SSA_step()

SSA_stepst::iterator symex_target_equationt::get_SSA_step ( unsigned s )

inline

◆ output() [1/2]

void symex_target_equationt::output	(	const expr2tc &	guard,
		const sourcet &	source,
		const std::string &	fmt,
		const std::list< expr2tc > &	args )

overridevirtual

Implements symex_targett.

◆ output() [2/2]

void symex_target_equationt::output ( std::ostream & out ) const

◆ pop_ctx()

void symex_target_equationt::pop_ctx ( )

overridevirtual

Implements symex_targett.

◆ push_ctx()

void symex_target_equationt::push_ctx ( )

overridevirtual

Implements symex_targett.

◆ reconstruct_symbolic_expression()

void symex_target_equationt::reconstruct_symbolic_expression	(	expr2tc &	expr,
		bool	keep_local_variables ) const

overridevirtual

Replaces trace symbols from expression with their values.

For example, for a trace a0 = nondet_symbol(0); a1 = a0 + 1; guard = a1 > 5) calling this function with "guard" will result in:

keep_local_variables(true): a1 > 5
keep_local_variables(false): nondet_symbol(0) + 1 > 5

Parameters

expr
keep_local_variables

Implements symex_targett.

◆ renumber()

void symex_target_equationt::renumber	(	const expr2tc &	guard,
		const expr2tc &	symbol,
		const expr2tc &	size,
		const sourcet &	source )

overridevirtual

Implements symex_targett.

◆ replace_rec()

void symex_target_equationt::replace_rec	(	const SSA_stept &	step,
		expr2tc &	e,
		bool	keep_local ) const

◆ short_output()

void symex_target_equationt::short_output	(	std::ostream &	out,
		bool	show_ignored = false ) const

Member Data Documentation

◆ debug_print

bool symex_target_equationt::debug_print

protected

◆ ns

const namespacet& symex_target_equationt::ns

protected

◆ output_count

unsigned symex_target_equationt::output_count

protected

◆ ssa_smt_trace

bool symex_target_equationt::ssa_smt_trace

protected

◆ SSA_steps

SSA_stepst symex_target_equationt::SSA_steps

◆ ssa_trace

bool symex_target_equationt::ssa_trace

protected

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

Classes

Public Types

Public Member Functions

Public Attributes

Protected Attributes

Member Typedef Documentation

◆ SSA_stepst

Member Enumeration Documentation

◆ assertion_modet

Constructor & Destructor Documentation

◆ symex_target_equationt()

Member Function Documentation

◆ assertion()

◆ assignment()

◆ assumption()

◆ branching()

◆ check_for_duplicate_assigns()

◆ clear()

◆ clear_assertions()

◆ clone()

◆ convert()

◆ count_ignored_SSA_steps()

◆ get_SSA_step()

◆ output() [1/2]

◆ output() [2/2]

◆ pop_ctx()

◆ push_ctx()

◆ reconstruct_symbolic_expression()

◆ renumber()

◆ replace_rec()

◆ short_output()

Member Data Documentation

◆ debug_print

◆ ns

◆ output_count

◆ ssa_smt_trace

◆ SSA_steps

◆ ssa_trace