cprover
context_abstract_objectt Class Reference

#include <context_abstract_object.h>

+ Inheritance diagram for context_abstract_objectt:
+ Collaboration diagram for context_abstract_objectt:

Public Member Functions

 context_abstract_objectt (const abstract_object_pointert child, const typet &type)
 
 context_abstract_objectt (const abstract_object_pointert child, const typet &type, bool top, bool bottom)
 
 context_abstract_objectt (const abstract_object_pointert child, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 
virtual ~context_abstract_objectt ()
 
const typettype () const override
 Get the real type of the variable this abstract object is representing. More...
 
bool is_top () const override
 Find out if the abstract object is top. More...
 
bool is_bottom () const override
 Find out if the abstract object is bottom. More...
 
exprt to_constant () const override
 Converts to a constant expression if possible. More...
 
abstract_object_pointert expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
 Try to resolve an expression with the maximum level of precision available. More...
 
void output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const override
 Output a representation of the value of this abstract object. More...
 
abstract_object_pointert unwrap_context () const override
 
void get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
 
abstract_object_pointert get_child () const
 
- Public Member Functions inherited from abstract_objectt
 abstract_objectt (const typet &type)
 
 abstract_objectt (const typet &type, bool top, bool bottom)
 Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true. More...
 
 abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 Construct an abstract object from the expression. More...
 
 abstract_objectt (const typet &type, const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 Ctor for building object of types that differ from the types of input expressions. More...
 
virtual ~abstract_objectt ()
 
virtual bool verify () const
 Verify the internal structure of an abstract_object is correct. More...
 
virtual abstract_object_pointert meet (const abstract_object_pointert &other) const
 Base implementation of the meet operation: only used if no more precise abstraction can be used, can only result in {TOP, BOTTOM, one of the original objects}. More...
 
virtual abstract_object_pointert update_location_context (const locationst &locations, const bool update_sub_elements) const
 Update the location context for an abstract object, potentially propogating the update to any children of this abstract object. More...
 
abstract_object_pointert make_top () const
 
abstract_object_pointert clear_top () const
 
virtual abstract_object_pointert visit_sub_elements (const abstract_object_visitort &visitor) const
 Apply a visitor operation to all sub elements of this abstract_object. More...
 
virtual size_t internal_hash () const
 
virtual bool internal_equality (const abstract_object_pointert &other) const
 

Protected Member Functions

void set_child (const abstract_object_pointert &child)
 
void set_top_internal () override
 
void set_not_top_internal () override
 
abstract_object_pointert write (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &specifier, const abstract_object_pointert &value, bool merging_write) const override
 A helper function to evaluate writing to a component of an abstract object. More...
 
bool has_been_modified (const abstract_object_pointert before) const override
 Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. More...
 
- Protected Member Functions inherited from abstract_objectt
virtual internal_abstract_object_pointert mutable_clone () const
 
abstract_object_pointert abstract_object_merge (const abstract_object_pointert other) const
 Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More...
 
bool should_use_base_merge (const abstract_object_pointert other) const
 To detect the cases where the base merge is sufficient to do a merge We can't do if this->is_bottom() since we want the specific. More...
 
virtual abstract_object_pointert merge (abstract_object_pointert other) const
 Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself. More...
 
abstract_object_pointert abstract_object_meet (const abstract_object_pointert &other) const
 Helper function for base meet. More...
 
bool should_use_base_meet (const abstract_object_pointert &other) const
 Helper function to decide if base meet implementation should be used. More...
 
void set_top ()
 
void set_not_top ()
 
void set_not_bottom ()
 

Protected Attributes

CLONE abstract_object_pointert child_abstract_object
 

Additional Inherited Members

- Public Types inherited from abstract_objectt
typedef std::set< goto_programt::const_targettlocationst
 
typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hashshared_mapt
 
- Static Public Member Functions inherited from abstract_objectt
static void dump_map (std::ostream out, const shared_mapt &m)
 
static void dump_map_diff (std::ostream out, const shared_mapt &m1, const shared_mapt &m2)
 Dump all elements in m1 that are different or missing in m2. More...
 
static abstract_object_pointert merge (abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
 Clones the first parameter and merges it with the second. More...
 
static abstract_object_pointert merge (abstract_object_pointert op1, abstract_object_pointert op2)
 
static abstract_object_pointert meet (abstract_object_pointert op1, abstract_object_pointert op2, bool &out_modifications)
 Interface method for the meet operation. More...
 
- Protected Types inherited from abstract_objectt
template<class T >
using internal_sharing_ptrt = std::shared_ptr< T >
 
typedef internal_sharing_ptrt< class abstract_objecttinternal_abstract_object_pointert
 

Detailed Description

Definition at line 21 of file context_abstract_object.h.

Constructor & Destructor Documentation

◆ context_abstract_objectt() [1/3]

context_abstract_objectt::context_abstract_objectt ( const abstract_object_pointert  child,
const typet type 
)
inlineexplicit

Definition at line 26 of file context_abstract_object.h.

◆ context_abstract_objectt() [2/3]

context_abstract_objectt::context_abstract_objectt ( const abstract_object_pointert  child,
const typet type,
bool  top,
bool  bottom 
)
inline

Definition at line 34 of file context_abstract_object.h.

◆ context_abstract_objectt() [3/3]

context_abstract_objectt::context_abstract_objectt ( const abstract_object_pointert  child,
const exprt expr,
const abstract_environmentt environment,
const namespacet ns 
)
inlineexplicit

Definition at line 44 of file context_abstract_object.h.

◆ ~context_abstract_objectt()

virtual context_abstract_objectt::~context_abstract_objectt ( )
inlinevirtual

Definition at line 54 of file context_abstract_object.h.

Member Function Documentation

◆ expression_transform()

abstract_object_pointert context_abstract_objectt::expression_transform ( const exprt expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt environment,
const namespacet ns 
) const
overridevirtual

Try to resolve an expression with the maximum level of precision available.

Parameters
exprthe expression to evaluate and find the result of. This will be the symbol referred to be op0()
operandsthe operands to use instead of expr.operands()
environmentthe abstract environment in which to resolve 'expr'
nsthe current namespace
Returns
the resolved expression

Reimplemented from abstract_objectt.

Definition at line 86 of file context_abstract_object.cpp.

◆ get_child()

abstract_object_pointert context_abstract_objectt::get_child ( ) const

Definition at line 11 of file context_abstract_object.cpp.

◆ get_statistics()

void context_abstract_objectt::get_statistics ( abstract_object_statisticst statistics,
abstract_object_visitedt visited,
const abstract_environmentt env,
const namespacet ns 
) const
overridevirtual

Reimplemented from abstract_objectt.

Definition at line 153 of file context_abstract_object.cpp.

◆ has_been_modified()

bool context_abstract_objectt::has_been_modified ( const abstract_object_pointert  before) const
overrideprotectedvirtual

Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state.

Parameters
beforeThe abstract_object_pointert to use as a reference to compare against
Returns
true if 'this' is considered to have been modified in comparison to 'before', false otherwise.

Reimplemented from abstract_objectt.

Reimplemented in write_location_contextt, and data_dependency_contextt.

Definition at line 135 of file context_abstract_object.cpp.

◆ is_bottom()

bool context_abstract_objectt::is_bottom ( ) const
inlineoverridevirtual

Find out if the abstract object is bottom.

Returns
Returns true if the abstract object is representing the bottom.

Reimplemented from abstract_objectt.

Definition at line 68 of file context_abstract_object.h.

◆ is_top()

bool context_abstract_objectt::is_top ( ) const
inlineoverridevirtual

Find out if the abstract object is top.

Returns
Returns true if the abstract object is representing the top (i.e. we don't know anything about the value).

Reimplemented from abstract_objectt.

Definition at line 63 of file context_abstract_object.h.

◆ output()

void context_abstract_objectt::output ( std::ostream &  out,
const class ai_baset ai,
const namespacet ns 
) const
overridevirtual

Output a representation of the value of this abstract object.

Parameters
outthe stream to write to
aithe abstract interpreter that contains the abstract domain (that contains the object ... )
nsthe current namespace

Reimplemented from abstract_objectt.

Reimplemented in write_location_contextt, and data_dependency_contextt.

Definition at line 119 of file context_abstract_object.cpp.

◆ set_child()

void context_abstract_objectt::set_child ( const abstract_object_pointert child)
protected

Definition at line 16 of file context_abstract_object.cpp.

◆ set_not_top_internal()

void context_abstract_objectt::set_not_top_internal ( )
overrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 27 of file context_abstract_object.cpp.

◆ set_top_internal()

void context_abstract_objectt::set_top_internal ( )
overrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 21 of file context_abstract_object.cpp.

◆ to_constant()

exprt context_abstract_objectt::to_constant ( ) const
inlineoverridevirtual

Converts to a constant expression if possible.

Returns
Returns an exprt representing the value if the value is known and constant. Otherwise returns the nil expression

If abstract element represents a single value, then that value, otherwise nil. E.G. if it is an interval then this will be x if it is [x,x] This is the (sort of) dual to the constant_exprt constructor that allows an object to be built from a value.

Reimplemented from abstract_objectt.

Definition at line 73 of file context_abstract_object.h.

◆ type()

const typet& context_abstract_objectt::type ( ) const
inlineoverridevirtual

Get the real type of the variable this abstract object is representing.

Returns
The program type this abstract object represents

Reimplemented from abstract_objectt.

Definition at line 58 of file context_abstract_object.h.

◆ unwrap_context()

abstract_object_pointert context_abstract_objectt::unwrap_context ( ) const
overridevirtual

Reimplemented from abstract_objectt.

Definition at line 148 of file context_abstract_object.cpp.

◆ write()

abstract_object_pointert context_abstract_objectt::write ( abstract_environmentt environment,
const namespacet ns,
const std::stack< exprt > &  stack,
const exprt specifier,
const abstract_object_pointert value,
bool  merging_write 
) const
overrideprotectedvirtual

A helper function to evaluate writing to a component of an abstract object.

More precise abstractions may override this to update what they are storing for a specific component.

Parameters
environmentthe abstract environment
nsthe current namespace
stackthe remaining stack of expressions on the LHS to evaluate
specifierthe expression uses to access a specific component
valuethe value we are trying to write to the component
merging_writeif true, this and all future writes will be merged with the current value
Returns
the abstract_objectt representing the result of writing to a specific component.

Reimplemented from abstract_objectt.

Reimplemented in write_location_contextt, and data_dependency_contextt.

Definition at line 49 of file context_abstract_object.cpp.

Member Data Documentation

◆ child_abstract_object

CLONE abstract_object_pointert context_abstract_objectt::child_abstract_object
protected

Definition at line 101 of file context_abstract_object.h.


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