cprover
constant_propagator_domaint Class Reference

#include <constant_propagator.h>

Inheritance diagram for constant_propagator_domaint:
[legend]
Collaboration diagram for constant_propagator_domaint:
[legend]

Classes

struct  valuest
 

Public Member Functions

void transform (locationt, locationt, ai_baset &, const namespacet &) final
 
void output (std::ostream &, const ai_baset &, const namespacet &) const final
 
void make_top () final
 
void make_bottom () final
 
void make_entry () final
 
bool merge (const constant_propagator_domaint &, locationt, locationt)
 
virtual bool ai_simplify (exprt &condition, const namespacet &ns) const override
 Simplify the condition given context-sensitive knowledge from the abstract state. More...
 
- Public Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 
virtual ~ai_domain_baset ()
 
virtual void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 
virtual jsont output_json (const ai_baset &ai, const namespacet &ns) const
 
virtual xmlt output_xml (const ai_baset &ai, const namespacet &ns) const
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Use the information in the domain to simplify the expression on the LHS of an assignment. More...
 

Public Attributes

valuest values
 

Private Member Functions

void assign (valuest &dest, const symbol_exprt &lhs, exprt rhs, const namespacet &ns) const
 
void assign_rec (valuest &values, const exprt &lhs, const exprt &rhs, const namespacet &ns)
 
bool two_way_propagate_rec (const exprt &expr, const namespacet &ns)
 handles equalities and conjunctions containing equalities More...
 

Additional Inherited Members

- Public Types inherited from ai_domain_baset
typedef goto_programt::const_targett locationt
 

Detailed Description

Definition at line 19 of file constant_propagator.h.

Member Function Documentation

◆ ai_simplify()

bool constant_propagator_domaint::ai_simplify ( exprt condition,
const namespacet ns 
) const
overridevirtual

Simplify the condition given context-sensitive knowledge from the abstract state.

parameters: The condition to simplify and its namespace.
Returns
The simplified condition.

Reimplemented from ai_domain_baset.

Definition at line 270 of file constant_propagator.cpp.

References replace_symbol_extt::replace(), constant_propagator_domaint::valuest::replace_const, simplify(), and values.

◆ assign()

void constant_propagator_domaint::assign ( valuest dest,
const symbol_exprt lhs,
exprt  rhs,
const namespacet ns 
) const
private

◆ assign_rec()

◆ make_bottom()

void constant_propagator_domaint::make_bottom ( )
inlinefinalvirtual

◆ make_entry()

void constant_propagator_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 33 of file constant_propagator.h.

References constant_propagator_domaint::valuest::set_to_top(), and values.

◆ make_top()

void constant_propagator_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 31 of file constant_propagator.h.

References constant_propagator_domaint::valuest::set_to_top(), and values.

◆ merge()

bool constant_propagator_domaint::merge ( const constant_propagator_domaint other,
locationt  from,
locationt  to 
)
Returns
Return true if "this" has changed.

Definition at line 459 of file constant_propagator.cpp.

References constant_propagator_domaint::valuest::merge(), and values.

◆ output()

void constant_propagator_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
finalvirtual

Reimplemented from ai_domain_baset.

Definition at line 371 of file constant_propagator.cpp.

References constant_propagator_domaint::valuest::output(), and values.

Referenced by transform().

◆ transform()

◆ two_way_propagate_rec()

bool constant_propagator_domaint::two_way_propagate_rec ( const exprt expr,
const namespacet ns 
)
private

Member Data Documentation

◆ values

valuest constant_propagator_domaint::values

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