cprover
points_to.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-sensitive, location-insensitive points-to analysis
4
5Author: Daniel Kroening, kroening@kroening.com
6
7\*******************************************************************/
8
11
12#ifndef CPROVER_GOTO_INSTRUMENT_POINTS_TO_H
13#define CPROVER_GOTO_INSTRUMENT_POINTS_TO_H
14
15#include <iosfwd>
16
18#include <goto-programs/cfg.h>
19
20#include "object_id.h"
21
23{
24public:
26 {
27 }
28
29 void operator()(goto_modelt &goto_model)
30 {
31 // build the CFG data structure
32 cfg(goto_model.goto_functions);
33
34 // iterate
35 fixedpoint();
36 }
37
38 const object_id_sett &operator[](const object_idt &object_id)
39 {
40 value_mapt::const_iterator it=value_map.find(object_id);
41 if(it!=value_map.end())
42 return it->second;
43 return empty_set;
44 }
45
46 void output(std::ostream &out) const;
47
48protected:
51
52 typedef std::map<object_idt, object_id_sett> value_mapt;
54
55 void fixedpoint();
56 bool transform(const cfgt::nodet&);
57
59};
60
61inline std::ostream &operator<<(
62 std::ostream &out,
63 const points_tot &points_to)
64{
65 points_to.output(out);
66 return out;
67}
68
69#endif // CPROVER_GOTO_INSTRUMENT_POINTS_TO_H
Control Flow Graph.
base_grapht::nodet nodet
Definition: cfg.h:92
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
void fixedpoint()
Definition: points_to.cpp:14
bool transform(const cfgt::nodet &)
Definition: points_to.cpp:54
std::map< object_idt, object_id_sett > value_mapt
Definition: points_to.h:52
cfgt cfg
Definition: points_to.h:50
void operator()(goto_modelt &goto_model)
Definition: points_to.h:29
cfg_baset< empty_cfg_nodet > cfgt
Definition: points_to.h:49
const object_id_sett & operator[](const object_idt &object_id)
Definition: points_to.h:38
const object_id_sett empty_set
Definition: points_to.h:58
value_mapt value_map
Definition: points_to.h:53
points_tot()
Definition: points_to.h:25
void output(std::ostream &out) const
Definition: points_to.cpp:33
Symbol Table + CFG.
Object Identifiers.
std::set< object_idt > object_id_sett
Definition: object_id.h:58
std::ostream & operator<<(std::ostream &out, const points_tot &points_to)
Definition: points_to.h:61