diff --git a/.gitignore b/.gitignore index 7038e51f8f..da004ca979 100644 --- a/.gitignore +++ b/.gitignore @@ -54,6 +54,7 @@ goblint.bc.js *.rej sv-comp/goblint.zip +scripts/sv-comp/goblint.zip privPrecCompare privPrecCompare-creduce diff --git a/Makefile b/Makefile index 1d2d93672a..0d8b16c2f2 100644 --- a/Makefile +++ b/Makefile @@ -2,3 +2,21 @@ native : % : @./make.sh $@ + + +.PHONY: sv-comp-tag sv-comp-build sv-comp-smoketest-ubuntu sv-comp-smoketest-competition sv-comp-smoketest sv-comp + +sv-comp-tag: + git tag -m "SV-COMP 2026" svcomp26 + +sv-comp-build: sv-comp-tag + docker build . -f scripts/sv-comp/Dockerfile --output=scripts/sv-comp/ + +sv-comp-smoketest-ubuntu: sv-comp-tag + docker build . -f scripts/sv-comp/Dockerfile --target smoketest-ubuntu + +sv-comp-smoketest-competition: sv-comp-tag + docker build . -f scripts/sv-comp/Dockerfile --target smoketest-competition + +sv-comp-smoketest: sv-comp-smoketest-ubuntu sv-comp-smoketest-competition; +sv-comp: sv-comp-smoketest sv-comp-build; diff --git a/conf/svcomp.json b/conf/svcomp26/level00-validate.json similarity index 80% rename from conf/svcomp.json rename to conf/svcomp26/level00-validate.json index b9f447ffea..63f68cb8e2 100644 --- a/conf/svcomp.json +++ b/conf/svcomp26/level00-validate.json @@ -6,12 +6,11 @@ }, "int": { "def_exc": true, - "enums": false, - "interval": true + "enums": false }, "float": { - "interval": true, - "evaluate_math_functions": true + "interval": false, + "evaluate_math_functions": false }, "activated": [ "base", @@ -27,12 +26,12 @@ "expRelation", "mhp", "assert", - "var_eq", "symb_locks", "region", "thread", "threadJoins", - "abortUnless" + "abortUnless", + "unassume" ], "path_sens": [ "mutex", @@ -61,9 +60,6 @@ "reduceAnalyses", "mallocWrappers", "noRecursiveIntervals", - "enums", - "congruence", - "octagon", "wideningThresholds", "loopUnrollHeuristic", "memsafetySpecification", @@ -71,6 +67,9 @@ "termination", "tmpSpecialAnalysis" ] + }, + "widen": { + "tokens": true } }, "exp": { @@ -90,25 +89,25 @@ }, "witness": { "yaml": { - "enabled": true, - "sv-comp-true-only": false, + "enabled": false, + "strict": true, "format-version": "2.0", "entry-types": [ - "invariant_set" + "invariant_set", + "violation_sequence" ], "invariant-types": [ + "location_invariant", "loop_invariant" ] }, "invariant": { "loop-head": true, - "after-lock": false, - "other": false, - "accessed": false, - "exact": true + "after-lock": true, + "other": true } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp26/level00.json b/conf/svcomp26/level00.json index 23c4582663..ca82e274ad 100644 --- a/conf/svcomp26/level00.json +++ b/conf/svcomp26/level00.json @@ -6,7 +6,7 @@ }, "int": { "def_exc": true, - "enums": false + "enums": false }, "float": { "interval": false, @@ -30,7 +30,7 @@ "region", "thread", "threadJoins", - "abortUnless" + "abortUnless" ], "path_sens": [ "mutex", @@ -39,7 +39,7 @@ "expsplit", "activeSetjmp", "memLeak", - "threadflag" + "threadflag" ], "context": { "widen": false @@ -86,6 +86,7 @@ "witness": { "yaml": { "enabled": true, + "sv-comp-true-only": false, "format-version": "2.0", "entry-types": [ "invariant_set" @@ -103,6 +104,6 @@ } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp-validate.json b/conf/svcomp26/level01-validate.json similarity index 98% rename from conf/svcomp-validate.json rename to conf/svcomp26/level01-validate.json index 0ce6ce841b..2dea814df5 100644 --- a/conf/svcomp-validate.json +++ b/conf/svcomp26/level01-validate.json @@ -113,6 +113,6 @@ } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp26/level01.json b/conf/svcomp26/level01.json index b9f447ffea..a595fe3e04 100644 --- a/conf/svcomp26/level01.json +++ b/conf/svcomp26/level01.json @@ -109,6 +109,6 @@ } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp26/level02-validate.json b/conf/svcomp26/level02-validate.json new file mode 100644 index 0000000000..a9bed8d371 --- /dev/null +++ b/conf/svcomp26/level02-validate.json @@ -0,0 +1,134 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": true, + "congruence": true, + "bitfield":true, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "affeq", + "apron", + "unassume" + ], + "apron": { + "domain": "octagon" + }, + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + }, + "structs": { + "domain": "sets" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + }, + "widen": { + "tokens": true + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "solvers": { + "td3": { + "widen_gas": 30, + "side_widen_gas": 30 + } + }, + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": false, + "strict": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set", + "violation_sequence" + ], + "invariant-types": [ + "location_invariant", + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": true, + "other": true + } + }, + "pre": { + "transform-paths": false + } +} diff --git a/conf/svcomp26/level02.json b/conf/svcomp26/level02.json index e5d1824a00..1b5478f77b 100644 --- a/conf/svcomp26/level02.json +++ b/conf/svcomp26/level02.json @@ -107,6 +107,7 @@ "witness": { "yaml": { "enabled": true, + "sv-comp-true-only": false, "format-version": "2.0", "entry-types": [ "invariant_set" @@ -124,6 +125,6 @@ } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp26/level03-validate.json b/conf/svcomp26/level03-validate.json new file mode 100644 index 0000000000..6eef37fa52 --- /dev/null +++ b/conf/svcomp26/level03-validate.json @@ -0,0 +1,132 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "enums": true, + "congruence": true, + "bitfield":true, + "interval": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "branchSet", + "unassume" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag", + "branchSet" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "partitioned" + }, + "structs": { + "domain": "sets" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + }, + "widen": { + "tokens": true + } + }, + "exp": { + "region-offsets": true + }, + "solver": "td3", + "solvers": { + "td3": { + "narrow-globs": { + "enabled": true + } + } + }, + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": false, + "strict": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set", + "violation_sequence" + ], + "invariant-types": [ + "location_invariant", + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": true, + "other": true + } + }, + "pre": { + "transform-paths": false + } +} diff --git a/conf/svcomp26/level03.json b/conf/svcomp26/level03.json index 3963328e0c..98f4767892 100644 --- a/conf/svcomp26/level03.json +++ b/conf/svcomp26/level03.json @@ -34,8 +34,8 @@ "region", "thread", "threadJoins", - "abortUnless", - "branchSet" + "abortUnless", + "branchSet" ], "path_sens": [ "mutex", @@ -44,8 +44,8 @@ "expsplit", "activeSetjmp", "memLeak", - "threadflag", - "branchSet" + "threadflag", + "branchSet" ], "context": { "widen": false @@ -57,7 +57,6 @@ "structs": { "domain": "sets" } - }, "race": { "free": false, @@ -106,6 +105,7 @@ "witness": { "yaml": { "enabled": true, + "sv-comp-true-only": false, "format-version": "2.0", "entry-types": [ "invariant_set" @@ -123,6 +123,6 @@ } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp26/level04-validate.json b/conf/svcomp26/level04-validate.json new file mode 100644 index 0000000000..69ae050cb4 --- /dev/null +++ b/conf/svcomp26/level04-validate.json @@ -0,0 +1,127 @@ +{ + "ana": { + "sv-comp": { + "enabled": true, + "functions": true + }, + "int": { + "def_exc": true, + "congruence": true, + "bitfield":true, + "enums": true, + "interval": true, + "interval_threshold_widening": true + }, + "float": { + "interval": true, + "evaluate_math_functions": true + }, + "activated": [ + "base", + "threadid", + "threadflag", + "threadreturn", + "mallocWrapper", + "mutexEvents", + "mutex", + "access", + "race", + "escape", + "expRelation", + "mhp", + "assert", + "var_eq", + "symb_locks", + "region", + "thread", + "threadJoins", + "abortUnless", + "unassume" + ], + "path_sens": [ + "mutex", + "malloc_null", + "uninit", + "expsplit", + "activeSetjmp", + "memLeak", + "threadflag", + "base" + ], + "context": { + "widen": false + }, + "base": { + "arrays": { + "domain": "unroll", + "unrolling-factor": 16 + }, + "structs": { + "domain": "sets" + } + }, + "race": { + "free": false, + "call": false + }, + "autotune": { + "enabled": true, + "activated": [ + "reduceAnalyses", + "mallocWrappers", + "noRecursiveIntervals", + "enums", + "congruence", + "octagon", + "wideningThresholds", + "loopUnrollHeuristic", + "memsafetySpecification", + "noOverflows", + "termination", + "tmpSpecialAnalysis" + ] + }, + "widen": { + "tokens": true + } + }, + "exp": { + "region-offsets": true, + "unrolling-factor": 4 + }, + "solver": "td3", + "sem": { + "unknown_function": { + "spawn": false + }, + "int": { + "signed_overflow": "assume_none" + }, + "null-pointer": { + "dereference": "assume_none" + } + }, + "witness": { + "yaml": { + "enabled": false, + "strict": true, + "format-version": "2.0", + "entry-types": [ + "invariant_set", + "violation_sequence" + ], + "invariant-types": [ + "location_invariant", + "loop_invariant" + ] + }, + "invariant": { + "loop-head": true, + "after-lock": true, + "other": true + } + }, + "pre": { + "transform-paths": false + } +} diff --git a/conf/svcomp26/level04.json b/conf/svcomp26/level04.json index 46e9ffe8d0..4c3995a73f 100644 --- a/conf/svcomp26/level04.json +++ b/conf/svcomp26/level04.json @@ -9,9 +9,8 @@ "congruence": true, "bitfield":true, "enums": true, - "interval": true, - "interval_threshold_widening": true - + "interval": true, + "interval_threshold_widening": true }, "float": { "interval": true, @@ -36,7 +35,7 @@ "region", "thread", "threadJoins", - "abortUnless" + "abortUnless" ], "path_sens": [ "mutex", @@ -45,8 +44,8 @@ "expsplit", "activeSetjmp", "memLeak", - "threadflag", - "base" + "threadflag", + "base" ], "context": { "widen": false @@ -101,6 +100,7 @@ "witness": { "yaml": { "enabled": true, + "sv-comp-true-only": false, "format-version": "2.0", "entry-types": [ "invariant_set" @@ -118,6 +118,6 @@ } }, "pre": { - "enabled": false + "transform-paths": false } } diff --git a/conf/svcomp26/seq-validate.txt b/conf/svcomp26/seq-validate.txt new file mode 100644 index 0000000000..a3a1f540f4 --- /dev/null +++ b/conf/svcomp26/seq-validate.txt @@ -0,0 +1,13 @@ +# Portfolio Configuration Sequence +# paths are relative to analyzer base directory +# +# minimalist run, basically only constants/def_exc +--conf conf/svcomp26/level00-validate.json +# standard run based on svcomp 25 settings +--conf conf/svcomp26/level01-validate.json +# apron/affeq run with enums,congruence, bitfield and sets for structs, sporting (side_)widen_gas 30 +--conf conf/svcomp26/level02-validate.json +# branchset-pathsensitive run +--conf conf/svcomp26/level03-validate.json +# base-pathsensitive run +--conf conf/svcomp26/level04-validate.json \ No newline at end of file diff --git a/docs/developer-guide/releasing.md b/docs/developer-guide/releasing.md index 85203283fe..508b599b8a 100644 --- a/docs/developer-guide/releasing.md +++ b/docs/developer-guide/releasing.md @@ -71,51 +71,26 @@ ### Before all preruns -1. Make sure you are running the same Ubuntu version as will be used for SV-COMP. +1. Update Ubuntu version used for SV-COMP in `scripts/sv-comp/Dockerfile`. 2. Create conf file for SV-COMP year. -3. Make sure this repository is checked out into a directory called `goblint`, not the default `analyzer`. +3. Update SV-COMP year in `Makefile`, `scripts/sv-comp/archive.sh`, `scripts/sv-comp/smoketest.sh` and `scripts/sv-comp/Dockerfile`. - This is required such that the created archive would have everything in a single directory called `goblint`. + This includes: git tag name, git tag message, zipped conf file and [SV-COMP container image tag](https://gitlab.com/sosy-lab/benchmarking/competition-scripts/#container-image). -4. Update SV-COMP year in `scripts/sv-comp/archive.sh`. - - This includes: git tag name, git tag message and zipped conf file. - -5. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository. +4. Open MR with conf file name to the [bench-defs](https://gitlab.com/sosy-lab/sv-comp/bench-defs) repository. ### For each prerun -1. Update opam pins: - - 1. Make sure you have the same `goblint-cil` version pinned as `goblint.opam` specifies. - 2. Unpin `zarith.1.12-gob0`, because Gobview compatibility is not required. - -2. Make sure you have nothing valuable that would be deleted by `make clean`. -3. Delete git tag from previous prerun: `git tag -d svcompXY`. -4. Create archive: `./scripts/sv-comp/archive.sh`. +1. Make sure you have a clean git repository. +2. Delete git tag from previous prerun (if exists): `git tag -d svcompXY`. +3. Create archive: `make sv-comp`. + This locally creates the `svcompXY` git tag, which should _not_ be pushed until after all preruns (see below). + This also smoke tests (with `scripts/sv-comp/smoketest.sh`) the archive on clean Ubuntu (with required packages) and competition Ubuntu. The resulting archive is `scripts/sv-comp/goblint.zip`. -5. Check unextracted archive in latest SV-COMP container image: . - - Inside Docker: - - 1. Check version: `./goblint --version`. - 2. Mount some sv-benchmarks and properties, e.g. as `/tool-test`, and run Goblint on them manually. - - This ensures that the environment and the archive have all the correct system libraries. - -6. Create (or add new version) Zenodo artifact and upload the archive. - -7. Open MR with Zenodo version DOI to the [fm-tools](https://gitlab.com/sosy-lab/benchmarking/fm-tools) repository. - - +4. Create (or add new version) Zenodo artifact and upload the archive. +5. Open MR with Zenodo version DOI to the [fm-tools](https://gitlab.com/sosy-lab/benchmarking/fm-tools) repository. ### After all preruns diff --git a/make.sh b/make.sh index 2d87dbd509..1045656179 100755 --- a/make.sh +++ b/make.sh @@ -15,6 +15,7 @@ rule() { case $1 in # new rules using dune clean) + eval $(opam env) git clean -X -f dune clean ;; nat*) @@ -75,7 +76,7 @@ rule() { ;; setup) echo "Make sure you have the following installed: opam >= 2.0.0, git, patch, m4, autoconf, libgmp-dev, libmpfr-dev, pkg-config" echo "For the --html output you also need: graphviz and python3-pygments (optional)" - echo "For running the regression tests you also need: ruby, gem, curl, and the `os` gem" + echo "For running the regression tests you also need: ruby, gem, curl, and the os gem" echo "For reference see ./Dockerfile or ./scripts/travis-ci.sh" opam_setup ;; dev) diff --git a/scripts/creduce/branches.sh b/scripts/creduce/branches.sh index d509a19576..6ca83557b4 100755 --- a/scripts/creduce/branches.sh +++ b/scripts/creduce/branches.sh @@ -5,7 +5,7 @@ set -e gcc -c -Werror=implicit-function-declaration ./bad.c GOBLINTDIR="/home/simmo/dev/goblint/sv-comp/goblint" -OPTS="--conf $GOBLINTDIR/conf/svcomp.json --set ana.specification $GOBLINTDIR/../sv-benchmarks/c/properties/unreach-call.prp bad.c --enable pre.enabled" +OPTS="--conf $GOBLINTDIR/conf/svcomp25.json --set ana.specification $GOBLINTDIR/../sv-benchmarks/c/properties/unreach-call.prp bad.c --enable pre.enabled" LOG="goblint.log" $GOBLINTDIR/goblint $OPTS -v &> $LOG diff --git a/scripts/sv-comp/Dockerfile b/scripts/sv-comp/Dockerfile new file mode 100644 index 0000000000..3f833bf038 --- /dev/null +++ b/scripts/sv-comp/Dockerfile @@ -0,0 +1,52 @@ +# just -opam tag because make setup will install ocaml compiler +FROM ocaml/opam:ubuntu-24.04-opam AS build +# make opam 2.4 default for make setup +RUN sudo ln -sf /usr/bin/opam-2.4 /usr/bin/opam + +RUN sudo apt-get update \ + && sudo apt-get install -y gcc-multilib chrpath wget zip +# update local opam repository because base image may be outdated +RUN cd /home/opam/opam-repository \ + && git pull origin master \ + && opam update -y + +# copy only files for make setup to cache docker layers without code changes +COPY --chown=opam make.sh goblint.opam goblint.opam.locked /home/opam/goblint/ +WORKDIR /home/opam/goblint/ +# unsafe-yes to allow opam to install depexts via apt unattended +RUN OPAMCONFIRMLEVEL=unsafe-yes ./make.sh setup + +# copy the rest +COPY --chown=opam . /home/opam/goblint +RUN ./scripts/sv-comp/archive.sh + +FROM ubuntu:24.04 AS smoketest-ubuntu + +# cannot use opam depext because no opam here, also additional preprocessing/header dependencies +# libgmp for zarith, libmpfr for apron, cpp for preprocessing, libc6 for pthread.h, libgcc for stddef.h +RUN apt-get update \ + && apt-get install -y unzip libgmp10 libmpfr6 cpp libc6-dev libc6-dev-i386 libgcc-13-dev lib32gcc-13-dev python3 \ + && rm -rf /var/lib/apt/lists/* + +WORKDIR /root +COPY --from=build /home/opam/goblint/scripts/sv-comp/goblint.zip . +RUN unzip goblint.zip + +WORKDIR /root/goblint +RUN ./smoketest.sh + +FROM registry.gitlab.com/sosy-lab/benchmarking/competition-scripts/user:2026 AS smoketest-competition + +RUN apt-get update \ + && apt-get install -y unzip \ + && rm -rf /var/lib/apt/lists/* + +WORKDIR /root +COPY --from=build /home/opam/goblint/scripts/sv-comp/goblint.zip . +RUN unzip goblint.zip + +WORKDIR /root/goblint +RUN ./smoketest.sh + +FROM scratch +COPY --from=build /home/opam/goblint/scripts/sv-comp/goblint.zip . diff --git a/scripts/sv-comp/archive.sh b/scripts/sv-comp/archive.sh index 33ea1b4368..3111216aed 100755 --- a/scripts/sv-comp/archive.sh +++ b/scripts/sv-comp/archive.sh @@ -4,7 +4,7 @@ make clean -git tag -m "SV-COMP 2025" svcomp25 +eval $(opam env) dune build --profile=release src/goblint.exe rm -f goblint @@ -19,24 +19,29 @@ cp _opam/share/apron/lib/liboctD.so lib/ cp _opam/share/apron/lib/libboxD.so lib/ cp _opam/share/apron/lib/libpolkaMPQ.so lib/ wget -O lib/LICENSE.APRON https://raw.githubusercontent.com/antoinemine/apron/master/COPYING +cp scripts/sv-comp/goblint_runner.py . +cp scripts/sv-comp/smoketest.sh . +cp -r scripts/sv-comp/smoketests . # done outside to ensure archive contains goblint/ directory cd .. rm goblint/scripts/sv-comp/goblint.zip -zip goblint/scripts/sv-comp/goblint.zip \ +zip -r goblint/scripts/sv-comp/goblint.zip \ goblint/goblint \ + goblint/goblint_runner.py \ goblint/lib/libapron.so \ goblint/lib/liboctD.so \ goblint/lib/libboxD.so \ goblint/lib/libpolkaMPQ.so \ goblint/lib/LICENSE.APRON \ - goblint/conf/svcomp25.json \ - goblint/conf/svcomp25-validate.json \ + goblint/conf/svcomp26/ \ goblint/lib/libc/stub/include/assert.h \ goblint/lib/goblint/runtime/include/goblint.h \ goblint/lib/libc/stub/src/stdlib.c \ goblint/lib/sv-comp/stub/src/sv-comp.c \ goblint/README.md \ - goblint/LICENSE + goblint/LICENSE \ + goblint/smoketest.sh \ + goblint/smoketests/ diff --git a/scripts/sv-comp/goblint_runner.py b/scripts/sv-comp/goblint_runner.py index d5aae51cd4..54f8f0b044 100755 --- a/scripts/sv-comp/goblint_runner.py +++ b/scripts/sv-comp/goblint_runner.py @@ -21,8 +21,8 @@ def __init__(self, logger): parser = argparse.ArgumentParser( description="""A facade in front of goblint to enable running a portfolio of configurations for SV-COMP. All args apart from --portfolio-conf/-p are passed on to the actual goblint calls. - The portfolio config file is a plaintext file whose lines each consist of goblint parameters, in particular including - --conf followed by a path to a goblint config file (relative to the goblint base dir, or absolute). + The portfolio config file is a plaintext file whose lines each consist of goblint parameters, in particular including + --conf followed by a path to a goblint config file (relative to the goblint base dir, or absolute). Goblint is run with each parameterset in order of specification as long as goblint produces an unknown verdict or reaches the end of the list. You may add comments to the portfolio config file by starting a line with #. """ @@ -35,13 +35,14 @@ def __init__(self, logger): self.configs = [] if conf_args.portfolio: + conf_args.portfolio = path.join(path.dirname(self.goblint_executable_path), conf_args.portfolio) if not path.exists(conf_args.portfolio): logger.error(f" Could not find portfolio conf file at {conf_args.portfolio}") exit(1) with open(conf_args.portfolio, "r") as conflist_file: self.configs = [c.strip() for c in conflist_file.readlines() if not c.strip().startswith("#")] logger.info(f"Loaded goblint configs: {", ".join(self.configs)}") - + def run_with_config(self, config_str): config_args = config_str.split(" ") args = [*config_args] + self.other_args @@ -70,7 +71,7 @@ def run(self): for i, config in enumerate(self.configs): logger.info(f"Starting config [{i}]") verdict, go_on = self.run_with_config(config) - if not go_on: + if not go_on: logger.info(f"Stopping portfolio sequence with verdict [{verdict}] after config [{i}]") break if go_on: diff --git a/scripts/sv-comp/smoketest.sh b/scripts/sv-comp/smoketest.sh new file mode 100755 index 0000000000..01f33eab5d --- /dev/null +++ b/scripts/sv-comp/smoketest.sh @@ -0,0 +1,48 @@ +#!/usr/bin/env bash + +set -e # Make script fail if any command fails. +set -o pipefail # Make pipes fail if any command in pipe fails. + + +# Print version for reference. +./goblint --version +# This also checks if all linked dependencies are available (glibc (correct version), Apron, ...), crashes otherwise. +# Also check if goblint_runner exists and runs. +./goblint_runner.py --version + + +# Run smoke tests in subdirectory for convenience. +cd smoketests/ +GOBLINT="../goblint_runner.py --portfolio-conf conf/svcomp26/seq.txt" +# This will also check if Goblint works when executed from different directory (finds Apron libs, conf, lib stubs), crashes otherwise. + + +# Check if architectures are supported (CIL Machdeps, C standard headers available for both) and return correct results. +# This is based on the cram test tests/regression/29-svcomp/36-svcomp-arch.t. +# There should be overflow on ILP32: +$GOBLINT --set ana.specification no-overflow.prp --set exp.architecture 32bit 36-svcomp-arch.c | grep "SV-COMP result: unknown" + +# There shouldn't be an overflow on LP64: +$GOBLINT --set ana.specification no-overflow.prp --set exp.architecture 64bit 36-svcomp-arch.c | grep "SV-COMP result: true" + + +# Check if basic data race analysis returns correct results. +$GOBLINT --set ana.specification no-data-race.prp --set exp.architecture 32bit 04-mutex_01-simple_rc.c | grep "SV-COMP result: unknown" +$GOBLINT --set ana.specification no-data-race.prp --set exp.architecture 32bit 04-mutex_02-simple_nr.c | grep "SV-COMP result: true" + + +# Check if witness validation returns correct results. +GOBLINT_VALIDATOR="../goblint_runner.py --portfolio-conf conf/svcomp26/seq-validate.txt" + +# From scratch verification actually succeeds for a variety of reasons (abortUnless analysis, wideningThresholds autotuner): +# This is not intentional. +$GOBLINT --set ana.specification unreach-call.prp --set exp.architecture 64bit mine2017-ex4.6.c | grep "SV-COMP result: true" + +# Correct invariant should be confirmed: +$GOBLINT_VALIDATOR --set ana.specification unreach-call.prp --set exp.architecture 64bit mine2017-ex4.6.c --set witness.yaml.unassume mine2017-ex4.6-witness-correct.yml --set witness.yaml.validate mine2017-ex4.6-witness-correct.yml | grep "SV-COMP result: true" + +# Imprecise invariant shouldn't be confirmed due to precision loss from unassuming it: +$GOBLINT_VALIDATOR --set ana.specification unreach-call.prp --set exp.architecture 64bit mine2017-ex4.6.c --set witness.yaml.unassume mine2017-ex4.6-witness-imprecise.yml --set witness.yaml.validate mine2017-ex4.6-witness-imprecise.yml | grep "SV-COMP result: unknown" + +# Incorrect invariant shouldn't be confirmed: +$GOBLINT_VALIDATOR --set ana.specification unreach-call.prp --set exp.architecture 64bit mine2017-ex4.6.c --set witness.yaml.unassume mine2017-ex4.6-witness-incorrect.yml --set witness.yaml.validate mine2017-ex4.6-witness-incorrect.yml | grep "SV-COMP result: unknown" diff --git a/scripts/sv-comp/smoketests/04-mutex_01-simple_rc.c b/scripts/sv-comp/smoketests/04-mutex_01-simple_rc.c new file mode 100644 index 0000000000..53899fe2cb --- /dev/null +++ b/scripts/sv-comp/smoketests/04-mutex_01-simple_rc.c @@ -0,0 +1,30 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2005-2021 University of Tartu & Technische Universität München +// +// SPDX-License-Identifier: MIT + +#include +#include + +int myglobal; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex2); + myglobal=myglobal+1; // RACE! + pthread_mutex_unlock(&mutex2); + pthread_join (id, NULL); + return 0; +} diff --git a/scripts/sv-comp/smoketests/04-mutex_02-simple_nr.c b/scripts/sv-comp/smoketests/04-mutex_02-simple_nr.c new file mode 100644 index 0000000000..dbf9c214fa --- /dev/null +++ b/scripts/sv-comp/smoketests/04-mutex_02-simple_nr.c @@ -0,0 +1,30 @@ +// This file is part of the SV-Benchmarks collection of verification tasks: +// https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +// +// SPDX-FileCopyrightText: 2005-2021 University of Tartu & Technische Universität München +// +// SPDX-License-Identifier: MIT + +#include +#include + +int myglobal; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; +pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + myglobal=myglobal+1; // NORACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex1); + myglobal=myglobal+1; // NORACE + pthread_mutex_unlock(&mutex1); + pthread_join (id, NULL); + return 0; +} diff --git a/scripts/sv-comp/smoketests/36-svcomp-arch.c b/scripts/sv-comp/smoketests/36-svcomp-arch.c new file mode 100644 index 0000000000..ea68ba187c --- /dev/null +++ b/scripts/sv-comp/smoketests/36-svcomp-arch.c @@ -0,0 +1,8 @@ +// CRAM +#include + +int main() { + long k = INT_MAX; + long n = k * k; + return 0; +} diff --git a/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-correct.yml b/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-correct.yml new file mode 100644 index 0000000000..b93c296c97 --- /dev/null +++ b/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-correct.yml @@ -0,0 +1,33 @@ +# This file is part of the SV-Benchmarks collection of verification tasks: +# https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +# +# SPDX-FileCopyrightText: 2023-2025 Simmo Saan +# +# SPDX-License-Identifier: MIT + +- entry_type: invariant_set + metadata: + format_version: "2.0" + uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941483 + creation_time: 2025-10-17T17:14:00Z + producer: + name: Simmo Saan + version: n/a + task: + input_files: + - mine2017-ex4.6.c + input_file_hashes: + mine2017-ex4.6.c: 543af0d5de8128e2a70ef5165e255b68288cac9b22ac9c5f5408c2a6cc1efe34 + specification: G ! call(reach_error()) + data_model: LP64 + language: C + content: + - invariant: + type: loop_invariant + location: + file_name: mine2017-ex4.6.c + line: 11 + column: 3 + function: main + value: 0 <= x && x <= 40 + format: c_expression diff --git a/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-imprecise.yml b/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-imprecise.yml new file mode 100644 index 0000000000..02cec2bc2a --- /dev/null +++ b/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-imprecise.yml @@ -0,0 +1,33 @@ +# This file is part of the SV-Benchmarks collection of verification tasks: +# https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +# +# SPDX-FileCopyrightText: 2023-2025 Simmo Saan +# +# SPDX-License-Identifier: MIT + +- entry_type: invariant_set + metadata: + format_version: "2.0" + uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941484 + creation_time: 2025-10-17T17:14:00Z + producer: + name: Simmo Saan + version: n/a + task: + input_files: + - mine2017-ex4.6.c + input_file_hashes: + mine2017-ex4.6.c: 543af0d5de8128e2a70ef5165e255b68288cac9b22ac9c5f5408c2a6cc1efe34 + specification: G ! call(reach_error()) + data_model: LP64 + language: C + content: + - invariant: + type: loop_invariant + location: + file_name: mine2017-ex4.6.c + line: 11 + column: 3 + function: main + value: 0 <= x && x <= 80 + format: c_expression diff --git a/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-incorrect.yml b/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-incorrect.yml new file mode 100644 index 0000000000..73002b9983 --- /dev/null +++ b/scripts/sv-comp/smoketests/mine2017-ex4.6-witness-incorrect.yml @@ -0,0 +1,33 @@ +# This file is part of the SV-Benchmarks collection of verification tasks: +# https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks +# +# SPDX-FileCopyrightText: 2023-2025 Simmo Saan +# +# SPDX-License-Identifier: MIT + +- entry_type: invariant_set + metadata: + format_version: "2.0" + uuid: 0e84a9de-b9f6-44dd-ab8d-ebdeca941485 + creation_time: 2025-10-17T17:14:00Z + producer: + name: Simmo Saan + version: n/a + task: + input_files: + - mine2017-ex4.6.c + input_file_hashes: + mine2017-ex4.6.c: 543af0d5de8128e2a70ef5165e255b68288cac9b22ac9c5f5408c2a6cc1efe34 + specification: G ! call(reach_error()) + data_model: LP64 + language: C + content: + - invariant: + type: loop_invariant + location: + file_name: mine2017-ex4.6.c + line: 11 + column: 3 + function: main + value: 20 <= x && x <= 40 + format: c_expression diff --git a/scripts/sv-comp/smoketests/mine2017-ex4.6.c b/scripts/sv-comp/smoketests/mine2017-ex4.6.c new file mode 100644 index 0000000000..fb7a30880b --- /dev/null +++ b/scripts/sv-comp/smoketests/mine2017-ex4.6.c @@ -0,0 +1,18 @@ +// Source: Antoine Miné: "Tutorial on static inference of numeric invariants by abstract interpretation", FTPL 2017. +// Example 4.6. + +#include +extern void abort(void); +void reach_error() { assert(0); } +void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } } + +int main() { + int x = 40; + while (x != 0) { + __VERIFIER_assert(x <= 40); + x--; + __VERIFIER_assert(x >= 0); + } + __VERIFIER_assert(x == 0); + return 0; +} diff --git a/scripts/sv-comp/smoketests/no-data-race.prp b/scripts/sv-comp/smoketests/no-data-race.prp new file mode 100644 index 0000000000..e9812e8dff --- /dev/null +++ b/scripts/sv-comp/smoketests/no-data-race.prp @@ -0,0 +1,2 @@ +CHECK( init(main()), LTL(G ! data-race) ) + diff --git a/scripts/sv-comp/smoketests/no-overflow.prp b/scripts/sv-comp/smoketests/no-overflow.prp new file mode 100644 index 0000000000..26c5bded7a --- /dev/null +++ b/scripts/sv-comp/smoketests/no-overflow.prp @@ -0,0 +1,2 @@ +CHECK( init(main()), LTL(G ! overflow) ) + diff --git a/scripts/sv-comp/smoketests/unreach-call.prp b/scripts/sv-comp/smoketests/unreach-call.prp new file mode 100644 index 0000000000..7ae12e84e7 --- /dev/null +++ b/scripts/sv-comp/smoketests/unreach-call.prp @@ -0,0 +1,2 @@ +CHECK( init(main()), LTL(G ! call(reach_error())) ) + diff --git a/tests/sv-comp/dune.inc b/tests/sv-comp/dune.inc index 06d9e23b10..689f97ebf3 100644 --- a/tests/sv-comp/dune.inc +++ b/tests/sv-comp/dune.inc @@ -12,7 +12,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -34,7 +34,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -56,7 +56,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -78,7 +78,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -100,7 +100,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -122,7 +122,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -144,7 +144,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -166,7 +166,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -188,7 +188,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -210,7 +210,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -232,7 +232,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -254,7 +254,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -276,7 +276,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -298,7 +298,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -320,7 +320,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -342,7 +342,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -364,7 +364,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -386,7 +386,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -408,7 +408,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -430,7 +430,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -452,7 +452,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -474,7 +474,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -496,7 +496,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -518,7 +518,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -540,7 +540,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -562,7 +562,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -584,7 +584,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -606,7 +606,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -628,7 +628,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -650,7 +650,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -672,7 +672,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -694,7 +694,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -716,7 +716,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -738,7 +738,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -760,7 +760,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -782,7 +782,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -804,7 +804,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -826,7 +826,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -848,7 +848,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -870,7 +870,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -892,7 +892,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -914,7 +914,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) @@ -936,7 +936,7 @@ (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %{prop} %{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %{target} (run graph-easy --as=boxart arg.dot))))) diff --git a/tests/sv-comp/gen/gen.ml b/tests/sv-comp/gen/gen.ml index 2b2cbfcdd3..a8ad72be67 100644 --- a/tests/sv-comp/gen/gen.ml +++ b/tests/sv-comp/gen/gen.ml @@ -19,7 +19,7 @@ let generate_rule c_dir_file = (action (progn (ignore-outputs - (run goblint --conf svcomp.json --disable ana.autotune.enabled --set ana.specification %%{prop} %%{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) + (run goblint --conf svcomp25.json --disable ana.autotune.enabled --set ana.specification %%{prop} %%{c} --enable exp.arg.uncil --enable exp.arg.stack --enable exp.arg.enabled --set exp.arg.dot.path arg.dot --set exp.arg.dot.node-label empty)) (with-outputs-to %%{target} (run graph-easy --as=boxart arg.dot)))))