Allow parallel update_suite run with -w

Author: sim642

scripts/update_suite.rb

@@ -73,9 +73,6 @@ def clearline
 incremental = (ARGV.last == "-i" && ARGV.pop) || cfg
 report = ARGV.last == "-r" && ARGV.pop
 only = ARGV[0] unless ARGV[0].nil?
-if witness then
-  sequential = true
-end
 if marshal && incremental then
   fail "Marshal (-m) and Incremental (-i) tests can not be activated at the same time!"
 end
@@ -567,13 +564,14 @@ def create_test_set(lines)
   end
   def run ()
     filename = File.basename(@path)
-    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable warn.debug --set dbg.timing.enabled true --enable witness.yaml.enabled --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
-    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable warn.debug --set dbg.timing.enabled true --set witness.yaml.unassume witness.yml --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
+    witness = "witness-#{@id.sub('/','-')}.yml"
+    cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile}0 --enable warn.debug --set dbg.timing.enabled true --enable witness.yaml.enabled --set witness.yaml.path #{witness} --set goblint-dir .goblint-#{@id.sub('/','-')}-witness1 2>#{@testset.statsfile}0"
+    cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --set ana.activated[+] unassume --enable warn.debug --set dbg.timing.enabled true --set witness.yaml.unassume #{witness} --set goblint-dir .goblint-#{@id.sub('/','-')}-witness2 2>#{@testset.statsfile}"
     starttime = Time.now
     run_testset(@testset, cmd1, starttime)
     starttime = Time.now
     run_testset(@testset, cmd2, starttime)
-    FileUtils.rm_f('witness.yml')
+    FileUtils.rm_f(witness)
     end
 end
 

tests/regression/01-cpa/48-inf-recursion.c

@@ -1,4 +1,4 @@
-// SKIP
+// SKIP NOTIMEOUT
 
 // Can be used to try timeouts.
 // With defaults this will create |int| contexts and lead to a stack overflow in

tests/regression/02-base/05-result_thread_creation.c

@@ -1,4 +1,4 @@
-// SKIP This is not testing anything right now...
+// SKIP NOCHECK This is not testing anything right now...
 #include<stdlib.h>
 #include<pthread.h>