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  // function body must end with an END_FUNCTION instruction
40  if(body_available())
41  {
42  DATA_CHECK(
43  vm,
44  body.instructions.back().is_end_function(),
45  "last instruction should be of end function type");
46  }
47 
48  body.validate(ns, vm);
49 }
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
Definition: goto_function.h:27
goto_programt body
Definition: goto_function.h:29
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:36
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:38
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
void validate(const namespacet &ns, const validation_modet vm) const
Check that the goto program is well-formed.
Definition: goto_program.h:800
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:92
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.
#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