CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
locals.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Local variables whose address is taken
4
5Author: Daniel Kroening
6
7Date: 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
22class goto_functiont;
23
25{
26public:
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
45protected:
46 void build(const goto_functiont &goto_function);
47};
48
49inline 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...
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