From b60c23755ac6b7efe82c5afbe4c10f1b47fd1b66 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 8 Apr 2022 20:10:05 +0000 Subject: [PATCH] Goto functions validation: provide parameter name This validation step failed for Kani-generated GOTO models (cf. https://github.com/model-checking/kani/issues/957), but the error message turned out not to be very useful. --- src/goto-programs/goto_function.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/goto-programs/goto_function.cpp b/src/goto-programs/goto_function.cpp index 6a97413f7ad..f3ed1e76db6 100644 --- a/src/goto-programs/goto_function.cpp +++ b/src/goto-programs/goto_function.cpp @@ -40,10 +40,12 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm) { for(const auto &identifier : parameter_identifiers) { - DATA_CHECK( + DATA_CHECK_WITH_DIAGNOSTICS( vm, identifier.empty() || ns.lookup(identifier).is_parameter, - "parameter should be marked 'is_parameter' in the symbol table"); + "parameter should be marked 'is_parameter' in the symbol table", + "affected parameter: ", + identifier); } // function body must end with an END_FUNCTION instruction