CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
goto_function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: A GOTO Function
4
5Author: Daniel Kroening
6
7Date: May 2018
8
9\*******************************************************************/
10
13
14#include "goto_function.h"
15
16#include <util/namespace.h>
17#include <util/symbol.h>
18
22 const goto_functiont &goto_function,
23 std::set<irep_idt> &dest)
24{
25 goto_function.body.get_decl_identifiers(dest);
26
27 // add parameters
28 for(const auto &identifier : goto_function.parameter_identifiers)
29 {
30 if(!identifier.empty())
31 dest.insert(identifier);
32 }
33}
34
40 const
41{
42 for(const auto &identifier : parameter_identifiers)
43 {
45 vm,
46 identifier.empty() || ns.lookup(identifier).is_parameter,
47 "parameter should be marked 'is_parameter' in the symbol table",
48 "affected parameter: ",
49 identifier);
50 }
51
52 // function body must end with an END_FUNCTION instruction
53 if(body_available())
54 {
56 vm,
57 body.instructions.back().is_end_function(),
58 "last instruction should be of end function type");
59 }
60
61 body.validate(ns, vm);
62}
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.
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
bool body_available() const
instructionst instructions
The list of instructions in the goto program.
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void get_local_identifiers(const goto_functiont &goto_function, std::set< irep_idt > &dest)
Return in dest the identifiers of the local variables declared in the goto_function and the identifie...
Goto Function.
Symbol table entry.
#define DATA_CHECK_WITH_DIAGNOSTICS(vm, condition, message,...)
Definition validate.h:37
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet