From 6f622d118a2a7599eb24bbe437ec761d9b15bc5f Mon Sep 17 00:00:00 2001
From: Daniel Poetzl <daniel.poetzl@diffblue.com>
Date: Thu, 15 Feb 2018 18:21:04 +0000
Subject: [PATCH] Fixes for is_threadedt, --is-threaded

---
 regression/goto-instrument/is-threaded1/main.c       |  5 +++++
 src/analyses/is_threaded.cpp                         | 12 ++++--------
 .../goto_instrument_parse_options.cpp                |  4 ++++
 3 files changed, 13 insertions(+), 8 deletions(-)

diff --git a/regression/goto-instrument/is-threaded1/main.c b/regression/goto-instrument/is-threaded1/main.c
index 875af72fec0..000787014b9 100644
--- a/regression/goto-instrument/is-threaded1/main.c
+++ b/regression/goto-instrument/is-threaded1/main.c
@@ -1,6 +1,11 @@
 
 int x;
 
+void func3()
+{
+  x = 6;
+}
+
 void func2()
 {
   x = 3;
diff --git a/src/analyses/is_threaded.cpp b/src/analyses/is_threaded.cpp
index c509fcac857..ca1ddff4718 100644
--- a/src/analyses/is_threaded.cpp
+++ b/src/analyses/is_threaded.cpp
@@ -33,10 +33,8 @@ class is_threaded_domaint:public ai_domain_baset
     locationt from,
     locationt to)
   {
-    // assert(src.reachable);
-
-    if(!src.reachable)
-      return false;
+    INVARIANT(src.reachable,
+              "Abstract states are only merged at reachable locations");
 
     bool old_reachable=reachable;
     bool old_is_threaded=is_threaded;
@@ -52,10 +50,8 @@ class is_threaded_domaint:public ai_domain_baset
   transform(locationt from, locationt to, ai_baset &ai, const namespacet &ns)
     final override
   {
-    // assert(reachable);
-
-    if(!reachable)
-      return;
+    INVARIANT(reachable,
+              "Transformers are only applied at reachable locations");
 
     if(from->is_start_thread())
       is_threaded=true;
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
index a98acd741f6..6b208827fd5 100644
--- a/src/goto-instrument/goto_instrument_parse_options.cpp
+++ b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -257,6 +257,8 @@ int goto_instrument_parse_optionst::doit()
                     << "\n\n";
         }
       }
+
+      return CPROVER_EXIT_SUCCESS;
     }
 
     if(cmdline.isset("show-value-sets"))
@@ -1493,6 +1495,8 @@ void goto_instrument_parse_optionst::help()
     // NOLINTNEXTLINE(whitespace/line_length)
     " --reachable-call-graph       show graph of function calls potentially reachable from main function\n"
     " --class-hierarchy            show class hierarchy\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --show-threaded              show instructions that may be executed by more than one thread\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"