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 
19  const goto_functiont &goto_function,
20  std::set<irep_idt> &dest)
21 {
22  goto_function.body.get_decl_identifiers(dest);
23 
24  // add parameters
25  for(const auto &identifier : goto_function.parameter_identifiers)
26  {
27  if(!identifier.empty())
28  dest.insert(identifier);
29  }
30 }
31 
37  const
38 {
39  for(const auto &identifier : parameter_identifiers)
40  {
41  DATA_CHECK(
42  vm,
43  identifier.empty() || ns.lookup(identifier).is_parameter,
44  "parameter should be marked 'is_parameter' in the symbol table");
45  }
46 
47  // function body must end with an END_FUNCTION instruction
48  if(body_available())
49  {
50  DATA_CHECK(
51  vm,
52  body.instructions.back().is_end_function(),
53  "last instruction should be of end function type");
54  }
55 
56  body.validate(ns, vm);
57 }
goto_functiont::body
goto_programt body
Definition: goto_function.h:29
DATA_CHECK
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition: validate.h:22
goto_functiont::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto function is well-formed.
Definition: goto_function.cpp:36
goto_programt::get_decl_identifiers
void get_decl_identifiers(decl_identifierst &decl_identifiers) const
get the variables in decl statements
Definition: goto_program.cpp:230
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:141
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:38
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_functiont
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
goto_programt::validate
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:813
get_local_identifiers
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...
Definition: goto_function.cpp:18
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:569
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
goto_function.h
Goto Function.