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}.

virtual abstract_object_pointert write_location_context (const locationt &location) const

Update the write location context for an abstract object.

virtual abstract_object_pointert merge_location_context (const locationt &location) const

Update the merge location context for an abstract object.

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.

virtual size_t internal_hash () const

virtual bool internal_equality (const abstract_object_pointert &other) const

Protected Member Functions

abstract_object_pointert merge (const abstract_object_pointert &op1, const widen_modet &widen_mode) const override

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

internal_abstract_object_pointert mutable_clone () const override

exprt to_predicate_internal (const exprt &name) const override

to_predicate implementation - derived classes will override

- Protected Member Functions inherited from abstract_objectt

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.

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.

abstract_object_pointert abstract_object_meet (const abstract_object_pointert &other) const

Helper function for base meet.

bool should_use_base_meet (const abstract_object_pointert &other) const

Helper function to decide if base meet implementation should be used.

void set_top ()

void set_not_top ()

void set_not_bottom ()

Private Types

typedef sharing_ptrt< constant_pointer_abstract_objectt > constant_pointer_abstract_pointert

Private Member Functions

bool same_target (abstract_object_pointert other) const

exprt offset () const

exprt offset_from (abstract_object_pointert other) const

abstract_object_pointert merge_constant_pointers (const constant_pointer_abstract_pointert &other, const widen_modet &widen_mode) const

Merges two constant pointers.

Private Attributes

write_stackt value_stack

Additional Inherited Members

- Public Types inherited from abstract_objectt

typedef goto_programt::const_targett locationt

typedef sharing_mapt< irep_idt, abstract_object_pointert, false, irep_id_hash > shared_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.

static combine_result merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const locationt &merge_location, const widen_modet &widen_mode)

static combine_result merge (const abstract_object_pointert &op1, const abstract_object_pointert &op2, const widen_modet &widen_mode)

static combine_result meet (const abstract_object_pointert &op1, const abstract_object_pointert &op2)

Interface method for the meet operation.

- Protected Types inherited from abstract_objectt

template<class T >

using internal_sharing_ptrt = std::shared_ptr< T >

typedef internal_sharing_ptrt< class abstract_objectt > internal_abstract_object_pointert

Detailed Description

Definition at line 19 of file constant_pointer_abstract_object.h.

Member Typedef Documentation

◆ constant_pointer_abstract_pointert

typedef sharing_ptrt<constant_pointer_abstract_objectt> constant_pointer_abstract_objectt::constant_pointer_abstract_pointert

private

Definition at line 23 of file constant_pointer_abstract_object.h.

Constructor & Destructor Documentation

◆ constant_pointer_abstract_objectt() [1/3]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const typet & type,

bool top,

bool bottom

)

Parameters: type the type the abstract_object is representing

top is the abstract_object starting as top

bottom is 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 22 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [2/3]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const typet & type,

const constant_pointer_abstract_objectt & old

)

Definition at line 31 of file constant_pointer_abstract_object.cpp.

◆ constant_pointer_abstract_objectt() [3/3]

constant_pointer_abstract_objectt::constant_pointer_abstract_objectt ( const exprt & expr,

const abstract_environmentt & environment,

const namespacet & ns

)

Parameters: expr the expression to use as the starting pointer for an abstract object

environment the environment in which we evaluate expr

ns the current namespace

Definition at line 39 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 286 of file constant_pointer_abstract_object.cpp.

◆ merge()

abstract_object_pointert constant_pointer_abstract_objectt::merge ( const abstract_object_pointert & op1,

const widen_modet & widen_mode

) 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: op1 the pointer being merged

widen_mode Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 57 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 widen_modet & widen_mode

) const

private

Merges two constant pointers.

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

Parameters: other the pointer being merged

widen_mode Indicates if this is a widening merge

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 112 of file constant_pointer_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert constant_pointer_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 143 of file constant_pointer_abstract_object.h.

◆ offset()

exprt constant_pointer_abstract_objectt::offset ( ) const

private

Definition at line 90 of file constant_pointer_abstract_object.cpp.

◆ offset_from()

exprt constant_pointer_abstract_objectt::offset_from ( abstract_object_pointert other ) const

private

Definition at line 97 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: out the stream to write to

ai the domain in which this object appears given as ai_baset so that the interface is the same across all domains

ns the current namespace

Definition at line 142 of file constant_pointer_abstract_object.cpp.

◆ ptr_comparison_expr()

exprt constant_pointer_abstract_objectt::ptr_comparison_expr ( const exprt & expr,

const std::vector< abstract_object_pointert > & operands,

const abstract_environmentt & environment,

const namespacet & ns

) const

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 353 of file constant_pointer_abstract_object.cpp.

◆ ptr_diff()

abstract_object_pointert constant_pointer_abstract_objectt::ptr_diff ( const exprt & expr,

const std::vector< abstract_object_pointert > & operands,

const abstract_environmentt & environment,

const namespacet & ns

) const

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 301 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: env the environment

ns the namespace

Returns: An abstract object representing the value this pointer is pointing to

Implements abstract_pointer_objectt.

Definition at line 189 of file constant_pointer_abstract_object.cpp.

◆ same_target()

bool constant_pointer_abstract_objectt::same_target ( abstract_object_pointert other ) const

private

Definition at line 69 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 128 of file constant_pointer_abstract_object.cpp.

◆ to_predicate_internal()

exprt constant_pointer_abstract_objectt::to_predicate_internal ( const exprt & name ) const

overrideprotectedvirtual

to_predicate implementation - derived classes will override

Parameters: name - the variable name to substitute into the expression

Returns: Returns an exprt representing the object as an invariant.

Reimplemented from abstract_objectt.

Definition at line 387 of file constant_pointer_abstract_object.cpp.

◆ typecast()

abstract_object_pointert constant_pointer_abstract_objectt::typecast ( const typet & new_type,

const abstract_environmentt & environment,

const namespacet & ns

) const

overridevirtual

Implements abstract_pointer_objectt.

Definition at line 257 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: environment the environment

ns the namespace

stack the remaining stack

value the value to write to the dereferenced pointer

merging_write is 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.

Implements abstract_pointer_objectt.

Definition at line 207 of file constant_pointer_abstract_object.cpp.

Member Data Documentation

◆ value_stack

write_stackt constant_pointer_abstract_objectt::value_stack

private

Definition at line 165 of file constant_pointer_abstract_object.h.

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

/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/constant_pointer_abstract_object.h
/home/runner/work/cbmc/cbmc/src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp