Goto functions validation: provide parameter name

tautschnig · tautschnig · commit b60c23755ac6 · 2022-04-08T20:23:37.000Z
This validation step failed for Kani-generated GOTO models (cf. model-checking/kani#957), but the error message turned out not to be very useful.
diff --git 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

Original file line number	Diff line number	Diff line change
`@@ -40,10 +40,12 @@ void goto_functiont::validate(const namespacet &ns, const validation_modet vm)`
`40`	`40`	`{`
`41`	`41`	`for(const auto &identifier : parameter_identifiers)`
`42`	`42`	`{`
`43`		`- DATA_CHECK(`
	`43`	`+ DATA_CHECK_WITH_DIAGNOSTICS(`
`44`	`44`	`vm,`
`45`	`45`	`identifier.empty() \|\| ns.lookup(identifier).is_parameter,`
`46`		`- "parameter should be marked 'is_parameter' in the symbol table");`
	`46`	`+ "parameter should be marked 'is_parameter' in the symbol table",`
	`47`	`+ "affected parameter: ",`
	`48`	`+ identifier);`
`47`	`49`	`}`
`48`	`50`
`49`	`51`	`// function body must end with an END_FUNCTION instruction`