cprover
Loading...
Searching...
No Matches
value_set_domain_fivr.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Value Set (Flow Insensitive, Sharing, Validity Regions)
4
5Author: Daniel Kroening, kroening@kroening.com
6 CM Wintersteiger
7
8\*******************************************************************/
9
12
13#ifndef CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVR_H
14#define CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVR_H
15
17
18#include "value_set_fivr.h"
19
21{
22public:
24
25 // overloading
26
27 void output(const namespacet &ns, std::ostream &out) const override
28 {
29 value_set.output(ns, out);
30 }
31
32 void initialize(const namespacet &) override
33 {
35 }
36
38 const namespacet &ns,
39 const irep_idt &function_from,
40 locationt from_l,
41 const irep_idt &function_to,
42 locationt to_l) override;
43
45 const namespacet &ns,
46 const exprt &expr,
47 expr_sett &expr_set) override
48 {
49 value_set.get_reference_set(expr, expr_set, ns);
50 }
51
52 void clear(void) override
53 {
55 }
56};
57
58#endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_DOMAIN_FIVR_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
void initialize(const namespacet &) override
void get_reference_set(const namespacet &ns, const exprt &expr, expr_sett &expr_set) override
void clear(void) override
void output(const namespacet &ns, std::ostream &out) const override
bool transform(const namespacet &ns, const irep_idt &function_from, locationt from_l, const irep_idt &function_to, locationt to_l) override
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, Sharing, Validity Regions)