CBMC: /home/runner/work/cbmc/cbmc/src/analyses/locals.cpp Source File

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().identifier());

24 }

25

26 locals.insert(

27 goto_function.parameter_identifiers.begin(),

28 goto_function.parameter_identifiers.end());

29}

31 void localst::output(std::ostream &out) const

32{

33 for(const auto &local : locals)

34 out << local << "\n";

35}

goto_functiont

A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...

Definition goto_function.h:24

goto_functiont::body

goto_programt body

Definition goto_function.h:26

goto_functiont::parameter_identifiers

parameter_identifierst parameter_identifiers

The identifiers of the parameters of this function.

Definition goto_function.h:33

goto_programt::instructions

instructionst instructions

The list of instructions in the goto program.

Definition goto_program.h:621

localst::build

void build(const goto_functiont &goto_function)

Definition locals.cpp:18

localst::output

void output(std::ostream &out) const

Definition locals.cpp:31

localst::locals

locals_sett locals

Definition locals.h:43

goto_function.h

Goto Function.

locals.h

Local variables whose address is taken.