cprover
invariant_set_domaint Class Reference

#include <invariant_set_domain.h>

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

Public Member Functions

 invariant_set_domaint ()
 
bool merge (const invariant_set_domaint &other, locationt from, locationt to)
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
 
virtual void transform (locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final
 
void make_top () final
 
void make_bottom () final
 
void make_entry () final
 
- 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 (exprt &condition, 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

tvt has_values
 
invariant_sett invariant_set
 

Additional Inherited Members

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

Detailed Description

Definition at line 20 of file invariant_set_domain.h.

Constructor & Destructor Documentation

§ invariant_set_domaint()

invariant_set_domaint::invariant_set_domaint ( )
inline

Definition at line 23 of file invariant_set_domain.h.

Member Function Documentation

§ make_bottom()

void invariant_set_domaint::make_bottom ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 67 of file invariant_set_domain.h.

References invariant_sett::make_false().

§ make_entry()

void invariant_set_domaint::make_entry ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 73 of file invariant_set_domain.h.

References invariant_sett::make_true().

§ make_top()

void invariant_set_domaint::make_top ( )
inlinefinalvirtual

Implements ai_domain_baset.

Definition at line 61 of file invariant_set_domain.h.

References invariant_sett::make_true().

§ merge()

bool invariant_set_domaint::merge ( const invariant_set_domaint other,
locationt  from,
locationt  to 
)
inline

§ output()

void invariant_set_domaint::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
inlinefinalvirtual

Reimplemented from ai_domain_baset.

Definition at line 44 of file invariant_set_domain.h.

References tvt::is_known(), invariant_sett::output(), tvt::to_string(), and transform().

§ transform()

Member Data Documentation

§ has_values

tvt invariant_set_domaint::has_values

Definition at line 27 of file invariant_set_domain.h.

§ invariant_set

invariant_sett invariant_set_domaint::invariant_set

Definition at line 28 of file invariant_set_domain.h.

Referenced by merge(), and transform().


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