Print info using DATA_INVARIANT_WITH_DIAGNOSTICS

Author: adpaco-aws

src/goto-programs/goto_convert_functions.cpp

@@ -163,36 +163,24 @@ void goto_convert_functionst::convert_function(
     symbol.is_compiled()) /* goto_inline may have removed the body */
     return;
 
-  const size_t ERROR_MSG_LEN = 512;
-  char parameter_error_message[ERROR_MSG_LEN];
   // we have a body, make sure all parameter names are valid
   for(const auto &p : f.parameter_identifiers)
   {
-    if (p.empty())
-    {
-      snprintf(parameter_error_message,
-               ERROR_MSG_LEN - 1,
-               "parameter identifier should not be empty\n"
-               "function: %s\n"
-               "parameter: %s",
-               identifier.c_str(),
-               p.c_str());
-    }
-    DATA_INVARIANT(!p.empty(), parameter_error_message);
-
-    if (!symbol_table.has_symbol(p))
-    {
-      snprintf(parameter_error_message,
-               ERROR_MSG_LEN - 1,
-               "parameter identifier must be a known symbol\n"
-               "function: %s\n"
-               "parameter: %s",
-               identifier.c_str(),
-               p.c_str());
-    }
-    DATA_INVARIANT(
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
+      !p.empty(),
+      "parameter identifier should not be empty",
+      "function:",
+      identifier,
+      "parameter:",
+      p);
+
+    DATA_INVARIANT_WITH_DIAGNOSTICS(
       symbol_table.has_symbol(p),
-      parameter_error_message);
+      "parameter identifier must be a known symbol",
+      "function:",
+      identifier,
+      "parameter:",
+      p);
   }
 
   lifetimet parent_lifetime = lifetime;