Skip to content

Commit 87bb3ed

Browse files
danpoePetr Bauch
authored and
Petr Bauch
committed
Add validate() methods to (components of) goto models
1 parent 5045c4d commit 87bb3ed

File tree

2 files changed

+16
-4
lines changed

2 files changed

+16
-4
lines changed

src/goto-programs/goto_functions.h

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -130,6 +130,19 @@ class goto_functionst
130130

131131
std::vector<function_mapt::const_iterator> sorted() const;
132132
std::vector<function_mapt::iterator> sorted();
133+
134+
/// Check that the goto functions are well-formed
135+
///
136+
/// The validation mode indicates whether well-formedness check failures are
137+
/// reported via DATA_INVARIANT violations or exceptions.
138+
void validate(const namespacet &ns, const validation_modet vm) const
139+
{
140+
for(const auto &entry : function_map)
141+
{
142+
const goto_functiont &goto_function = entry.second;
143+
goto_function.validate(ns, vm);
144+
}
145+
}
133146
};
134147

135148
#define Forall_goto_functions(it, functions) \

src/util/exception_utils.h

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -118,10 +118,9 @@ incorrect_goto_program_exceptiont::incorrect_goto_program_exceptiont(
118118
Diagnostic &&diagnostic,
119119
Diagnostics &&... diagnostics)
120120
: message(std::move(message)),
121-
diagnostics(
122-
detail::assemble_diagnostics(
123-
std::forward(diagnostic),
124-
std::forward<Diagnostics>(diagnostics)...))
121+
diagnostics(detail::assemble_diagnostics(
122+
std::forward(diagnostic),
123+
std::forward<Diagnostics>(diagnostics)...))
125124
{
126125
}
127126

0 commit comments

Comments
 (0)