cprover
abstract_environment.h File Reference

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

#include <iosfwd>
#include <map>
#include <memory>
#include <stack>
#include <vector>
#include "abstract_object_statistics.h"
#include <analyses/variable-sensitivity/abstract_object.h>
#include <util/sharing_map.h>
#include <util/std_expr.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 >
 

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