diff --git a/.github/workflows/unlocked.yml b/.github/workflows/unlocked.yml index 37fa38640f..7fcba9212e 100644 --- a/.github/workflows/unlocked.yml +++ b/.github/workflows/unlocked.yml @@ -193,13 +193,13 @@ jobs: run: ruby scripts/update_suite.rb group apron-mukherjee -s - name: Test marshal regression - run: ruby scripts/update_suite.rb -m + run: ruby scripts/update_suite.rb -m -s - name: Test incremental regression - run: ruby scripts/update_suite.rb -i + run: ruby scripts/update_suite.rb -i -s - name: Test incremental regression with cfg comparison - run: ruby scripts/update_suite.rb -c + run: ruby scripts/update_suite.rb -c -s gobview: strategy: diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb index 7509849b8e..044306ec20 100755 --- a/scripts/update_suite.rb +++ b/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 marshal || witness || incremental then - sequential = true -end if marshal && incremental then fail "Marshal (-m) and Incremental (-i) tests can not be activated at the same time!" end @@ -505,8 +502,9 @@ def create_test_set(lines) def run filename = File.basename(@path) - cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --enable incremental.save --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}" - cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --enable dbg.timing.enabled --enable incremental.load --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}" + incrdir = "incremental_data-#{@id.sub('/','-')}" + cmd = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --enable incremental.save --set incremental.save-dir #{incrdir} --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-save 2>#{@testset.statsfile}" + cmd_incr = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset_incr.warnfile} --enable dbg.timing.enabled --enable incremental.load --set incremental.load-dir #{incrdir} --set goblint-dir .goblint-#{@id.sub('/','-')}-incr-load 2>#{@testset_incr.statsfile}" starttime = Time.now run_testset(@testset_incr, cmd, starttime) # apply patch @@ -515,7 +513,7 @@ def run run_testset(@testset_incr, cmd_incr, starttime) # revert patch `patch -p3 -b -R <#{@patch_path}` - FileUtils.rm_rf('incremental_data') + FileUtils.rm_rf(incrdir) end def report @@ -549,12 +547,13 @@ def create_test_set(lines) end def run () filename = File.basename(@path) - cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set save_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}" - cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --conf run/config.json --set save_run '' --set load_run run --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}" + rundir = "run-#{@id.sub('/','-')}" + cmd1 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --set save_run #{rundir} --set goblint-dir .goblint-#{@id.sub('/','-')}-run-save 2>#{@testset.statsfile}" + cmd2 = "#{$goblint} #{filename} #{@params} #{ENV['gobopt']} 1>#{@testset.warnfile} --enable dbg.timing.enabled --conf #{rundir}/config.json --set save_run '' --set load_run #{rundir} --set goblint-dir .goblint-#{@id.sub('/','-')}-run-load 2>#{@testset.statsfile}" starttime = Time.now run_testset(@testset, cmd1, starttime) run_testset(@testset, cmd2, starttime) - FileUtils.rm_rf('run') + FileUtils.rm_rf(rundir) end end @@ -565,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 diff --git a/tests/regression/01-cpa/48-inf-recursion.c b/tests/regression/01-cpa/48-inf-recursion.c index 0bfcba6a8d..122ec90657 100644 --- a/tests/regression/01-cpa/48-inf-recursion.c +++ b/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 diff --git a/tests/regression/02-base/05-result_thread_creation.c b/tests/regression/02-base/05-result_thread_creation.c index 434f029fd9..532eeb4ac4 100644 --- a/tests/regression/02-base/05-result_thread_creation.c +++ b/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 #include