Merge pull request #6792 from tautschnig/feature/verbose-consistency-checks

kroening · web-flow · commit 318ab184068a · 2022-04-08T22:53:01.000+01:00
Goto functions validation: provide parameter name
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`