CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
value_set_domain_fi.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FI_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FI_H
15
17
18#include "value_set_fi.h"
19
21{
22public:
24
25 // overloading
26
27// virtual bool merge(const value_set_domain_fit &other)
28// {
29// return value_set.make_union(other.value_set);
30// }
31
32 void output(const namespacet &ns, std::ostream &out) const override
33 {
34 value_set.output(ns, out);
35 }
36
37 void initialize(const namespacet &) override
38 {
40 }
41
42 bool transform(
43 const namespacet &ns,
46 const irep_idt &function_to,
47 locationt to_l) override;
48
50 const namespacet &ns,
51 const exprt &expr,
52 expr_sett &expr_set) override
53 {
54 value_set.get_reference_set(expr, expr_set, ns);
55 }
56
57 void clear(void) override
58 {
60 }
61};
62
63#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FI_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
Base class for all expressions.
Definition expr.h:56
std::unordered_set< exprt, irep_hash > expr_sett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
void clear(void) override
void initialize(const namespacet &) override
bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set) override
void output(const namespacet &ns, std::ostream &out) const override
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
void output(const namespacet &ns, std::ostream &out) const
Flow Insensitive Static Analysis.
Value Set (Flow Insensitive, Sharing)