Merge pull request #6426 from adpaco-aws/debug-convert-function

Include function and parameter in `convert_function` error messages

Author: tautschnig

COMPILING.md

@@ -1,4 +1,4 @@
-#WHAT ARCHITECTURE ?
+# What architecture?
 
 CPROVER now needs a C++11 compliant compiler and is known to work in the
 following environments:
@@ -18,7 +18,7 @@ past, but are not actively tested:
 - Solaris 11
 - FreeBSD 11
 
-#Building using CMake
+# Building using CMake
 
 Building with CMake is supported across Linux, MacOS X and Windows with Visual
 Studio 2019. There are also hand-written make files which can be used to build

src/goto-programs/goto_convert_functions.cpp

@@ -166,10 +166,19 @@ void goto_convert_functionst::convert_function(
   // we have a body, make sure all parameter names are valid
   for(const auto &p : f.parameter_identifiers)
   {
-    DATA_INVARIANT(!p.empty(), "parameter identifier should not be empty");
-    DATA_INVARIANT(
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      !p.empty(),
+      "parameter identifier should not be empty",
+      "function:",
+      identifier);
+
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
       symbol_table.has_symbol(p),
-      "parameter identifier must be a known symbol");
+      "parameter identifier must be a known symbol",
+      "function:",
+      identifier,
+      "parameter:",
+      p);
   }
 
   lifetimet parent_lifetime = lifetime;