Run 56-witness apron tests automatically

goblint · Feb 28, 2024 · 9c2c167 · 9c2c167
1 parent fd0cb18
commit 9c2c167
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 1 deletion.
diff --git a/tests/regression/56-witness/25-apron-unassume-strengthening.c b/tests/regression/56-witness/25-apron-unassume-strengthening.c
@@ -7,7 +7,7 @@ int main() {
   if (x < y) {
     __goblint_check(x == 0); // UNKNOWN (intentional by unassume)
     __goblint_check(x >= 0);
-    __goblint_check(x < y);
+    __goblint_check(x < y); // TODO: https://github.com/goblint/analyzer/issues/1373
   }
   return 0;
 }
diff --git a/tests/regression/56-witness/dune b/tests/regression/56-witness/dune
@@ -1,2 +1,26 @@
+(rule
+ (aliases runtest runaprontest)
+ (enabled_if %{lib-available:apron})
+ (deps
+   (package goblint)
+   ../../../goblint ; update_suite calls local goblint
+   (:update_suite ../../../scripts/update_suite.rb)
+   (glob_files ??-*.c)
+   (glob_files ??-*.yml)) ; excluding witness.yml, etc. which might exist due to running update_suite outside of dune
+ (locks /update_suite)
+ (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)))))
+
 (cram
  (deps (glob_files *.c) (glob_files ??-*.yml)))