Merge branch 'master' of github.com:diffblue/cbmc

Author: kroening

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

@@ -0,0 +1,25 @@
+
+int x;
+
+void func2()
+{
+  x = 3;
+}
+
+void func1()
+{
+  x = 1;
+  func2();
+  x = 2;
+}
+
+int main()
+{
+  x = 4;
+  __CPROVER_ASYNC_0:
+    func1();
+  x = 5;
+
+  return 0;
+}
+

regression/goto-instrument/is-threaded1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--show-threaded
+activate-multi-line-match
+x = 2;\nIs threaded: True
+--
+^warning: ignoring

src/analyses/is_threaded.cpp

@@ -15,41 +15,33 @@ class is_threaded_domaint:public ai_domain_baset
 {
 public:
   bool reachable;
-  bool has_spawn;
   bool is_threaded;
 
-  inline is_threaded_domaint():
+  is_threaded_domaint():
     reachable(false),
-    has_spawn(false),
     is_threaded(false)
   {
     // this is bottom
   }
 
-  inline bool merge(
+  bool merge(
     const is_threaded_domaint &src,
     locationt from,
     locationt to)
   {
+    // assert(src.reachable);
+
+    if(!src.reachable)
+      return false;
+
     bool old_reachable=reachable;
-    if(src.reachable)
-      reachable=true;
-
-    bool old_h_s=has_spawn;
-    if(src.has_spawn &&
-       (from->is_end_function() ||
-        from->function==to->function))
-      has_spawn=true;
-
-    bool old_i_t=is_threaded;
-    if(has_spawn ||
-       (src.is_threaded &&
-       !from->is_end_function()))
-      is_threaded=true;
+    bool old_is_threaded=is_threaded;
+
+    reachable=true;
+    is_threaded|=src.is_threaded;
 
     return old_reachable!=reachable ||
-           old_i_t!=is_threaded ||
-           old_h_s!=has_spawn;
+           old_is_threaded!=is_threaded;
   }
 
   void transform(
@@ -58,30 +50,31 @@ class is_threaded_domaint:public ai_domain_baset
     ai_baset &ai,
     const namespacet &ns) final
   {
+    // assert(reachable);
+
     if(!reachable)
       return;
-    if(from->is_start_thread() ||
-       to->is_end_thread())
-    {
-      has_spawn=true;
+
+    if(from->is_start_thread())
       is_threaded=true;
-    }
   }
 
   void make_bottom() final
   {
-    reachable=has_spawn=is_threaded=false;
+    reachable=false;
+    is_threaded=false;
   }
 
   void make_top() final
   {
-    reachable=has_spawn=is_threaded=true;
+    reachable=true;
+    is_threaded=true;
   }
 
   void make_entry() final
   {
     reachable=true;
-    has_spawn=is_threaded=false;
+    is_threaded=false;
   }
 };
 

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -52,6 +52,7 @@ Author: Daniel Kroening, [email protected]
 #include <analyses/reaching_definitions.h>
 #include <analyses/dependence_graph.h>
 #include <analyses/constant_propagator.h>
+#include <analyses/is_threaded.h>
 
 #include <cbmc/version.h>
 
@@ -246,6 +247,31 @@ int goto_instrument_parse_optionst::doit()
       }
     }
 
+    if(cmdline.isset("show-threaded"))
+    {
+      namespacet ns(symbol_table);
+
+      is_threadedt is_threaded(goto_functions);
+
+      forall_goto_functions(f_it, goto_functions)
+      {
+        std::cout << "////" << std::endl;
+        std::cout << "//// Function: " << f_it->first << std::endl;
+        std::cout << "////" << std::endl;
+        std::cout << std::endl;
+
+        const goto_programt &goto_program=f_it->second.body;
+
+        forall_goto_program_instructions(i_it, goto_program)
+        {
+          goto_program.output_instruction(ns, "", std::cout, i_it);
+          std::cout << "Is threaded: " << (is_threaded(i_it)?"True":"False")
+                    << std::endl;
+          std::cout << std::endl;
+        }
+      }
+    }
+
     if(cmdline.isset("show-value-sets"))
     {
       do_indirect_call_and_rtti_removal();

src/goto-instrument/goto_instrument_parse_options.h

@@ -67,7 +67,8 @@ Author: Daniel Kroening, [email protected]
   "(interpreter)(show-reaching-definitions)(count-eloc)(list-eloc)" \
   "(list-symbols)(list-undefined-functions)" \
   "(z3)(add-library)(show-dependence-graph)" \
-  "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):"
+  "(horn)(skip-loops):(apply-code-contracts)(model-argc-argv):" \
+  "(show-threaded)"
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,