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, locationt)
 
void output (std::ostream &out, const ai_baset &, const namespacet &) const final override
 
virtual void transform (locationt from_l, locationt to_l, ai_baset &ai, const namespacet &ns) final override
 how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable) More...
 
void make_top () final override
 all states – the analysis doesn't use this, and domains may refuse to implement it. More...
 
void make_bottom () final override
 no states More...
 
void make_entry () final override
 a reasonable entry-point state More...
 
bool is_top () const override final
 
bool is_bottom () const override final
 
- Public Member Functions inherited from ai_domain_baset
virtual ~ai_domain_baset ()
 
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
 also add More...
 
virtual bool ai_simplify_lhs (exprt &condition, const namespacet &ns) const
 Simplifies the expression but keeps it as an l-value. More...
 
virtual exprt to_predicate (void) const
 Gives a Boolean condition that is true for all values represented by the domain. 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
 
- Protected Member Functions inherited from ai_domain_baset
 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. More...
 

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

◆ is_bottom()

bool invariant_set_domaint::is_bottom ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 84 of file invariant_set_domain.h.

References has_values, and tvt::is_false().

◆ is_top()

bool invariant_set_domaint::is_top ( ) const
inlinefinaloverridevirtual

Implements ai_domain_baset.

Definition at line 79 of file invariant_set_domain.h.

References has_values, and tvt::is_true().

◆ make_bottom()

void invariant_set_domaint::make_bottom ( )
inlinefinaloverridevirtual

no states

Implements ai_domain_baset.

Definition at line 67 of file invariant_set_domain.h.

References has_values, invariant_set, and invariant_sett::make_false().

◆ make_entry()

void invariant_set_domaint::make_entry ( )
inlinefinaloverridevirtual

a reasonable entry-point state

Implements ai_domain_baset.

Definition at line 73 of file invariant_set_domain.h.

References has_values, invariant_set, and invariant_sett::make_true().

◆ make_top()

void invariant_set_domaint::make_top ( )
inlinefinaloverridevirtual

all states – the analysis doesn't use this, and domains may refuse to implement it.

Implements ai_domain_baset.

Definition at line 61 of file invariant_set_domain.h.

References has_values, invariant_set, and invariant_sett::make_true().

◆ merge()

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

◆ output()

void invariant_set_domaint::output ( std::ostream &  out,
const ai_baset ,
const namespacet  
) const
inlinefinaloverridevirtual

◆ transform()

void invariant_set_domaint::transform ( locationt  from,
locationt  to,
ai_baset ai,
const namespacet ns 
)
finaloverridevirtual

how function calls are treated: a) there is an edge from each call site to the function head b) there is an edge from the last instruction (END_FUNCTION) of the function to the instruction following the call site (this also needs to set the LHS, if applicable)

"this" is the domain before the instruction "from" "from" is the instruction to be interpretted "to" is the next instruction (for GOTO, FUNCTION_CALL, END_FUNCTION)

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") PRECONDITION(are_comparable(from,to) || (from->is_function_call() || from->is_end_function())

Implements ai_domain_baset.

Definition at line 16 of file invariant_set_domain.cpp.

References invariant_sett::apply_code(), ASSERT, ASSIGN, invariant_sett::assignment(), ASSUME, DECL, FUNCTION_CALL, GOTO, invariant_set, code_assignt::lhs(), exprt::make_not(), invariant_sett::make_threaded(), OTHER, RETURN, code_assignt::rhs(), simplify(), START_THREAD, invariant_sett::strengthen(), and to_code_assign().

Member Data Documentation

◆ has_values

tvt invariant_set_domaint::has_values

Definition at line 27 of file invariant_set_domain.h.

Referenced by is_bottom(), is_top(), make_bottom(), make_entry(), make_top(), merge(), and output().

◆ invariant_set

invariant_sett invariant_set_domaint::invariant_set

Definition at line 28 of file invariant_set_domain.h.

Referenced by make_bottom(), make_entry(), make_top(), merge(), output(), and transform().


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