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 
50  find_symbols_sett typetags;
51  find_type_symbols(type, typetags);
52  const symbolt *symbol;
53  for(const auto &identifier : typetags)
54  {
55  DATA_CHECK(
56  vm, !ns.lookup(identifier, symbol), id2string(identifier) + " not found");
57  }
58 
59  // Check that a void function does not contain any RETURN instructions
60  if(to_code_type(type).return_type().id() == ID_empty)
61  {
63  {
64  DATA_CHECK(
65  vm,
66  !instruction->is_return(),
67  "void function should not return a value");
68  }
69  }
70 
71  validate_full_type(type, ns, vm);
72 }
goto_functiont::body
goto_programt body
Definition: goto_function.h:30
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
validate_full_type
void validate_full_type(const typet &type, const namespacet &ns, const validation_modet vm)
Check that the given type is well-formed (full check, including checks of subtypes)
Definition: validate_types.cpp:103
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:229
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:140
goto_functiont::body_available
bool body_available() const
Definition: goto_function.h:44
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:946
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
find_type_symbols
void find_type_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:186
validation_modet
validation_modet
Definition: validation_mode.h:13
goto_functiont
A goto function, consisting of function type (see type), function body (see body),...
Definition: goto_function.h:28
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:829
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:585
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
symbolt
Symbol table entry.
Definition: symbol.h:28
goto_functiont::parameter_identifiers
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
Definition: goto_function.h:42
goto_functiont::type
code_typet type
The type of the function, indicating the return type and parameter types.
Definition: goto_function.h:34
goto_function.h
Goto Function.
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196