cprover
goto_function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: A GOTO Function
4 
5 Author: Daniel Kroening
6 
7 Date: May 2018
8 
9 \*******************************************************************/
10 
13 
14 #include "goto_function.h"
15 
16 #include <util/symbol.h>
17 
21  const goto_functiont &goto_function,
22  std::set<irep_idt> &dest)
23 {
24  goto_function.body.get_decl_identifiers(dest);
25 
26  // add parameters
27  for(const auto &identifier : goto_function.parameter_identifiers)
28  {
29  if(!identifier.empty())
30  dest.insert(identifier);
31  }
32 }
33 
39  const
40 {
41  for(const auto &identifier : parameter_identifiers)
42  {
43  DATA_CHECK(
44  vm,
45  identifier.empty() || ns.lookup(identifier).is_parameter,
46  "parameter should be marked 'is_parameter' in the symbol table");
47  }
48 
49  // function body must end with an END_FUNCTION instruction
50  if(body_available())
51  {
52  DATA_CHECK(
53  vm,
54  body.instructions.back().is_end_function(),
55  "last instruction should be of end function type");
56  }
57 
58  body.validate(ns, vm);
59 }
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
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
bool body_available() const
Definition: goto_function.h:35
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:652
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:893
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().
Definition: namespace.cpp:138
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(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
validation_modet