cprover
value_set_domain_fivrns.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set Domain (Flow Insensitive, Validity Regions)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVRNS_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVRNS_H
15
17
18#include "value_set_fivrns.h"
19
22{
23public:
25
26 // overloading
27
28 virtual void output(
29 const namespacet &ns,
30 std::ostream &out) const
31 {
32 value_set.output(ns, out);
33 }
34
35 virtual void initialize(
36 const namespacet &)
37 {
39 }
40
41 virtual bool transform(
42 const namespacet &ns,
43 const irep_idt &function_from,
44 locationt from_l,
45 const irep_idt &function_to,
46 locationt to_l);
47
48 virtual void get_reference_set(
49 const namespacet &ns,
50 const exprt &expr,
51 expr_sett &expr_set)
52 {
53 value_set.get_reference_set(expr, expr_set, ns);
54 }
55
56 virtual void clear(void)
57 {
59 }
60};
61
62#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVRNS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Base class for all expressions.
Definition: expr.h:54
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
virtual void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set)
virtual void initialize(const namespacet &)
virtual bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l)
virtual void output(const namespacet &ns, std::ostream &out) const
void output(const namespacet &ns, std::ostream &out) const
void get_reference_set(const exprt &expr, expr_sett &expr_set, const namespacet &ns) const
Flow Insensitive Static Analysis.
Value Set (Flow Insensitive, Validity Regions)