cprover
ai_domain_baset Class Referenceabstract

#include <ai.h>

Inheritance diagram for ai_domain_baset:
[legend]

Public Types

typedef goto_programt::const_targett locationt
 

Public Member Functions

 ai_domain_baset ()
 
virtual ~ai_domain_baset ()
 
virtual void transform (locationt from, locationt to, ai_baset &ai, const namespacet &ns)=0
 
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
 
virtual void make_top ()=0
 
virtual void make_entry ()=0
 
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...
 

Detailed Description

Definition at line 29 of file ai.h.

Member Typedef Documentation

◆ locationt

Definition at line 42 of file ai.h.

Constructor & Destructor Documentation

◆ ai_domain_baset()

ai_domain_baset::ai_domain_baset ( )
inline

Definition at line 34 of file ai.h.

◆ ~ai_domain_baset()

virtual ai_domain_baset::~ai_domain_baset ( )
inlinevirtual

Definition at line 38 of file ai.h.

Member Function Documentation

◆ ai_simplify()

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

Reimplemented in interval_domaint, and constant_propagator_domaint.

Definition at line 93 of file ai.h.

Referenced by ai_simplify_lhs().

◆ ai_simplify_lhs()

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

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 53 of file ai.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().

◆ make_bottom()

◆ make_entry()

◆ make_top()

◆ 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 24 of file ai.cpp.

References json(), and output().

Referenced by ai_baset::output_json().

◆ output_xml()

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

Definition at line 34 of file ai.cpp.

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

◆ transform()

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

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