ESBMC
Efficient SMT-based Context-Bounded Model Checker
Loading...
Searching...
No Matches
ssa_features Class Reference

#include <features.h>

Inheritance diagram for ssa_features:
[legend]

Public Member Functions

 ssa_features ()
bool run (symex_target_equationt::SSA_stepst &) override
 Executes the algorithm over a T object.
void print_result () const
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_assert (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.

Public Attributes

std::unordered_set< SSA_FEATURES > features

Protected Member Functions

void check (const expr2tc &e)
bool is_entirely_constant (const expr2tc &e)

Additional Inherited Members

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

Constructor & Destructor Documentation

◆ ssa_features()

ssa_features::ssa_features ( )
inline

Member Function Documentation

◆ check()

void ssa_features::check ( const expr2tc & e)
protected

◆ ignored()

BigInt ssa_features::ignored ( ) const
inlineoverridevirtual

How many steps were ignored after this algorithm.

Implements ssa_step_algorithm.

◆ is_entirely_constant()

bool ssa_features::is_entirely_constant ( const expr2tc & e)
protected

◆ print_result()

void ssa_features::print_result ( ) const

◆ run()

bool ssa_features::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 >.

Member Data Documentation

◆ features

std::unordered_set<SSA_FEATURES> ssa_features::features
The documentation for this class was generated from the following files: