abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual variables in the general non-relational domain. More...

#include <memory>
#include <set>
#include <stack>
#include <goto-programs/goto_program.h>
#include <util/sharing_map.h>

Include dependency graph for abstract_object.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	abstract_objectt

struct	abstract_objectt::combine_result
	Clones the first parameter and merges it with the second. More...

struct	abstract_objectt::abstract_object_visitort
	Pure virtual interface required of a client that can apply a copy-on-write operation to a given abstract_object_pointert. More...

struct	abstract_hashert

struct	abstract_equalert

Macros
#define	CLONE

Typedefs
template<class T >
using	sharing_ptrt = std::shared_ptr< const T >
	Merge is designed to allow different abstractions to be merged gracefully. More...

typedef sharing_ptrt< class abstract_objectt >	abstract_object_pointert

using	abstract_object_visitedt = std::set< abstract_object_pointert >

Detailed Description

abstract_objectt is the top of the inheritance heirarchy of objects used to represent individual variables in the general non-relational domain.

It is a two element abstraction (i.e. it is either top or bottom). Within the hierarchy of objects under it, child classes are more precise abstractions (the converse doesn't hold to avoid diamonds and inheriting unnecessary fields). Thus the common parent of two classes is an abstraction capable of representing both. This is important for understanding merge.

These objects are intended to be used in a copy-on-write style, which is why their interface differs a bit from ai_domain_baset's modify-in-place style of interface.

Although these can represent bottom (this variable cannot take any value) it is not common for them to do so.

Definition in file abstract_object.h.

Macro Definition Documentation

◆ CLONE

#define CLONE

Value:

  internal_abstract_object_pointert mutable_clone() const override             \
  {                                                                            \
    typedef std::remove_const<                                                 \
      std::remove_reference<decltype(*this)>::type>::type current_typet;       \
    return internal_abstract_object_pointert(new current_typet(*this));        \
  }

Definition at line 41 of file abstract_object.h.

Typedef Documentation

◆ abstract_object_pointert

typedef sharing_ptrt<class abstract_objectt> abstract_object_pointert

Definition at line 69 of file abstract_object.h.

◆ abstract_object_visitedt

using abstract_object_visitedt = std::set<abstract_object_pointert>

Definition at line 70 of file abstract_object.h.

◆ sharing_ptrt

template<class T >

using sharing_ptrt = std::shared_ptr<const T>

Merge is designed to allow different abstractions to be merged gracefully.

There are two real use-cases for this:

Having different abstractions for the variable in different parts of the program.
Allowing different domains to write to ambiguous locations for example, if a stores multiple values (maybe one per location) with a constant for each, i does not represent one single value (top, non-unit interval, etc.) and v is something other than constant, then a[i] = v will cause this to happen.

To handle this, merge is dispatched to the first abstract object being merged, which switches based on the type of the other object. If it can merge then it merges, otherwise it calls the parent merge.

Definition at line 67 of file abstract_object.h.

Classes

Macros