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

abstract_object_pointert make_top () const

abstract_object_pointert clear_top () const

virtual abstract_object_pointert unwrap_context () const

virtual size_t internal_hash () const

virtual bool internal_equality (const abstract_object_pointert &other) const

Protected Member Functions

internal_abstract_object_pointert mutable_clone () const override

abstract_object_pointert read_component (const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const override

A helper function to read elements from an array.

abstract_object_pointert write_component (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const override

A helper function to evaluate writing to a index of an array.

void statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override

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

Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent merge.

bool verify () const override

To validate that the struct object is in a valid state.

void set_top_internal () override

Perform any additional structural modifications when setting this object to TOP.

- 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_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht > shared_array_mapt

Private Member Functions

abstract_object_pointert read_element (const abstract_environmentt &env, const exprt &expr, const namespacet &ns) const

abstract_object_pointert write_element (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const

abstract_object_pointert write_sub_element (abstract_environmentt &environment, const namespacet &ns, const std::stack< exprt > &stack, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const

abstract_object_pointert write_leaf_element (abstract_environmentt &environment, const namespacet &ns, const exprt &expr, const abstract_object_pointert &value, bool merging_write) const

void map_put (mp_integer index, const abstract_object_pointert &value, bool overrun)

abstract_object_pointert map_find_or_top (mp_integer index, const abstract_environmentt &env, const namespacet &ns) const

abstract_object_pointert get_top_entry (const abstract_environmentt &env, const namespacet &ns) const

Short hand method for creating a top element of the array.

abstract_object_pointert full_array_merge (const full_array_pointert &other, const widen_modet &widen_mode) const

Merges an array into this array.

exprt to_predicate_internal (const exprt &name) const override

to_predicate implementation - derived classes will override

Private Attributes

shared_array_mapt map

Additional Inherited Members

- 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

- Static Protected Member Functions inherited from abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >

static bool merge_shared_maps (const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map1, const sharing_mapt< keyt, abstract_object_pointert, false, hash > &map2, sharing_mapt< keyt, abstract_object_pointert, false, hash > &out_map, const widen_modet &widen_mode)

Detailed Description

Definition at line 23 of file full_array_abstract_object.h.

Member Typedef Documentation

◆ abstract_aggregate_baset

typedef abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet> full_array_abstract_objectt::abstract_aggregate_baset

Definition at line 32 of file full_array_abstract_object.h.

◆ full_array_pointert

typedef sharing_ptrt<full_array_abstract_objectt> const full_array_abstract_objectt::full_array_pointert

Definition at line 28 of file full_array_abstract_object.h.

◆ shared_array_mapt

typedef sharing_mapt< mp_integer, abstract_object_pointert, false, mp_integer_hasht> full_array_abstract_objectt::shared_array_mapt

private

Definition at line 201 of file full_array_abstract_object.h.

Constructor & Destructor Documentation

◆ full_array_abstract_objectt() [1/2]

full_array_abstract_objectt::full_array_abstract_objectt ( 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.

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

Definition at line 67 of file full_array_abstract_object.cpp.

◆ full_array_abstract_objectt() [2/2]

full_array_abstract_objectt::full_array_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 the abstract object is being created in

ns the namespace

Definition at line 76 of file full_array_abstract_object.cpp.

Member Function Documentation

◆ full_array_merge()

abstract_object_pointert full_array_abstract_objectt::full_array_merge ( const full_array_pointert & other,

const widen_modet & widen_mode

) const

private

Merges an array into this array.

Parameters: other The object to merge in

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 123 of file full_array_abstract_object.cpp.

◆ get_top_entry()

abstract_object_pointert full_array_abstract_objectt::get_top_entry ( const abstract_environmentt & env,

const namespacet & ns

) const

private

Short hand method for creating a top element of the array.

Parameters: env the abstract environment

ns the namespace

Returns: An abstract object pointer of type type().subtype() (i.e. the type of the array's values).

Definition at line 387 of file full_array_abstract_object.cpp.

◆ map_find_or_top()

abstract_object_pointert full_array_abstract_objectt::map_find_or_top ( mp_integer index,

const abstract_environmentt & env,

const namespacet & ns

) const

private

Definition at line 376 of file full_array_abstract_object.cpp.

◆ map_put()

void full_array_abstract_objectt::map_put ( mp_integer index,

const abstract_object_pointert & value,

bool overrun

)

private

Definition at line 354 of file full_array_abstract_object.cpp.

◆ merge()

abstract_object_pointert full_array_abstract_objectt::merge ( const abstract_object_pointert & other,

const widen_modet & widen_mode

) const

overrideprotectedvirtual

Tries to do an array/array merge if merging with a constant array If it can't, falls back to parent merge.

Parameters: other The object to merge in

widen_mode Indicates if this is a widening merge

Returns: Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 111 of file full_array_abstract_object.cpp.

◆ merge_location_context()

abstract_object_pointert full_array_abstract_objectt::merge_location_context ( const locationt & location ) const

overridevirtual

Update the merge location context for an abstract object.

Parameters: location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented from abstract_objectt.

Definition at line 401 of file full_array_abstract_object.cpp.

◆ mutable_clone()

internal_abstract_object_pointert full_array_abstract_objectt::mutable_clone ( ) const

inlineoverrideprotectedvirtual

Reimplemented from abstract_objectt.

Definition at line 90 of file full_array_abstract_object.h.

◆ output()

void full_array_abstract_objectt::output ( std::ostream & out,

const ai_baset & ai,

const namespacet & ns

) const

override

the current known value about this object.

For this array we print: { [0] - <output of object at index 0... }

Parameters: out the stream to write to

ai the abstract interpreter that contains the abstract domain (that contains the object ... )

ns the current namespace

Definition at line 148 of file full_array_abstract_object.cpp.

◆ read_component()

abstract_object_pointert full_array_abstract_objectt::read_component ( const abstract_environmentt & env,

const exprt & expr,

const namespacet & ns

) const

overrideprotectedvirtual

A helper function to read elements from an array.

This will return the abstract object stored for that index, or top if we don't know about the specified index. If we can't resolve the index to a constant, we return top

Parameters: env the environment

expr the expression used to access the specific value in the array

ns the namespace

Returns: An abstract object representing the value in the array

Reimplemented from abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 170 of file full_array_abstract_object.cpp.

◆ read_element()

abstract_object_pointert full_array_abstract_objectt::read_element ( const abstract_environmentt & env,

const exprt & expr,

const namespacet & ns

) const

private

Definition at line 208 of file full_array_abstract_object.cpp.

◆ set_top_internal()

void full_array_abstract_objectt::set_top_internal ( )

overrideprotectedvirtual

Perform any additional structural modifications when setting this object to TOP.

Reimplemented from abstract_objectt.

Definition at line 104 of file full_array_abstract_object.cpp.

◆ statistics()

void full_array_abstract_objectt::statistics ( abstract_object_statisticst & statistics,

abstract_object_visitedt & visited,

const abstract_environmentt & env,

const namespacet & ns

) const

overrideprotectedvirtual

Implements abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 440 of file full_array_abstract_object.cpp.

◆ to_predicate_internal()

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

overrideprivatevirtual

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 418 of file full_array_abstract_object.cpp.

◆ verify()

bool full_array_abstract_objectt::verify ( ) const

overrideprotectedvirtual

To validate that the struct object is in a valid state.

This means either it is top or bottom, or if neither of those then there exists something in the map of components. If there is something in the map, then it can't be top or bottom

Returns: Returns true if the struct is valid

Reimplemented from abstract_objectt.

Definition at line 96 of file full_array_abstract_object.cpp.

◆ visit_sub_elements()

abstract_object_pointert full_array_abstract_objectt::visit_sub_elements ( const abstract_object_visitort & visitor ) const

overridevirtual

Apply a visitor operation to all sub elements of this abstract_object.

A sub element might be a member of a struct, or an element of an array, for instance, but this is entirely determined by the particular derived instance of abstract_objectt.

Parameters: visitor an instance of a visitor class that will be applied to all sub elements

Returns: A new abstract_object if it's contents is modifed, or this if no modification is needed

Reimplemented from abstract_objectt.

Definition at line 407 of file full_array_abstract_object.cpp.

◆ write_component()

abstract_object_pointert full_array_abstract_objectt::write_component ( abstract_environmentt & environment,

const namespacet & ns,

const std::stack< exprt > & stack,

const exprt & expr,

const abstract_object_pointert & value,

bool merging_write

) const

overrideprotectedvirtual

A helper function to evaluate writing to a index of an array.

Parameters: environment the abstract environment

ns the namespace

stack the remaining stack of expressions on the LHS to evaluate

expr the expression uses to access a specific index

value the value we are trying to assign to that value in the array

merging_write Should this and all future writes be merged with the current value

Returns: The abstract_object_pointert representing the result of writing to a specific index.

Reimplemented from abstract_aggregate_objectt< full_array_abstract_objectt, array_aggregate_typet >.

Definition at line 188 of file full_array_abstract_object.cpp.

◆ write_element()

abstract_object_pointert full_array_abstract_objectt::write_element ( abstract_environmentt & environment,

const namespacet & ns,

const std::stack< exprt > & stack,

const exprt & expr,

const abstract_object_pointert & value,

bool merging_write

) const

private

Definition at line 236 of file full_array_abstract_object.cpp.

◆ write_leaf_element()

abstract_object_pointert full_array_abstract_objectt::write_leaf_element ( abstract_environmentt & environment,

const namespacet & ns,

const exprt & expr,

const abstract_object_pointert & value,

bool merging_write

) const

private

Definition at line 301 of file full_array_abstract_object.cpp.

◆ write_location_context()

abstract_object_pointert full_array_abstract_objectt::write_location_context ( const locationt & location ) const

overridevirtual

Update the location context for an abstract object.

Parameters: location the location to be updated

Returns: a clone of this abstract object with its location context updated

Reimplemented from abstract_objectt.

Definition at line 395 of file full_array_abstract_object.cpp.

◆ write_sub_element()

abstract_object_pointert full_array_abstract_objectt::write_sub_element ( abstract_environmentt & environment,

const namespacet & ns,

const std::stack< exprt > & stack,

const exprt & expr,

const abstract_object_pointert & value,

bool merging_write

) const

private

Definition at line 257 of file full_array_abstract_object.cpp.

Member Data Documentation

◆ map

shared_array_mapt full_array_abstract_objectt::map

private

Definition at line 203 of file full_array_abstract_object.h.

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

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