CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
two_value_union_abstract_object.h
Go to the documentation of this file.
1/*******************************************************************\
2
3 Module: analyses variable-sensitivity
4
5 Author: Fotis Koutoulakis, fotis.koutoulakis@diffblue.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_ANALYSES_VARIABLE_SENSITIVITY_UNION_ABSTRACT_OBJECT_H
13#define CPROVER_ANALYSES_VARIABLE_SENSITIVITY_UNION_ABSTRACT_OBJECT_H
14
16
18 two_value_union_abstract_objectt,
19 union_aggregate_typet>
20{
21public:
26
37
44 const exprt &expr,
45 const abstract_environmentt &environment,
46 const namespacet &ns)
47 : abstract_aggregate_baset(expr, environment, ns)
48 {
49 }
50
51protected:
56 const namespacet &ns) const override
57 {
58 }
59};
60#endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_UNION_ABSTRACT_OBJECT_H
Common behaviour for abstract objects modelling aggregate values - arrays, structs,...
std::set< abstract_object_pointert > abstract_object_visitedt
virtual const typet & type() const
Get the real type of the variable this abstract object is representing.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
two_value_union_abstract_objectt(const exprt &expr, const abstract_environmentt &environment, const namespacet &ns)
void statistics(abstract_object_statisticst &statistics, abstract_object_visitedt &visited, const abstract_environmentt &env, const namespacet &ns) const override
abstract_aggregate_objectt< two_value_union_abstract_objectt, union_aggregate_typet > abstract_aggregate_baset
two_value_union_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.
The type of an expression, extends irept.
Definition type.h:29