From 0496142cd73bd6ac075d27188bf20301304b0d1e Mon Sep 17 00:00:00 2001
From: Pascal Kesseli <pascal_kesseli@hotmail.com>
Date: Tue, 12 Sep 2017 17:04:22 +0200
Subject: [PATCH] Account for replaced functions in exceptions_map

Invariant in `uncaught_exceptions_analysist::output` expects all
functions in the GOTO model to be present in the exceptions_map.
However, functions like __CPROVER_assert(...) get replaced by explicit
GOTO instructions and will not occur as function calls, thus not be in
the map.  This fix addresses this issue, which only occurs in a debug
output produced with -DDEBUG.
---
 regression/cbmc-java/exceptions25/main.c      |  7 +++++++
 regression/cbmc-java/exceptions25/test.desc   | 14 ++++++++++++++
 src/analyses/uncaught_exceptions_analysis.cpp |  8 +++++---
 3 files changed, 26 insertions(+), 3 deletions(-)
 create mode 100644 regression/cbmc-java/exceptions25/main.c
 create mode 100644 regression/cbmc-java/exceptions25/test.desc

diff --git a/regression/cbmc-java/exceptions25/main.c b/regression/cbmc-java/exceptions25/main.c
new file mode 100644
index 0000000000..ab24eded4f
--- /dev/null
+++ b/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;
+}
diff --git a/regression/cbmc-java/exceptions25/test.desc b/regression/cbmc-java/exceptions25/test.desc
new file mode 100644
index 0000000000..f8823e7d52
--- /dev/null
+++ b/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.
diff --git a/src/analyses/uncaught_exceptions_analysis.cpp b/src/analyses/uncaught_exceptions_analysis.cpp
index 4b0674c375..dfd0d9a51c 100644
--- a/src/analyses/uncaught_exceptions_analysis.cpp
+++ b/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())
     {