cprover
Loading...
Searching...
No Matches
goto_functions.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Goto Programs with Functions
4
5Author: Daniel Kroening
6
7Date: June 2003
8
9\*******************************************************************/
10
13
14#include "goto_functions.h"
15
16#include <util/symbol.h>
17
18#include <algorithm>
19
21{
23 for(auto &func : function_map)
24 {
25 // Side-effect: bumps unused_location_number.
26 func.second.body.compute_location_numbers(unused_location_number);
27 }
28}
29
31 goto_programt &program)
32{
33 // Renumber just this single function. Use fresh numbers in case it has
34 // grown since it was last numbered.
36}
37
39{
40 for(auto &func : function_map)
41 {
42 func.second.body.compute_incoming_edges();
43 }
44}
45
47{
48 for(auto &func : function_map)
49 {
50 func.second.body.compute_target_numbers();
51 }
52}
53
55{
56 for(auto &func : function_map)
57 {
58 func.second.body.compute_loop_numbers();
59 }
60}
61
63std::vector<goto_functionst::function_mapt::const_iterator>
65{
66 std::vector<function_mapt::const_iterator> result;
67
68 result.reserve(function_map.size());
69
70 for(auto it = function_map.begin(); it != function_map.end(); it++)
71 result.push_back(it);
72
73 std::sort(
74 result.begin(),
75 result.end(),
76 [](function_mapt::const_iterator a, function_mapt::const_iterator b) {
77 return id2string(a->first) < id2string(b->first);
78 });
79
80 return result;
81}
82
84std::vector<goto_functionst::function_mapt::iterator> goto_functionst::sorted()
85{
86 std::vector<function_mapt::iterator> result;
87
88 result.reserve(function_map.size());
89
90 for(auto it = function_map.begin(); it != function_map.end(); it++)
91 result.push_back(it);
92
93 std::sort(
94 result.begin(),
95 result.end(),
96 [](function_mapt::iterator a, function_mapt::iterator b) {
97 return id2string(a->first) < id2string(b->first);
98 });
99
100 return result;
101}
102
104 const
105{
106 for(const auto &entry : function_map)
107 {
108 const goto_functiont &goto_function = entry.second;
109 const auto &function_name = entry.first;
110 const symbolt &function_symbol = ns.lookup(function_name);
111 const code_typet::parameterst &parameters =
113
115 vm,
116 goto_function.parameter_identifiers.size() == parameters.size(),
117 id2string(function_name) + " parameter count inconsistency\n" +
118 "goto program: " +
119 std::to_string(goto_function.parameter_identifiers.size()) +
120 "\nsymbol table: " + std::to_string(parameters.size()));
121
122 auto it = goto_function.parameter_identifiers.begin();
123 for(const auto &parameter : parameters)
124 {
126 vm,
127 it->empty() || ns.lookup(*it).type == parameter.type(),
128 id2string(function_name) + " parameter type inconsistency\n" +
129 "goto program: " + ns.lookup(*it).type.id_string() +
130 "\nsymbol table: " + parameter.type().id_string());
131 ++it;
132 }
133
134 goto_function.validate(ns, vm);
135
136 // Check that a void function does not contain any RETURN instructions
138 {
139 for(const auto &instruction : goto_function.body.instructions)
140 {
142 vm,
143 !instruction.is_set_return_value(),
144 "void function should not return a value");
145 }
146 }
147 }
148}
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
std::vector< parametert > parameterst
Definition std_types.h:542
const parameterst & parameters() const
Definition std_types.h:655
const typet & return_type() const
Definition std_types.h:645
void compute_incoming_edges()
unsigned unused_location_number
A location number such that numbers in the interval [unused_location_number, MAX_UINT] are all unused...
function_mapt function_map
void compute_location_numbers()
void validate(const namespacet &, validation_modet) const
Check that the goto functions are well-formed.
std::vector< function_mapt::const_iterator > sorted() const
returns a vector of the iterators in alphabetical order
void compute_target_numbers()
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.
A generic container class for the GOTO intermediate representation of one function.
instructionst instructions
The list of instructions in the goto program.
void compute_location_numbers(unsigned &nr)
Compute location numbers.
const irep_idt & id() const
Definition irep.h:396
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().
Symbol table entry.
Definition symbol.h:28
Goto Programs with Functions.
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition std_types.h:744
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