CBMC
locals.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Local variables whose address is taken
4 
5 Author: Daniel Kroening
6 
7 Date: March 2013
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_ANALYSES_LOCALS_H
15 #define CPROVER_ANALYSES_LOCALS_H
16 
17 #include <iosfwd>
18 #include <unordered_set>
19 
20 #include <util/irep.h>
21 
22 class goto_functiont;
23 
24 class localst
25 {
26 public:
27  explicit localst(const goto_functiont &goto_function)
28  {
29  build(goto_function);
30  }
31 
32  void output(std::ostream &out) const;
33 
34  // Returns true for all procedure-local variables,
35  // not including those with static storage duration,
36  // but including the function parameters.
37  bool is_local(const irep_idt &identifier) const
38  {
39  return locals.find(identifier) != locals.end();
40  }
41 
42  typedef std::unordered_set<irep_idt> locals_sett;
44 
45 protected:
46  void build(const goto_functiont &goto_function);
47 };
48 
49 inline std::ostream &operator<<(
50  std::ostream &out, const localst &locals)
51 {
52  locals.output(out);
53  return out;
54 }
55 
56 #endif // CPROVER_ANALYSES_LOCALS_H
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:24
Definition: locals.h:25
void build(const goto_functiont &goto_function)
Definition: locals.cpp:18
localst(const goto_functiont &goto_function)
Definition: locals.h:27
void output(std::ostream &out) const
Definition: locals.cpp:31
bool is_local(const irep_idt &identifier) const
Definition: locals.h:37
locals_sett locals
Definition: locals.h:43
std::unordered_set< irep_idt > locals_sett
Definition: locals.h:42
std::ostream & operator<<(std::ostream &out, const localst &locals)
Definition: locals.h:49