CBMC
|
An abstract version of a program environment. More...
#include "abstract_object.h"
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) |
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.
using variable_sensitivity_object_factory_ptrt = std::shared_ptr<variable_sensitivity_object_factoryt> |
Definition at line 27 of file abstract_environment.h.
|
strong |
Enumerator | |
---|---|
no | |
could_widen |
Definition at line 30 of file abstract_environment.h.
bool is_ptr_comparison | ( | const exprt & | expr | ) |
Definition at line 70 of file abstract_environment.cpp.
bool is_ptr_diff | ( | const exprt & | expr | ) |
Definition at line 63 of file abstract_environment.cpp.
exprt simplify_vsd_expr | ( | exprt | src, |
const namespacet & | ns | ||
) |