assertion_cache Class Reference

@Brief This class stores all asserts conditions and guards for a given SSA, if some pair was already added then it will assume that it is UNSAT. More...

#include <cache.h>

Inheritance diagram for assertion_cache:

Public Member Functions
	assertion_cache (assert_db &db)
bool	run (symex_target_equationt::SSA_stepst &) override
	Executes the algorithm over a T object.
void	run_on_assert (symex_target_equationt::SSA_stept &) override
virtual BigInt	ignored () const override
	How many steps were ignored after this algorithm.
Public Member Functions inherited from ssa_step_algorithm
	ssa_step_algorithm (bool sideffect)
void	run_on_step (symex_target_equationt::SSA_stept &)
virtual void	run_on_assignment (symex_target_equationt::SSA_stept &)
virtual void	run_on_assume (symex_target_equationt::SSA_stept &)
virtual void	run_on_output (symex_target_equationt::SSA_stept &)
virtual void	run_on_skip (symex_target_equationt::SSA_stept &)
virtual void	run_on_renumber (symex_target_equationt::SSA_stept &)
virtual void	run_on_branching (symex_target_equationt::SSA_stept &)
Public Member Functions inherited from algorithm< symex_target_equationt::SSA_stepst >
	algorithm (bool sideeffect)
virtual	~algorithm ()=default
bool	has_sideeffect ()
	Says wether the algorithm is a plain analysis or if it also changes the structure.

Protected Attributes
assert_db &	db
Protected Attributes inherited from algorithm< symex_target_equationt::SSA_stepst >
const bool	sideeffect

Detailed Description

@Brief This class stores all asserts conditions and guards for a given SSA, if some pair was already added then it will assume that it is UNSAT.

Currently, this works for the base case check only.

Constructor & Destructor Documentation

assertion_cache()

assertion_cache::assertion_cache ( assert_db & db )

inline

Member Function Documentation

ignored()

virtual BigInt assertion_cache::ignored ( ) const

inlineoverridevirtual

How many steps were ignored after this algorithm.

Implements ssa_step_algorithm.

run()

bool assertion_cache::run ( symex_target_equationt::SSA_stepst & )

overridevirtual

Executes the algorithm over a T object.

Returns

success of the algorithm

Implements algorithm< symex_target_equationt::SSA_stepst >.

run_on_assert()

void assertion_cache::run_on_assert ( symex_target_equationt::SSA_stept & step )

overridevirtual

Reimplemented from ssa_step_algorithm.

Member Data Documentation

db

assert_db& assertion_cache::db

protected

---

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

• src/util/ssa/cache.h
• src/util/ssa/cache.cpp