CBMC
|
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 | widen_modet { widen_modet::no, widen_modet::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 30 of file abstract_environment.h.
|
strong |
Enumerator | |
---|---|
no | |
could_widen |
Definition at line 32 of file abstract_environment.h.
bool is_ptr_comparison | ( | const exprt & | expr | ) |
Definition at line 67 of file abstract_environment.cpp.
bool is_ptr_diff | ( | const exprt & | expr | ) |
Definition at line 60 of file abstract_environment.cpp.
exprt simplify_vsd_expr | ( | exprt | src, |
const namespacet & | ns | ||
) |