CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
locals.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Local variables
4
5Author: Daniel Kroening
6
7Date: March 2013
8
9\*******************************************************************/
10
13
14#include "locals.h"
15
17
18void localst::build(const goto_functiont &goto_function)
19{
20 for(const auto &instruction : goto_function.body.instructions)
21 {
22 if(instruction.is_decl())
23 locals.insert(instruction.decl_symbol().get_identifier());
24 }
25
26 locals.insert(
27 goto_function.parameter_identifiers.begin(),
28 goto_function.parameter_identifiers.end());
29}
30
31void localst::output(std::ostream &out) const
32{
33 for(const auto &local : locals)
34 out << local << "\n";
35}
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_programt body
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
instructionst instructions
The list of instructions in the goto program.
void build(const goto_functiont &goto_function)
Definition locals.cpp:18
void output(std::ostream &out) const
Definition locals.cpp:31
locals_sett locals
Definition locals.h:43
Goto Function.
Local variables whose address is taken.