Skip to content

Commit 44bbea0

Browse files
author
Daniel Kroening
committed
move goto_functionst::validate into .cpp file
The function is large, and thus, this improves compile times.
1 parent 35c31bb commit 44bbea0

File tree

2 files changed

+43
-40
lines changed

2 files changed

+43
-40
lines changed

src/goto-programs/goto_functions.cpp

Lines changed: 42 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -97,3 +97,45 @@ std::vector<goto_functionst::function_mapt::iterator> goto_functionst::sorted()
9797

9898
return result;
9999
}
100+
101+
void goto_functionst::validate(const namespacet &ns, const validation_modet vm)
102+
const
103+
{
104+
for(const auto &entry : function_map)
105+
{
106+
const goto_functiont &goto_function = entry.second;
107+
const auto &function_name = entry.first;
108+
const symbolt &function_symbol = ns.lookup(function_name);
109+
const code_typet::parameterst &parameters =
110+
to_code_type(function_symbol.type).parameters();
111+
112+
DATA_CHECK(
113+
vm,
114+
goto_function.type == ns.lookup(function_name).type,
115+
id2string(function_name) + " type inconsistency\ngoto program type: " +
116+
goto_function.type.id_string() +
117+
"\nsymbol table type: " + ns.lookup(function_name).type.id_string());
118+
119+
DATA_CHECK(
120+
vm,
121+
goto_function.parameter_identifiers.size() == parameters.size(),
122+
id2string(function_name) + " parameter count inconsistency\n" +
123+
"goto program: " +
124+
std::to_string(goto_function.parameter_identifiers.size()) +
125+
"\nsymbol table: " + std::to_string(parameters.size()));
126+
127+
auto it = goto_function.parameter_identifiers.begin();
128+
for(const auto &parameter : parameters)
129+
{
130+
DATA_CHECK(
131+
vm,
132+
it->empty() || ns.lookup(*it).type == parameter.type(),
133+
id2string(function_name) + " parameter type inconsistency\n" +
134+
"goto program: " + ns.lookup(*it).type.id_string() +
135+
"\nsymbol table: " + parameter.type().id_string());
136+
++it;
137+
}
138+
139+
goto_function.validate(ns, vm);
140+
}
141+
}

src/goto-programs/goto_functions.h

Lines changed: 1 addition & 40 deletions
Original file line numberDiff line numberDiff line change
@@ -111,46 +111,7 @@ class goto_functionst
111111
///
112112
/// The validation mode indicates whether well-formedness check failures are
113113
/// reported via DATA_INVARIANT violations or exceptions.
114-
void validate(const namespacet &ns, const validation_modet vm) const
115-
{
116-
for(const auto &entry : function_map)
117-
{
118-
const goto_functiont &goto_function = entry.second;
119-
const auto &function_name = entry.first;
120-
const symbolt &function_symbol = ns.lookup(function_name);
121-
const code_typet::parameterst &parameters =
122-
to_code_type(function_symbol.type).parameters();
123-
124-
DATA_CHECK(
125-
vm,
126-
goto_function.type == ns.lookup(function_name).type,
127-
id2string(function_name) + " type inconsistency\ngoto program type: " +
128-
goto_function.type.id_string() +
129-
"\nsymbol table type: " + ns.lookup(function_name).type.id_string());
130-
131-
DATA_CHECK(
132-
vm,
133-
goto_function.parameter_identifiers.size() == parameters.size(),
134-
id2string(function_name) + " parameter count inconsistency\n" +
135-
"goto program: " +
136-
std::to_string(goto_function.parameter_identifiers.size()) +
137-
"\nsymbol table: " + std::to_string(parameters.size()));
138-
139-
auto it = goto_function.parameter_identifiers.begin();
140-
for(const auto &parameter : parameters)
141-
{
142-
DATA_CHECK(
143-
vm,
144-
it->empty() || ns.lookup(*it).type == parameter.type(),
145-
id2string(function_name) + " parameter type inconsistency\n" +
146-
"goto program: " + ns.lookup(*it).type.id_string() +
147-
"\nsymbol table: " + parameter.type().id_string());
148-
++it;
149-
}
150-
151-
goto_function.validate(ns, vm);
152-
}
153-
}
114+
void validate(const namespacet &, validation_modet) const;
154115
};
155116

156117
#define Forall_goto_functions(it, functions) \

0 commit comments

Comments
 (0)