CBMC
abstract_environment.h File Reference

An abstract version of a program environment. More...

#include "abstract_object.h"
+ Include dependency graph for abstract_environment.h:
+ This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

class  abstract_environmentt
 

Typedefs

using variable_sensitivity_object_factory_ptrt = std::shared_ptr< variable_sensitivity_object_factoryt >
 

Enumerations

enum class  widen_modet { no , could_widen }
 

Functions

exprt simplify_vsd_expr (exprt src, const namespacet &ns)
 
bool is_ptr_diff (const exprt &expr)
 
bool is_ptr_comparison (const exprt &expr)
 

Detailed Description

An abstract version of a program environment.

Each variable has an abstract object rather than a value. If these are top then they are not explicitly stored so that the memory used is proportional to what is known rather than just the number of variables. Note the use of sharing_mapt is critical for scalability.

Definition in file abstract_environment.h.

Typedef Documentation

◆ variable_sensitivity_object_factory_ptrt

Enumeration Type Documentation

◆ widen_modet

enum widen_modet
strong
Enumerator
no 
could_widen 

Definition at line 30 of file abstract_environment.h.

Function Documentation

◆ is_ptr_comparison()

bool is_ptr_comparison ( const exprt expr)

Definition at line 70 of file abstract_environment.cpp.

◆ is_ptr_diff()

bool is_ptr_diff ( const exprt expr)

Definition at line 63 of file abstract_environment.cpp.

◆ simplify_vsd_expr()

exprt simplify_vsd_expr ( exprt  src,
const namespacet ns 
)