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 488dd0bab4..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) @@ -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" diff --git a/src/analyses/assert.ml b/src/analyses/assert.ml index aa9b6c6beb..2dd2b6cd89 100644 --- a/src/analyses/assert.ml +++ b/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 = 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",