CBMC
Loading...
Searching...
No Matches
Public Member Functions | Protected Member Functions | Static Protected Member Functions | List of all members
abstract_aggregate_objectt< aggregate_typet, aggregate_traitst > Class Template Referenceabstract

#include <abstract_aggregate_object.h>

+ Inheritance diagram for abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >:
[フレーム]
[legend]
+ Collaboration diagram for abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >:
[フレーム]
[legend]

Public Member Functions

  abstract_aggregate_objectt (const typet &type, bool tp, bool bttm)
 
  abstract_aggregate_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.
 
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.
 
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_objectt
  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.
 
  abstract_objectt (const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
  Construct an abstract object from the expression.
 
virtual  ~abstract_objectt ()
 
virtual const typet &  type () const
  Get the real type of the variable this abstract object is representing.
 
virtual bool  is_top () const
  Find out if the abstract object is top.
 
virtual bool  is_bottom () const
  Find out if the abstract object is bottom.
 
virtual bool  verify () const
  Verify the internal structure of an abstract_object is correct.
 
virtual exprt  to_constant () const
  Converts to a constant expression if possible.
 
exprt  to_predicate (const exprt &name) const
  Converts to an invariant expression.
 
virtual void  output (std::ostream &out, const class ai_baset &ai, const namespacet &ns) const
  Print the value of the abstract object.
 
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.
 
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}.
 
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
 
virtual exprt  to_predicate_internal (const exprt &name) const
  to_predicate implementation - derived classes will override
 

Protected Member Functions

virtual abstract_object_pointert  read_component (const abstract_environmentt &environment, const exprt &expr, const namespacet &ns) const
 
virtual 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
 
virtual void  statistics (abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const =0
 
- 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.
 
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.
 
virtual abstract_object_pointert  merge (const abstract_object_pointert &other, const widen_modet &widen_mode) const
  Create a new abstract object that is the result of the merge, unless the object would be unchanged, then would return itself.
 
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 ()
 

Static Protected Member Functions

template<class keyt , typename hash >
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)
 

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

template<class aggregate_typet, class aggregate_traitst>
class abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >

Definition at line 29 of file abstract_aggregate_object.h.

Constructor & Destructor Documentation

◆  abstract_aggregate_objectt() [1/2]

abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::abstract_aggregate_objectt ( const typet &  type,
bool  tp,
bool  bttm 
)
inline

Definition at line 33 of file abstract_aggregate_object.h.

◆  abstract_aggregate_objectt() [2/2]

abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::abstract_aggregate_objectt ( const exprt &  expr,
const abstract_environmentt &  environment,
const namespacet &  ns 
)
inline

Definition at line 45 of file abstract_aggregate_object.h.

Member Function Documentation

◆  expression_transform()

abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::expression_transform ( const exprt &  expr,
const std::vector< abstract_object_pointert > &  operands,
const abstract_environmentt &  environment,
const namespacet &  ns 
) const
inlineoverridevirtual

Interface for transforms.

Parameters
expr the expression to evaluate and find the result of it. This will be the symbol referred to be op0()
operands an abstract_object (pointer) that represent the possible values of each operand
environment the abstract environment in which the expression is being evaluated
ns the current variable namespace
Returns
Returns the abstract_object representing the result of this expression to the maximum precision available.

To try and resolve different expressions with the maximum level of precision available.

Reimplemented from abstract_objectt.

Definition at line 62 of file abstract_aggregate_object.h.

◆  get_statistics()

void abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::get_statistics ( abstract_object_statisticst &  statistics,
abstract_object_visitedt &  visited,
const abstract_environmentt &  env,
const namespacet &  ns 
) const
inlineoverridevirtual

Reimplemented from abstract_objectt.

Definition at line 87 of file abstract_aggregate_object.h.

◆  merge_shared_maps()

template<class keyt , typename hash >
static bool abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::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 
)
inlinestaticprotected

Definition at line 138 of file abstract_aggregate_object.h.

◆  read_component()

virtual abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::read_component ( const abstract_environmentt &  environment,
const exprt &  expr,
const namespacet &  ns 
) const
inlineprotectedvirtual

Reimplemented in full_array_abstract_objectt, and full_struct_abstract_objectt.

Definition at line 99 of file abstract_aggregate_object.h.

◆  statistics()

virtual void abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::statistics ( abstract_object_statisticst &  statistics,
abstract_object_visitedt &  visited,
const abstract_environmentt &  env,
const namespacet &  ns 
) const
protectedpure virtual

Implemented in full_array_abstract_objectt, full_struct_abstract_objectt, two_value_array_abstract_objectt, two_value_struct_abstract_objectt, and two_value_union_abstract_objectt.

◆  write()

abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::write ( abstract_environmentt &  environment,
const namespacet &  ns,
const std::stack< exprt > &  stack,
const exprt &  specifier,
const abstract_object_pointert &  value,
bool  merging_write 
) const
inlineoverridevirtual

A helper function to evaluate writing to a component of an abstract object.

More precise abstractions may override this to update what they are storing for a specific component.

Parameters
environment the abstract environment
ns the current namespace
stack the remaining stack of expressions on the LHS to evaluate
specifier the expression uses to access a specific component
value the value we are trying to write to the component
merging_write if true, this and all future writes will be merged with the current value
Returns
the abstract_objectt representing the result of writing to a specific component.

Reimplemented from abstract_objectt.

Definition at line 75 of file abstract_aggregate_object.h.

◆  write_component()

virtual abstract_object_pointert abstract_aggregate_objectt< aggregate_typet, aggregate_traitst >::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
inlineprotectedvirtual

Reimplemented in full_array_abstract_objectt, and full_struct_abstract_objectt.

Definition at line 113 of file abstract_aggregate_object.h.

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

AltStyle によって変換されたページ (->オリジナル) /