Merge branch 'goblint:master' into master

goblint · Apr 25, 2024 · 3bf5d00 · 3bf5d00
2 parents 49a44c0 + 06bc1e1
commit 3bf5d00
Show file tree

Hide file tree

Showing 13 changed files with 45 additions and 25 deletions.
diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
@@ -29,6 +29,7 @@ def pink; colorize(35) end
   def cyan; colorize(36) end
   def white; colorize(37) end
   def bg_black; colorize(40) end # gray for me
+  def bold; colorize(1) end
   def gray; colorize("38;5;240") end
 end
 class Array
@@ -63,6 +64,7 @@ def clearline
 #Command line parameters
 #Either only run a single test, or
 #"future" will also run tests we normally skip
+quiet = ARGV.last == "-q" && ARGV.pop
 $dump = ARGV.last == "-d" && ARGV.pop
 sequential = ARGV.last == "-s" && ARGV.pop
 marshal = ARGV.last == "-m" && ARGV.pop
@@ -85,10 +87,24 @@ def clearline
   future = thegroup.start_with?"-"
   future = !future # why does negation above fail?
   only = nil
+  descr = " group #{thegroup}"
 else
   future = false
+  if only.nil? then
+    descr = ""
+  else
+    descr = " #{only}"
+  end
 end
 
+if cfg then
+  descr = " incremental cfg"
+elsif incremental then
+  descr = " incremental ast"
+end
+
+print "update_suite#{descr}: ".bold
+
 $testresults = File.expand_path("tests/suite_result")
 begin
   Dir.mkdir($testresults)
@@ -608,9 +624,10 @@ def run ()
   dirname = File.dirname(filepath)
   filename = File.basename(filepath)
   Dir.chdir(dirname)
-  clearline
+  clearline unless quiet
   id = "#{p.id} #{p.group}/#{p.name}"
-  print "Testing #{id}"
+  print "Testing #{id}" unless quiet
+  print "." if quiet
   begin
     Dir.mkdir(File.join($testresults, p.group)) unless Dir.exist?(File.join($testresults, p.group))
   rescue
@@ -688,7 +705,7 @@ def run ()
   puts ("Results: " + theresultfile)
 end
 if $alliswell then
-  puts "No errors :)".green
+  puts "No errors :)".green unless quiet
 else
   puts "#{$failed.length} test(s) failed: #{$failed}".red
 end

diff --git a/tests/incremental/dune b/tests/incremental/dune
@@ -11,8 +11,8 @@
  (action
   (chdir ../..
    (progn
-     (run %{update_suite} -i) ; with AST comparison
-     (run %{update_suite} -c))))) ; with CFG comparison
+     (run %{update_suite} -i -q) ; with AST comparison
+     (run %{update_suite} -c -q))))) ; with CFG comparison
 
 (cram
  (applies_to :whole_subtree)

diff --git a/tests/regression/24-octagon/dune b/tests/regression/24-octagon/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group octagon))))
+ (action (chdir ../../.. (run %{update_suite} group octagon -q))))
diff --git a/tests/regression/36-apron/dune b/tests/regression/36-apron/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group apron))))
+ (action (chdir ../../.. (run %{update_suite} group apron -q))))
diff --git a/tests/regression/46-apron2/dune b/tests/regression/46-apron2/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group apron2))))
+ (action (chdir ../../.. (run %{update_suite} group apron2 -q))))
diff --git a/tests/regression/52-apron-mukherjee/dune b/tests/regression/52-apron-mukherjee/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group apron-mukherjee))))
+ (action (chdir ../../.. (run %{update_suite} group apron-mukherjee -q))))
diff --git a/tests/regression/56-witness/45-apron-tracked-global-annot.c b/tests/regression/56-witness/45-apron-tracked-global-annot.c
@@ -1,4 +1,4 @@
-// PARAM: --set ana.activated[+] apron --enable annotation.goblint_relation_track --set ana.activated[+] unassume --set witness.yaml.unassume 45-apron-tracked-global-annot.yml
+// SKIP PARAM: --set ana.activated[+] apron --enable annotation.goblint_relation_track --set ana.activated[+] unassume --set witness.yaml.unassume 45-apron-tracked-global-annot.yml
 #include <goblint.h>
 
 int g __attribute__((__goblint_relation_track__)) = 0;

diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune
@@ -11,16 +11,17 @@
  (action
   (chdir ../../..
    (progn
-     (run %{update_suite} apron-unassume-interval)
-     (run %{update_suite} apron-unassume-branch)
-     (run %{update_suite} apron-unassume-global)
-     (run %{update_suite} apron-unassume-priv)
-     (run %{update_suite} apron-unassume-priv2)
-     (run %{update_suite} apron-unassume-strengthening)
-     (run %{update_suite} mine-tutorial-ex4.10)
-     (run %{update_suite} hh-ex3)
-     (run %{update_suite} bh-ex1-poly)
-     (run %{update_suite} apron-unassume-precheck)))))
+     (run %{update_suite} apron-unassume-interval -q)
+     (run %{update_suite} apron-unassume-branch -q)
+     (run %{update_suite} apron-unassume-global -q)
+     (run %{update_suite} apron-unassume-priv -q)
+     (run %{update_suite} apron-unassume-priv2 -q)
+     (run %{update_suite} apron-unassume-strengthening -q)
+     (run %{update_suite} mine-tutorial-ex4.10 -q)
+     (run %{update_suite} hh-ex3 -q)
+     (run %{update_suite} bh-ex1-poly -q)
+     (run %{update_suite} apron-unassume-precheck -q)
+     (run %{update_suite} apron-tracked-global-annot -q)))))
 
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml)))
diff --git a/tests/regression/63-affeq/dune b/tests/regression/63-affeq/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group affeq))))
+ (action (chdir ../../.. (run %{update_suite} group affeq -q))))
diff --git a/tests/regression/77-lin2vareq/dune b/tests/regression/77-lin2vareq/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group lin2vareq))))
+ (action (chdir ../../.. (run %{update_suite} group lin2vareq -q))))
diff --git a/tests/regression/78-termination/dune b/tests/regression/78-termination/dune
@@ -7,4 +7,4 @@
    (:update_suite ../../../scripts/update_suite.rb)
    (glob_files ??-*.c))
  (locks /update_suite)
- (action (chdir ../../.. (run %{update_suite} group termination))))
+ (action (chdir ../../.. (run %{update_suite} group termination -q))))
diff --git a/tests/regression/dune b/tests/regression/dune
@@ -17,7 +17,7 @@
    (glob_files_rec 56-witness/??-*.yml) ; excluding witness.yml, etc. which might exist due to running update_suite outside of dune
    (source_tree ../../linux-headers))
  (locks /update_suite)
- (action (chdir ../.. (run %{update_suite}))))
+ (action (chdir ../.. (run %{update_suite} -q))))
 
 (cram
  (applies_to :whole_subtree)

diff --git a/tests/unit/mainTest.ml b/tests/unit/mainTest.ml
@@ -15,4 +15,6 @@ let all_tests =
     IntOpsTest.tests;
   ]
 
-let () = run_test_tt_main all_tests
+let () =
+  print_string "\027[0;1munit: \027[0;0;00m";
+  run_test_tt_main all_tests