Remove dbg.regression option

docs/developer-guide/testing.md

@@ -16,17 +16,24 @@ Regression tests can be run with various granularity:
 
 * Run all (non-Apron) regression tests with: `./scripts/update_suite.rb`.
 * Run all Apron tests with: `dune build @runaprontest`.
-* Run a group of tests with: `./scripts/update_suite.rb group sanity`.
+* Run a group of tests (by directory, without number) with: `./scripts/update_suite.rb group sanity`.
 
     Unfortunately this also runs skipped tests.
     This is a bug that is used as a feature in the tests with Apron, as not all CI jobs have the Apron library installed.
 
-* Run a single test with: `./scripts/update_suite.rb assert`.
-* Run a single test with full output: `./regtest.sh 00 01`.
+* Run a single test (by name, without group or number) with: `./scripts/update_suite.rb assert`.
 
-    Additional options are also passed to Goblint.
+    This compares Goblint output with test annotations (described below) and only outputs mismatches (i.e. test failures).
+    It is useful for checking if the test passes (or which parts don't).
+    Since group name is not specified, beware of same test name in multiple groups.
 
-To pass additional options to Goblint with `update_suite.rb`, use the `gobopt` environment variable, e.g.:
+* Run a single test (by group and test number) with full output: `./regtest.sh 00 01`.
+
+    This _does not_ compare Goblint output with test annotations, but directly shows all Goblint output.
+    It is useful for debugging the test.
+    Additional command-line options are also passed to Goblint.
+
+To pass additional command-line options to Goblint with `update_suite.rb`, use the `gobopt` environment variable, e.g.:
 ```
 gobopt='--set ana.base.privatization write+lock' ./scripts/update_suite.rb
 ```

regtest.sh

@@ -2,6 +2,7 @@
 #MacOS: needs brew install grep
 if [ $# -lt 2 ]; then
     echo "Usage: $0 group-nr test-nr [extra options]"
+    echo "(Does not check test annotations.)"
     exit 1
 fi
 file=(tests/regression/$1*/$2*.c)
@@ -14,7 +15,7 @@ if [[ $OSTYPE == 'darwin'* ]]; then
   grep="ggrep"
 fi
 params="`$grep -oP "PARAM: \K.*" $file`"
-cmd="./goblint --enable warn.debug --enable dbg.regression --html $params ${@:3} $file" # -v
+cmd="./goblint --enable warn.debug --html $params ${@:3} $file" # -v
 echo "$cmd"
 eval $cmd
 echo "See result/index.xml"

src/analyses/assert.ml

@@ -14,36 +14,24 @@ struct
   (* transfer functions *)
 
   let assert_fn man e check refine =
-    let expr = CilType.Exp.show e in
-    let warn warn_fn ?annot msg = if check then
-        if get_bool "dbg.regression" then ( (* This only prints unexpected results (with the difference) as indicated by the comment behind the assert (same as used by the regression test script). *)
-          let loc = !M.current_loc in
-          let line = List.at (List.of_enum @@ File.lines_of loc.file) (loc.line-1) in (* nosemgrep: batenum-of_enum *)
-          let open Str in
-          let expected = if string_match (regexp ".+//.*\\(FAIL\\|UNKNOWN\\).*") line 0 then Some (matched_group 1 line) else None in
-          if expected <> annot then (
-            let result = if annot = None && (expected = Some ("NOWARN") || (expected = Some ("UNKNOWN") && not (String.exists line "UNKNOWN!"))) then "improved" else "failed" in
-            (* Expressions with logical connectives like a && b are calculated in temporary variables by CIL. Instead of the original expression, we then see something like tmp___0. So we replace expr in msg by the original source if this is the case. *)
-            let assert_expr = if string_match (regexp ".*assert(\\(.+\\));.*") line 0 then matched_group 1 line else expr in
-            let msg = if expr <> assert_expr then String.nreplace ~str:msg ~sub:expr ~by:assert_expr else msg in
-            warn_fn (msg ^ " Expected: " ^ (expected |? "SUCCESS") ^ " -> " ^ result)
-          )
-        ) else
-          warn_fn msg
+    let assert_msg severity fmt =
+      if check then
+        M.msg severity ~category:Assert fmt
+      else
+        GobPretty.igprintf () fmt
     in
-    (* TODO: use format instead of %s for the following messages *)
     match Queries.eval_bool (Analyses.ask_of_man man) e with
     | `Lifted false ->
-      warn (M.error ~category:Assert "%s") ~annot:"FAIL" ("Assertion \"" ^ expr ^ "\" will fail.");
+      assert_msg Error "Assertion \"%a\" will fail." CilType.Exp.pretty e;
       if refine then raise Analyses.Deadcode else man.local
     | `Lifted true ->
-      warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed");
+      assert_msg Success "Assertion \"%a\" will succeed" CilType.Exp.pretty e;
       man.local
     | `Bot ->
-      M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)");
+      M.error ~category:Assert "Assertion \"%a\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)" CilType.Exp.pretty e;
       man.local
     | `Top ->
-      warn (M.warn ~category:Assert "%s") ~annot:"UNKNOWN" ("Assertion \"" ^ expr ^ "\" is unknown.");
+      assert_msg Warning "Assertion \"%a\" is unknown." CilType.Exp.pretty e;
       man.local
 
   let special man (lval: lval option) (f:varinfo) (args:exp list) : D.t =

src/config/options.schema.json

@@ -2202,13 +2202,6 @@
           "type": "boolean",
           "default": false
         },
-        "regression": {
-          "title": "dbg.regression",
-          "description":
-            "Only output warnings for assertions that have an unexpected result (no comment, comment FAIL, comment UNKNOWN)",
-          "type": "boolean",
-          "default": false
-        },
         "test": {
           "title": "dbg.test",
           "type": "object",