#include <symex_target.h>

Inheritance diagram for symex_targett:

Classes
struct	sourcet

Public Types
enum	step_typet { ASSIGNMENT , ASSUME , ASSERT , OUTPUT , SKIP , RENUMBER , BREANCHING }

Public Member Functions
virtual	~symex_targett ()=default
virtual 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)=0
virtual void	output (const expr2tc &guard, const sourcet &source, const std::string &fmt, const std::list< expr2tc > &args)=0
virtual void	branching (const expr2tc &guard, const expr2tc &cond, const sourcet &source, const bool hidden, unsigned loop_number)=0
virtual void	assumption (const expr2tc &guard, const expr2tc &cond, const sourcet &source, unsigned loop_number)=0
virtual 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)=0
	`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).
virtual void	renumber (const expr2tc &guard, const expr2tc &symbol, const expr2tc &size, const sourcet &source)=0
virtual void	reconstruct_symbolic_expression (expr2tc &expr, bool keep_local_variables) const =0
	Replaces trace symbols from expression with their values.
virtual std::shared_ptr< symex_targett >	clone () const =0
virtual void	push_ctx ()=0
virtual void	pop_ctx ()=0

Member Enumeration Documentation

◆ step_typet

enum symex_targett::step_typet

Enumerator
ASSIGNMENT
ASSUME
ASSERT
OUTPUT
SKIP
RENUMBER
BREANCHING

Constructor & Destructor Documentation

◆ ~symex_targett()

virtual symex_targett::~symex_targett ( )

virtualdefault

Member Function Documentation

◆ assertion()

virtual void symex_targett::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 )

pure virtual

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

Implemented in symex_target_equationt.

◆ assignment()

virtual void symex_targett::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 )