cprover
constant_pointer_abstract_objectt Class Reference

#include <constant_pointer_abstract_object.h>

+ Inheritance diagram for constant_pointer_abstract_objectt:
+ Collaboration diagram for constant_pointer_abstract_objectt:

Public Member Functions

 constant_pointer_abstract_objectt (const typet &type)
 
 constant_pointer_abstract_objectt (const typet &type, bool top, bool bottom)
 
 constant_pointer_abstract_objectt (const constant_pointer_abstract_objectt &old)
 
 constant_pointer_abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 
exprt to_constant () const override
 To try and find a constant expression for this abstract object. More...
 
void output (std::ostream &out, const ai_baset &ai, const namespacet &ns) const override
 Print the value of the pointer. More...
 
abstract_object_pointert read_dereference (const abstract_environmentt &env, const namespacet &ns) const override
 A helper function to dereference a value from a pointer. More...
 
abstract_object_pointert write_dereference (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const abstract_object_pointert &value, bool merging_write) const override
 A helper function to evaluate writing to a pointers value. More...
 
void get_statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
 
- Public Member Functions inherited from abstract_pointer_objectt
 abstract_pointer_objectt (const typet &type)
 
 abstract_pointer_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_pointer_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 
abstract_object_pointert expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const override
 Interface for transforms. More...
 
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...
 
- 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 const typettype () const
 Get the real type of the variable this abstract object is representing. More...
 
virtual bool is_top () const
 Find out if the abstract object is top. More...
 
virtual bool is_bottom () const
 Find out if the abstract object is bottom. More...
 
virtual bool verify () const
 Verify the internal structure of an abstract_object is correct. More...
 
virtual void output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
 Print the value of the abstract object. More...
 
virtual bool has_been_modified (const abstract_object_pointert before) const
 Determine whether 'this' abstract_object has been modified in comparison to a previous 'before' state. 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 unwrap_context () 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

abstract_object_pointert merge (abstract_object_pointert op1) const override
 Set this abstract object to be the result of merging this abstract object. 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...
 
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 ()
 

Private Types

typedef sharing_ptrt< constant_pointer_abstract_objecttconstant_pointer_abstract_pointert
 

Private Member Functions

abstract_object_pointert merge_constant_pointers (const constant_pointer_abstract_pointert &other) const
 Merges two constant pointers. More...
 

Private Attributes

write_stackt value_stack
 

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 19 of file constant_pointer_abstract_object.h.

Member Typedef Documentation

◆ constant_pointer_abstract_pointert

Constructor & Destructor Documentation

◆ constant_pointer_abstract_objectt() [1/4]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const typet type)
explicit
Parameters
typethe type the abstract_object is representing

Definition at line 19 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [2/4]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const typet type,
bool  top,
bool  bottom 
)
Parameters
typethe type the abstract_object is representing
topis the abstract_object starting as top
bottomis the abstract_object starting as bottom

Start the abstract object at either top or bottom or neither Asserts if both top and bottom are true

Definition at line 26 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [3/4]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const constant_pointer_abstract_objectt old)
Parameters
oldthe abstract object to copy from

Definition at line 35 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [4/4]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const exprt expr,
const abstract_environmentt environment,
const namespacet ns 
)
Parameters
exprthe expression to use as the starting pointer for an abstract object
environmentthe environment in which we evaluate expr
nsthe current namespace

Definition at line 41 of file constant_pointer_abstract_object.cpp.

Member Function Documentation

◆ get_statistics()

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

Reimplemented from abstract_pointer_objectt.

Definition at line 222 of file constant_pointer_abstract_object.cpp.

◆ merge()

abstract_object_pointert constant_pointer_abstract_objectt::merge ( abstract_object_pointert  op1) const
overrideprotectedvirtual

Set this abstract object to be the result of merging this abstract object.

This calls the merge_constant_pointers if we are trying to merge a constant pointer we use the constant pointer constant pointer merge

Parameters
op1the pointer being merged
Returns
Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 60 of file constant_pointer_abstract_object.cpp.

◆ merge_constant_pointers()

abstract_object_pointert constant_pointer_abstract_objectt::merge_constant_pointers ( const constant_pointer_abstract_pointert other) const
private

Merges two constant pointers.

If they are pointing at the same value, we merge, otherwise we set to top.

Parameters
otherthe pointer being merged
Returns
Returns a new abstract object that is the result of the merge unless the merge is the same as this abstract object, in which case it returns this.

Definition at line 76 of file constant_pointer_abstract_object.cpp.

◆ output()

void constant_pointer_abstract_objectt::output ( std::ostream &  out,
const ai_baset ai,
const namespacet ns 
) const
override

Print the value of the pointer.

Either NULL if nullpointer or ptr -> ( output of what the pointer is pointing to).

Parameters
outthe stream to write to
aithe domain in which this object appears given as ai_baset so that the interface is the same across all domains
nsthe current namespace

Definition at line 113 of file constant_pointer_abstract_object.cpp.

◆ read_dereference()

abstract_object_pointert constant_pointer_abstract_objectt::read_dereference ( const abstract_environmentt env,
const namespacet ns 
) const
overridevirtual

A helper function to dereference a value from a pointer.

Providing the pointer can only be pointing at one thing, returns an abstract object representing that thing. If null or top will return top.

Parameters
envthe environment
nsthe namespace
Returns
An abstract object representing the value this pointer is pointing to

Reimplemented from abstract_pointer_objectt.

Definition at line 156 of file constant_pointer_abstract_object.cpp.

◆ to_constant()

exprt constant_pointer_abstract_objectt::to_constant ( ) const
overridevirtual

To try and find a constant expression for this abstract object.

Returns
Returns an expression representing the value if it can. Returns a nil expression if it can be more than one value. Returns null_pointer expression if it must be null Returns an address_of_exprt with the value set to the result of to_constant called on whatever abstract object this pointer is pointing to.

Reimplemented from abstract_objectt.

Definition at line 99 of file constant_pointer_abstract_object.cpp.

◆ write_dereference()

abstract_object_pointert constant_pointer_abstract_objectt::write_dereference ( abstract_environmentt environment,
const namespacet ns,
const std::stack< exprt > &  stack,
const abstract_object_pointert value,
bool  merging_write 
) const
overridevirtual

A helper function to evaluate writing to a pointers value.

If the pointer can only be pointing to one element that it overwrites that element (or merges if merging_write) with the new value. If don't know what we are pointing to, we delegate to the parent.

Parameters
environmentthe environment
nsthe namespace
stackthe remaining stack
valuethe value to write to the dereferenced pointer
merging_writeis it a merging write (i.e. we aren't certain we are writing to this particular pointer therefore the value should be merged with whatever is already there or we are certain we are writing to this pointer so therefore the value can be replaced
Returns
A modified abstract object representing this pointer after it has been written to.

Reimplemented from abstract_pointer_objectt.

Definition at line 174 of file constant_pointer_abstract_object.cpp.

Member Data Documentation

◆ value_stack

write_stackt constant_pointer_abstract_objectt::value_stack
private

Definition at line 140 of file constant_pointer_abstract_object.h.


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