cprover
interval_abstract_valuet Class Reference

#include <interval_abstract_value.h>

+ Inheritance diagram for interval_abstract_valuet:
+ Collaboration diagram for interval_abstract_valuet:

Public Member Functions

 interval_abstract_valuet (const typet &t)
 
 interval_abstract_valuet (const typet &t, bool tp, bool bttm)
 
 interval_abstract_valuet (const constant_interval_exprt &e)
 
 interval_abstract_valuet (const exprt &e, const abstract_environmentt &environment, const namespacet &ns)
 
 ~interval_abstract_valuet () override=default
 
index_range_implementation_ptrt index_range_implementation (const namespacet &ns) const override
 
value_range_implementation_ptrt value_range_implementation () const override
 
exprt to_constant () const override
 Converts to a constant expression if possible. More...
 
constant_interval_exprt to_interval () const override
 
size_t internal_hash () const override
 
bool internal_equality (const abstract_object_pointert &other) const override
 
void output (std::ostream &out, const class ai_baset &ai, const class namespacet &ns) const override
 
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_value_objectt
 abstract_value_objectt (const typet &type)
 
 abstract_value_objectt (const typet &type, bool tp, bool bttm)
 
 abstract_value_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
 
index_ranget index_range (const namespacet &ns) const
 
value_ranget value_range () const
 
abstract_object_pointert expression_transform (const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns) const final
 Interface for transforms. 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 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
 A helper function to evaluate writing to a component of an abstract object. 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 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...
 

Protected Member Functions

CLONE abstract_object_pointert merge (abstract_object_pointert other) const override
 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 meet (const abstract_object_pointert &other) const override
 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...
 
- 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 ()
 
void set_not_bottom ()
 

Private Types

using interval_abstract_value_pointert = sharing_ptrt< interval_abstract_valuet >
 

Private Member Functions

abstract_object_pointert merge_intervals (abstract_value_pointert &other) const
 Merge another interval abstract object with this one. More...
 
abstract_object_pointert meet_intervals (interval_abstract_value_pointert other) const
 Meet another interval abstract object with this one. More...
 

Private Attributes

constant_interval_exprt interval
 

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 23 of file interval_abstract_value.h.

Member Typedef Documentation

◆ interval_abstract_value_pointert

Constructor & Destructor Documentation

◆ interval_abstract_valuet() [1/4]

interval_abstract_valuet::interval_abstract_valuet ( const typet t)
explicit

Definition at line 233 of file interval_abstract_value.cpp.

◆ interval_abstract_valuet() [2/4]

interval_abstract_valuet::interval_abstract_valuet ( const typet t,
bool  tp,
bool  bttm 
)

Definition at line 238 of file interval_abstract_value.cpp.

◆ interval_abstract_valuet() [3/4]

interval_abstract_valuet::interval_abstract_valuet ( const constant_interval_exprt e)
explicit

Definition at line 246 of file interval_abstract_value.cpp.

◆ interval_abstract_valuet() [4/4]

interval_abstract_valuet::interval_abstract_valuet ( const exprt e,
const abstract_environmentt environment,
const namespacet ns 
)

Definition at line 252 of file interval_abstract_value.cpp.

◆ ~interval_abstract_valuet()

interval_abstract_valuet::~interval_abstract_valuet ( )
overridedefault

Member Function Documentation

◆ get_statistics()

void interval_abstract_valuet::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 449 of file interval_abstract_value.cpp.

◆ index_range_implementation()

index_range_implementation_ptrt interval_abstract_valuet::index_range_implementation ( const namespacet ns) const
overridevirtual

Implements abstract_value_objectt.

Definition at line 433 of file interval_abstract_value.cpp.

◆ internal_equality()

bool interval_abstract_valuet::internal_equality ( const abstract_object_pointert other) const
overridevirtual

Reimplemented from abstract_objectt.

Definition at line 290 of file interval_abstract_value.cpp.

◆ internal_hash()

size_t interval_abstract_valuet::internal_hash ( ) const
overridevirtual

Reimplemented from abstract_objectt.

Definition at line 285 of file interval_abstract_value.cpp.

◆ meet()

abstract_object_pointert interval_abstract_valuet::meet ( const abstract_object_pointert other) const
overrideprotectedvirtual

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

Parameters
otherpointer to the abstract object to meet
Returns
the resulting abstract object pointer

Reimplemented from abstract_objectt.

Definition at line 386 of file interval_abstract_value.cpp.

◆ meet_intervals()

abstract_object_pointert interval_abstract_valuet::meet_intervals ( interval_abstract_value_pointert  other) const
private

Meet another interval abstract object with this one.

Parameters
otherThe interval abstract object to meet with
Returns
This if the other interval subsumes this, other if this subsumes other. Otherwise, a new interval abstract object with the intersection interval (of this and other)

Definition at line 406 of file interval_abstract_value.cpp.

◆ merge()

abstract_object_pointert interval_abstract_valuet::merge ( abstract_object_pointert  other) const
overrideprotectedvirtual

Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.

Parameters
otherThe object to merge with this
Returns
Returns the result of the merge.

Reimplemented from abstract_objectt.

Definition at line 343 of file interval_abstract_value.cpp.

◆ merge_intervals()

abstract_object_pointert interval_abstract_valuet::merge_intervals ( abstract_value_pointert other) const
private

Merge another interval abstract object with this one.

Parameters
otherThe abstract value object to merge with
Returns
This if the other interval is subsumed by this, other if this is subsumed by other. Otherwise, a new interval abstract object with the smallest interval that subsumes both this and other

Definition at line 365 of file interval_abstract_value.cpp.

◆ output()

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

Definition at line 298 of file interval_abstract_value.cpp.

◆ to_constant()

exprt interval_abstract_valuet::to_constant ( ) const
overridevirtual

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 264 of file interval_abstract_value.cpp.

◆ to_interval()

constant_interval_exprt interval_abstract_valuet::to_interval ( ) const
inlineoverridevirtual

Implements abstract_value_objectt.

Definition at line 44 of file interval_abstract_value.h.

◆ value_range_implementation()

value_range_implementation_ptrt interval_abstract_valuet::value_range_implementation ( ) const
overridevirtual

Implements abstract_value_objectt.

Definition at line 444 of file interval_abstract_value.cpp.

Member Data Documentation

◆ interval

constant_interval_exprt interval_abstract_valuet::interval
private

Definition at line 78 of file interval_abstract_value.h.


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