From a95793ec67d767ce151b1438442b466ff27fff14 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 1 Dec 2025 13:41:43 +0200 Subject: [PATCH 1/3] Remove dbg.regression option --- regtest.sh | 2 +- src/analyses/assert.ml | 22 +++++----------------- src/config/options.schema.json | 7 ------- 3 files changed, 6 insertions(+), 25 deletions(-) diff --git a/regtest.sh b/regtest.sh index 488dd0bab4..603d02f840 100755 --- a/regtest.sh +++ b/regtest.sh @@ -14,7 +14,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" diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index aa9b6c6beb..716ec29208 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -15,26 +15,14 @@ struct 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 warn warn_fn msg = + if check then + warn_fn msg 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."); + warn (M.error ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will fail."); if refine then raise Analyses.Deadcode else man.local | `Lifted true -> warn (M.success ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" will succeed"); @@ -43,7 +31,7 @@ struct M.error ~category:Assert "%s" ("Assertion \"" ^ expr ^ "\" produces a bottom. What does that mean? (currently uninitialized arrays' content is bottom)"); man.local | `Top -> - warn (M.warn ~category:Assert "%s") ~annot:"UNKNOWN" ("Assertion \"" ^ expr ^ "\" is unknown."); + warn (M.warn ~category:Assert "%s") ("Assertion \"" ^ expr ^ "\" is unknown."); man.local let special man (lval: lval option) (f:varinfo) (args:exp list) : D.t = diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 52f98ac84c..02e634d9e7 100644 --- a/src/config/options.schema.json +++ b/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", From 916913ad6753d0d87106b57c6e05fd0873c98c5b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 1 Dec 2025 13:51:42 +0200 Subject: [PATCH 2/3] Use format strings for assert messages --- src/analyses/assert.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index 716ec29208..2dd2b6cd89 100644 --- a/src/analyses/assert.ml +++ b/src/analyses/assert.ml @@ -14,24 +14,24 @@ struct (* transfer functions *) let assert_fn man e check refine = - let expr = CilType.Exp.show e in - let warn warn_fn msg = + let assert_msg severity fmt = if check then - warn_fn msg + 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") ("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") ("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 = From 604e87f51565d9bb4503bb8cb69662a50006ebf6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Tue, 9 Dec 2025 12:34:54 +0200 Subject: [PATCH 3/3] Expand single regression test documentation --- docs/developer-guide/testing.md | 17 ++++++++++++----- regtest.sh | 1 + 2 files changed, 13 insertions(+), 5 deletions(-) diff --git a/docs/developer-guide/testing.md b/docs/developer-guide/testing.md index 5bcfabe057..7b592ed1a7 100644 --- a/docs/developer-guide/testing.md +++ b/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 ``` diff --git a/regtest.sh b/regtest.sh index 603d02f840..685bc7f763 100755 --- a/regtest.sh +++ b/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)