cprover
Loading...
Searching...
No Matches
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/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 {
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 {
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}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs,...
Definition validate.h:22
validation_modet