Merge pull request #1375 from pkesseli/bugfix/uncaught-exceptions-invariant

Account for replaced functions in exceptions_map

Author: peterschrammel

regression/cbmc-java/exceptions25/main.c

@@ -0,0 +1,7 @@
+int main(void)
+{
+  int x;
+  __CPROVER_assume(x < 10);
+  __CPROVER_assert(x != 0, "");
+  return 0;
+}

regression/cbmc-java/exceptions25/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+VERIFICATION FAILED
+--
+^warning: ignoring
+--
+When compiling CBMC with -DDEBUG uncaught exception analysis prints an
+exceptions map per function.  This test ensures that meta-functions which are
+replaced by explicit GOTO instructions (e.g. __CPROVER_assert, __CPROVER_assume)
+and thus do not occur as explicit function calls in the final GOTO program are
+handled correctly.

src/analyses/uncaught_exceptions_analysis.cpp

@@ -193,9 +193,11 @@ void uncaught_exceptions_analysist::output(
   {
     const auto fn=it->first;
     const exceptions_mapt::const_iterator found=exceptions_map.find(fn);
-    INVARIANT(
-      found!=exceptions_map.end(),
-      "each function expected to be recorded in `exceptions_map`");
+    // Functions like __CPROVER_assert and __CPROVER_assume are replaced by
+    // explicit GOTO instructions and will not show up in exceptions_map.
+    if(found==exceptions_map.end())
+      continue;
+
     const auto &fs=found->second;
     if(!fs.empty())
     {