Fixes for is_threadedt, --is-threaded

Author: danpoe

regression/goto-instrument/is-threaded1/main.c

@@ -1,6 +1,11 @@
 
 int x;
 
+void func3()
+{
+  x = 6;
+}
+
 void func2()
 {
   x = 3;

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;

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"