cprover
ai_domain_baset Class Referenceabstract

The interface offered by a domain, allows code to manipulate domains without knowing their exact type. More...

#include <ai_domain.h>

Inheritance diagram for ai_domain_baset:
[legend]

Public Types

typedef goto_programt::const_targett locationt
 

Public Member Functions

virtual ~ai_domain_baset ()
 
virtual void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 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...
 
virtual void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const
 
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 void make_bottom ()=0
 no states More...
 
virtual void make_top ()=0
 all states – the analysis doesn't use this, and domains may refuse to implement it. More...
 
virtual void make_entry ()=0
 a reasonable entry-point state More...
 
virtual bool is_bottom () const =0
 
virtual bool is_top () const =0
 
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...
 

Protected Member Functions

 ai_domain_baset ()
 The constructor is expected to produce 'false' or 'bottom'. More...
 

Detailed Description

The interface offered by a domain, allows code to manipulate domains without knowing their exact type.

Derive from this to implement domains.

Definition at line 27 of file ai_domain.h.

Member Typedef Documentation

◆ locationt

Constructor & Destructor Documentation

◆ ai_domain_baset()

ai_domain_baset::ai_domain_baset ( )
inlineprotected

The constructor is expected to produce 'false' or 'bottom'.

Definition at line 31 of file ai_domain.h.

◆ ~ai_domain_baset()

virtual ai_domain_baset::~ai_domain_baset ( )
inlinevirtual

Definition at line 36 of file ai_domain.h.

Member Function Documentation

◆ ai_simplify()

virtual bool ai_domain_baset::ai_simplify ( exprt condition,
const namespacet ns 
) const
inlinevirtual

also add

bool merge(const T &b, locationt from, locationt to);

This computes the join between "this" and "b". Return true if "this" has changed. In the usual case, "b" is the updated state after "from" and "this" is the state before "to".

PRECONDITION(from.is_dereferenceable(), "Must not be _::end()") PRECONDITION(to.is_dereferenceable(), "Must not be _::end()") This method allows an expression to be simplified / evaluated using the current state. It is used to evaluate assertions and in program simplification return true if unchanged

Reimplemented in interval_domaint, and constant_propagator_domaint.

Definition at line 103 of file ai_domain.h.

Referenced by ai_simplify_lhs(), and static_verifier().

◆ ai_simplify_lhs()

bool ai_domain_baset::ai_simplify_lhs ( exprt condition,
const namespacet ns 
) const
virtual

Simplifies the expression but keeps it as an l-value.

Use the information in the domain to simplify the expression on the LHS of an assignment.

This for example won't simplify symbols to their values, but does simplify indices in arrays, members of structs and dereferencing of pointers

Parameters
conditionthe expression to simplify
nsthe namespace
Returns
True if condition did not change. False otherwise. condition will be updated with the simplified condition if it has worked

Definition at line 42 of file ai_domain.cpp.

References ai_simplify(), member_exprt::compound(), irept::id(), index_exprt::index(), dereference_exprt::pointer(), simplify_expr(), to_dereference_expr(), to_index_expr(), and to_member_expr().

◆ is_bottom()

◆ is_top()

◆ make_bottom()

◆ make_entry()

◆ make_top()

virtual void ai_domain_baset::make_top ( )
pure virtual

◆ output()

virtual void ai_domain_baset::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
inlinevirtual

◆ output_json()

jsont ai_domain_baset::output_json ( const ai_baset ai,
const namespacet ns 
) const
virtual

Reimplemented in dep_graph_domaint.

Definition at line 16 of file ai_domain.cpp.

References json(), and output().

◆ output_xml()

xmlt ai_domain_baset::output_xml ( const ai_baset ai,
const namespacet ns 
) const
virtual

Definition at line 25 of file ai_domain.cpp.

References xmlt::data, output(), and xml().

◆ to_predicate()

virtual exprt ai_domain_baset::to_predicate ( void  ) const
inlinevirtual

Gives a Boolean condition that is true for all values represented by the domain.

This allows domains to be converted into program invariants.

Definition at line 113 of file ai_domain.h.

References is_bottom().

◆ transform()

virtual void ai_domain_baset::transform ( locationt  from,
locationt  to,
ai_baset ai,
const namespacet ns 
)
pure virtual

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())

Implemented in rd_range_domaint, dep_graph_domaint, invariant_set_domaint, is_threaded_domaint, interval_domaint, uninitialized_domaint, escape_domaint, global_may_alias_domaint, custom_bitvector_domaint, and constant_propagator_domaint.

Referenced by ai_baset::do_function_call(), and ai_baset::visit().


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