CBMC
locals.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Local variables
4 
5 Author: Daniel Kroening
6 
7 Date: March 2013
8 
9 \*******************************************************************/
10 
13 
14 #include "locals.h"
15 
17 
18 void 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 
31 void 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...
Definition: goto_function.h:24
goto_programt body
Definition: goto_function.h:26
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:33
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
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.