diff --git a/.gitattributes b/.gitattributes
index 91434116d050a224e0f676a68ea47b63279057e0..81fb7ae21dcd777a52224de02ddba38cd050a364 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -166,13 +166,13 @@ README* header_spec=.ignore
/bin/sed_get_* header_spec=.ignore
-/devel_tools/docker/*.template header_spec=.ignore
+/dev/docker/*.template header_spec=.ignore
# TODO: header_spec=JCF_LGPL_2_only
-/devel_tools/size.mli header_spec=.ignore
-/devel_tools/size.ml header_spec=.ignore
-/devel_tools/size_states.ml header_spec=.ignore
-/devel_tools/size_states.mli header_spec=.ignore
+/dev/size.mli header_spec=.ignore
+/dev/size.ml header_spec=.ignore
+/dev/size_states.ml header_spec=.ignore
+/dev/size_states.mli header_spec=.ignore
/doc/CC-BY-SA-4.0 header_spec=.ignore
/doc/CHANGES.obfuscator header_spec=.ignore
@@ -220,7 +220,7 @@ README* header_spec=.ignore
/nix/frama-c-public/known_hosts header_spec=.ignore
/nix/sources.json header_spec=.ignore
-/ptests/tests/**/* header_spec=.ignore
+/tools/ptests/tests/**/* header_spec=.ignore
/share/framac.vim header_spec=.ignore
/share/META.frama-c header_spec=.ignore
@@ -337,7 +337,7 @@ README* header_spec=.ignore
/bin/frama-c* header_spec=CEA_LGPL
/doc/code/*.txt header_spec=CEA_LGPL
-/devel_tools/git-hooks/pre-commit header_spec=CEA_LGPL
+/dev/git-hooks/pre-commit header_spec=CEA_LGPL
/headers/headache_config.txt header_spec=CEA_LGPL
/headers/*.sh header_spec=CEA_LGPL_OR_PROPRIETARY
diff --git a/.gitignore b/.gitignore
index 0c9a3ffad1279180824a46972c05496b083c2975..29cae708d2d8f51474e32144a5d7b340d123060f 100644
--- a/.gitignore
+++ b/.gitignore
@@ -59,11 +59,10 @@ autom4te.cache
/tests/crowbar/mutable
/tests/crowbar/output-*
/tests/crowbar/test_ghost_cfg
-/tests/spec/preprocess_dos.c
/tests/*/*.opt
-/devel_tools/fc-time
-/devel_tools/fc-memuse
+/dev/fc-time
+/dev/fc-memuse
/bin/ocamldep_transitive_closure
#share
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 91148379f8623ed1e2cec1467b3273ecd2f1f82f..fa98eccd8623839fca158dfb0ac035d2583ce5ae 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -1,9 +1,13 @@
+################################################################################
+### STAGES
+
stages:
+ - prepare
- build
- tests
- distrib
- compatibility
- - make_public
+ - publish
################################################################################
### DEFAULT JOB PARAMETERS
@@ -17,23 +21,44 @@ default:
variables:
DEFAULT: "feature/bobot/jbuilder"
- OCAML: "4_12"
-# CURRENT: $CI_COMMIT_REF_NAME
-# FRAMA_CI_OPT: "--override frama-c:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ OCAML: "4.11"
+ PUBLISH: "no"
################################################################################
-### BUILD
+### PREPARE
check-no-old-frama-c:
- stage: build
+ stage: prepare
script:
- (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a HEAD)
- git merge-base --is-ancestor a35d2118fe6999dddce9e1847eff626fae9cc37c HEAD
+.build_template: &do_not_stop_pipeline_template
+ stage: prepare
+ interruptible: false
+ script:
+ - echo "This pipeline won't be interrupted"
+
+unstoppable-pipeline:
+ <<: *do_not_stop_pipeline_template
+ only:
+ variables:
+ - $DEFAULT == $CI_COMMIT_BRANCH
+
+do-not-stop-pipeline:
+ <<: *do_not_stop_pipeline_template
+ when: manual
+ except:
+ variables:
+ - $DEFAULT == $CI_COMMIT_BRANCH
+
+################################################################################
+### BUILD
+
frama-c:
stage: build
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.frama-c
+ - ./nix/build-proxy.sh frama-c
artifacts:
when: on_failure
paths:
@@ -58,147 +83,94 @@ ivette:
################################################################################
### TESTS
-acsl-importer:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh ACSL-importer
-
-caveat-importer:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh Caveat-importer
-
-cfp:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh context-from-precondition
e-acsl-tests:
stage: tests
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.e-acsl-tests
-
-# EVA
+ - ./nix/build-proxy.sh e-acsl-tests
.build_template: &eva_template
stage: tests
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.eva-$CONFIG-tests
+ - ./nix/build-proxy.sh eva-$CONFIG-tests
eva-default-tests:
variables:
CONFIG: "default"
<<: *eva_template
-eva-bitwise-tests:
- variables:
- CONFIG: "bitwise"
- <<: *eva_template
-
-eva-equality-tests:
- variables:
- CONFIG: "equality"
- <<: *eva_template
-
-eva-gauges-tests:
- variables:
- CONFIG: "gauges"
- <<: *eva_template
-
-eva-multidim-tests:
- variables:
- CONFIG: "multidim"
+eva-domains:
<<: *eva_template
-
-eva-octagon-tests:
- variables:
- CONFIG: "octagon"
- <<: *eva_template
-
-eva-symblocs-tests:
- variables:
- CONFIG: "symblocs"
- <<: *eva_template
-
-frama-clang:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh frama-clang
-
-genassigns:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh genassigns
+ parallel:
+ matrix:
+ - CONFIG: ["bitwise","equality","gauges","multidim","octagon","symblocs"]
kernel-tests:
stage: tests
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.kernel-tests
-
-linea-cabs:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh linea-cabs
-
-metacsl:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh meta
-
-mthread:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh mthread
+ - ./nix/build-proxy.sh kernel-tests
plugins-tests:
stage: tests
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.plugins-tests
+ - ./nix/build-proxy.sh plugins-tests
-security:
- stage: tests
- script:
- - ./nix/external-plugin-ci.sh security
-
-volatile:
+wp-tests:
stage: tests
script:
- - ./nix/external-plugin-ci.sh Volatile
+ - ./nix/build-proxy.sh wp-tests
-wp-tests:
+external-plugins:
stage: tests
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.wp-tests
+ - ./nix/external-plugin-ci.sh $PLUGIN
+ parallel:
+ matrix:
+ - PLUGIN: [
+ "ACSL-importer",
+ "Caveat-importer",
+ "context-from-precondition",
+ "frama-clang",
+ "genassigns",
+ "linea-cabs",
+ "meta",
+ "mthread",
+ "security",
+ "Volatile"
+ ]
################################################################################
### DISTRIB
# API documentation
-.build_template: &api-doc
+.build_template: &api_doc_template
stage: distrib
+ variables:
+ OUT: "api"
script:
- - nix-build -o api nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.api-doc
+ - ./nix/build-proxy.sh api-doc
api-doc-default: # Check that we successfully build but no artifact
- <<: *api-doc
+ <<: *api_doc_template
api-doc-artifact: # Note: the Nix store avoids rebuilding
- <<: *api-doc
+ <<: *api_doc_template
artifacts:
paths:
- api/frama-c-api.tar.gz
expire_in: 7 days
when: manual
-api-doc-scheduled: # Keep artifact for master branch each night
- <<: *api-doc
+api-doc-scheduled: # Keep artifact for published branch each night
+ <<: *api_doc_template
artifacts:
paths:
- api/frama-c-api.tar.gz
expire_in: 7 days # Note: the LAST artifact of the ref is always kept
only:
- - schedules
+ variables:
+ - $PUBLISH == "yes"
# Build distribution tarball
@@ -209,8 +181,7 @@ build-distrib-tarball:
CI_LINK: "yes"
HDRCK: "frama-c-hdrck"
script:
- - nix-shell nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.frama-c-checkers-shell
- --run 'autoconf && ./devel_tools/make-distrib.sh'
+ - ./nix/shell-checkers.sh "autoconf && ./dev/make-distrib.sh"
artifacts:
paths:
- ./*.tar.gz
@@ -223,9 +194,7 @@ header-check:
variables:
FRAMAC_HDRCK: ""
script:
- - ls -la
- - nix-shell nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.frama-c-checkers-shell
- --run 'make -f share/Makefile.headers check-headers'
+ - ./nix/shell-checkers.sh "make -f share/Makefile.headers check-headers"
# Lint files
@@ -234,18 +203,19 @@ lint:
variables:
LINT_MAKEFILE: "share/Makefile.linting"
script:
- - nix-shell nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.frama-c-checkers-shell
- --run 'make -f share/Makefile.linting lint'
+ - ./nix/shell-checkers.sh "make -f share/Makefile.linting lint"
# Manuals
-.build_template: &manuals
+.build_template: &manuals_template
stage: distrib
+ variables:
+ OUT: "manuals"
script:
- - nix-build -o manuals nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.manuals
+ - ./nix/build-proxy.sh manuals
manuals:
- <<: *manuals
+ <<: *manuals_template
when: manual
artifacts:
paths:
@@ -269,76 +239,136 @@ internal:
internal_nightly:
<<: *internal_template
+ # The Opam target may affect this job
+ timeout: 2h
only:
- schedules
# OCaml versions
-.build_template: &ocaml
+ocaml-versions:
stage: compatibility
script:
- - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.default-config-tests
+ - ./nix/build-proxy.sh default-config-tests
+ parallel:
+ matrix:
+ - OCAML: ["4.08", "4.13"]
+ # in schedules, each OCAML is tested in its own complete pipeline
+ except:
+ - schedules
-# ocaml-4.11:
-# variables:
-# OCAML: "4_11"
-# <<: *ocaml
+# Opam pin
-# ocaml-4.13:
-# variables:
-# OCAML: "4_13"
-# <<: *ocaml
+.build_template: &opam_template
+ stage: compatibility
+ image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
+ script:
+ - opam pin . -n
+ - opam depext frama-c --with-test
+ - opam install --jobs 2 frama-c --with-test
+ tags:
+ - docker
-src-distrib-tests:
+opam-pin:
+ <<: *opam_template
+ when: manual
+
+opam-pin-nightly:
+ <<: *opam_template
+ only:
+ - schedules
+ allow_failure: true
+
+# TODO: Enable this rule later:
+#
+# opam-pin-minimal:
+# variables:
+# OPAMSOLVERTIMEOUT: "500"
+# OPAMCRITERIA: "+count[version-lag,solution]"
+# OPAMEXTERNALSOLVER: "builtin-0install"
+# stage: prepare
+# image: 'ocaml/opam:ubuntu-20.04-ocaml-$OCAML'
+# script:
+# - sudo ln -f /usr/bin/opam-2.1 /usr/bin/opam
+# - opam --version
+# - opam init --reinit -ni
+# - opam pin . -n
+# - opam depext frama-c --with-test
+# - opam install --jobs 2 frama-c --with-test
+# tags:
+# - docker
+
+# Distrib
+
+.build_template: &src_distrib_tests_template
stage: compatibility
+ variables:
+ DIR: "extracted"
script:
- - mkdir extracted && tar -xzf frama-c.tar.gz --strip-components 1 -C ./extracted
- - nix-build extracted/nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.src-distrib-tests
+ - mkdir $DIR && tar -xzf frama-c.tar.gz --strip-components 1 -C ./extracted
+ - ./nix/build-proxy.sh src-distrib-tests
+
+src-distrib-tests:
+ <<: *src_distrib_tests_template
+ except:
+ - schedules
+
+src-distrib-tests-nightly:
+ <<: *src_distrib_tests_template
+ # The Opam target may affect this job
+ timeout: 2h
+ only:
+ - schedules
################################################################################
-### PUBLIC
+### PUBLISH
-# make_public stage is used to push the current master branch of Frama-C and
+# publish stage is used to push the current master branch of Frama-C and
# associated plugins from the internal frama-c group to the public pub group.
-# For that, it uses the 'frama-c to frama-c-public' deploy key. Thus, to publish
+#
+# For that, it uses the 'frama-c to frama-c-public' publish key. Thus, to publish
# a new plugin (while keeping its main repository internal), you can add a new
# target to this stage, adapting the script for MetAcsl or Frama-Clang to your
# own plugin.
-# You must also activate the deploy key on both frama-c/my_plugin
+#
+# You must also activate the publish key on both frama-c/my_plugin
# and pub/my_plugin repositories (the former should be read-only, the latter
-# must provide write access to the deploy key).
+# must provide write access to the publish key).
# Do not forget to trigger the target only on schedules, so that all public
# repositories stay synchronized.
-make_public:
- stage: make_public
+publish-frama-c:
+ stage: publish
script:
- (! git merge-base --is-ancestor a1e186c68a6418a53b3dc06237f49e8dcbf75f4a origin/master)
- echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- GIT_SSH=nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git push git@git.frama-c.com:pub/frama-c.git origin/master:refs/heads/master
only:
- - schedules
+ variables:
+ - $PUBLISH == "yes"
interruptible: false
-make_public_meta:
- stage: make_public
+publish-meta:
+ stage: publish
script:
- echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/meta.git nix/frama-c-public/meta
- GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/meta push git@git.frama-c.com:pub/meta origin/master:refs/heads/master
only:
- - schedules
+ variables:
+ - $PUBLISH == "yes"
interruptible: false
-make_public_fclang:
- stage: make_public
+publish-fclang:
+ stage: publish
script:
- echo "$FRAMA_C_PUBLIC_SSH_PRIVATE_KEY" | nix run -f channel:nixos-19.03 coreutils --command base64 -d > nix/frama-c-public/id_ed25519
- nix run -f channel:nixos-19.03 coreutils --command chmod 400 nix/frama-c-public/id_ed25519
- GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git clone git@git.frama-c.com:frama-c/frama-clang.git nix/frama-c-public/frama-clang
- GIT_SSH=$PWD/nix/frama-c-public/ssh.sh nix run -f channel:nixos-19.03 openssh --command git -C nix/frama-c-public/frama-clang push git@git.frama-c.com:pub/frama-clang origin/master:refs/heads/master
only:
- - schedules
+ variables:
+ - $PUBLISH == "yes"
interruptible: false
diff --git a/Makefile b/Makefile
index 41c1b6b039f502b6045a85fae1d8efcba55e3e92..b3735d0559e79e224576485d3d512e96448481ac 100644
--- a/Makefile
+++ b/Makefile
@@ -39,6 +39,12 @@ endif
DUNE_DISPLAY?=progress
DUNE_BUILD_OPTS+=--display $(DUNE_DISPLAY)
+# PTESTS SRC
+FRAMAC_PTESTS_SRC:=tools/ptests
+
+# HDRCK SRC
+FRAMAC_HDRCK_SRC:=tools/hdrck
+
###################
# Frama-C Version #
###################
@@ -77,7 +83,8 @@ config.sed: VERSION share/Makefile.config share/Makefile.common Makefile configu
clean:: purge-tests # to be done before a "dune" command
dune clean
- dune clean --root ptests
+ dune clean --root $(FRAMAC_PTESTS_SRC)
+ dune clean --root $(FRAMAC_HDRCK_SRC)
rm -rf _build .merlin config.sed autom4te.cache
########################################################################
@@ -144,10 +151,10 @@ include share/Makefile.headers
################################
# PTESTS is internal
-FRAMAC_PTESTS:=ptests/ptests.exe
+FRAMAC_PTESTS:=$(FRAMAC_PTESTS_SRC)/ptests.exe
# WTESTS is internal
-FRAMAC_WTESTS:=ptests/wtests.exe
+FRAMAC_WTESTS:=$(FRAMAC_PTESTS_SRC)/wtests.exe
# Frama-C also have ptest directories in plugins, so we do not use default
PTEST_ALL_DIRS:=tests $(wildcard src/plugins/*/tests)
diff --git a/bin/test.sh b/bin/test.sh
index 24b8d54c77ca2ded2b060d09461960a87b23c80f..a08a3d356c3c02e3929a6f76737e70d60628ee07 100755
--- a/bin/test.sh
+++ b/bin/test.sh
@@ -30,8 +30,8 @@ TESTS=
SAVE=
DUNE_OPT=
-DUNE_LOG=.test-errors.log
-
+DUNE_LOG=./.test-errors.log
+CACHEDIR=./.wp-cache
FRAMAC_WP_CACHE_GIT=git@git.frama-c.com:frama-c/wp-cache.git
# --------------------------------------------------------------------------
@@ -130,14 +130,18 @@ function SetEnv
FRAMAC_WP_CACHE=offline
Echo "Set FRAMAC_WP_CACHE=$FRAMAC_WP_CACHE"
fi
+
if [ "$FRAMAC_WP_QUALIF" != "" ]; then
- FRAMAC_WP_CACHEDIR=$FRAMAC_WP_QUALIF
- else
- if [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
- FRAMAC_WP_CACHEDIR=./.wp-cache
- Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
- fi
+ FRAMAC_WP_CACHEDIR="$FRAMAC_WP_QUALIF"
+ Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
+ elif [ "$FRAMAC_WP_CACHEDIR" = "" ]; then
+ FRAMAC_WP_CACHEDIR="$CACHEDIR"
+ Echo "Set FRAMAC_WP_CACHEDIR=$FRAMAC_WP_CACHEDIR"
fi
+
+ [ ! -f "$FRAMAC_WP_CACHEDIR" ] || [ -d "$FRAMAC_WP_CACHEDIR" ] \
+ || Error "$FRAMAC_WP_CACHEDIR is not a directory"
+
}
function CloneCache
diff --git a/default.nix b/default.nix
deleted file mode 100644
index e64150378a86d1a128776f31ba1f5912ea77af15..0000000000000000000000000000000000000000
--- a/default.nix
+++ /dev/null
@@ -1,15 +0,0 @@
-# standalone derivation, for nix-build, nix-shell, etc
-{ pkgs ? import <nixpkgs> {} }:
-let
- src = builtins.fetchGit {
- "url" = ./.git;
- "name" = "frama-c";
- "rev" = "ffa925f404779a3a0c4aacff5bd78b1c502def11";
- "ref" = "test-nix-fetchGit";
- };
- in
-
-pkgs.callPackage ./nix/default.nix {
- opam2nix = pkgs.callPackage ../Frama-CI/opam2nix-packages.nix {};
- src = src;
-}
diff --git a/devel_tools/docker/.gitignore b/dev/docker/.gitignore
similarity index 100%
rename from devel_tools/docker/.gitignore
rename to dev/docker/.gitignore
diff --git a/devel_tools/docker/Dockerfile.template b/dev/docker/Dockerfile.template
similarity index 100%
rename from devel_tools/docker/Dockerfile.template
rename to dev/docker/Dockerfile.template
diff --git a/devel_tools/docker/Makefile b/dev/docker/Makefile
similarity index 100%
rename from devel_tools/docker/Makefile
rename to dev/docker/Makefile
diff --git a/devel_tools/docker/README.md b/dev/docker/README.md
similarity index 100%
rename from devel_tools/docker/README.md
rename to dev/docker/README.md
diff --git a/devel_tools/docker/cvc4.template b/dev/docker/cvc4.template
similarity index 100%
rename from devel_tools/docker/cvc4.template
rename to dev/docker/cvc4.template
diff --git a/devel_tools/docker/env.template b/dev/docker/env.template
similarity index 100%
rename from devel_tools/docker/env.template
rename to dev/docker/env.template
diff --git a/devel_tools/docker/z3.template b/dev/docker/z3.template
similarity index 100%
rename from devel_tools/docker/z3.template
rename to dev/docker/z3.template
diff --git a/devel_tools/duplicates.pl b/dev/duplicates.pl
similarity index 100%
rename from devel_tools/duplicates.pl
rename to dev/duplicates.pl
diff --git a/devel_tools/frama-c-callgrind.sh b/dev/frama-c-callgrind.sh
similarity index 100%
rename from devel_tools/frama-c-callgrind.sh
rename to dev/frama-c-callgrind.sh
diff --git a/devel_tools/git-hooks/pre-commit b/dev/git-hooks/pre-commit
similarity index 100%
rename from devel_tools/git-hooks/pre-commit
rename to dev/git-hooks/pre-commit
diff --git a/devel_tools/make-distrib.sh b/dev/make-distrib.sh
similarity index 100%
rename from devel_tools/make-distrib.sh
rename to dev/make-distrib.sh
diff --git a/devel_tools/ocamldep_transitive_closure.ml b/dev/ocamldep_transitive_closure.ml
similarity index 100%
rename from devel_tools/ocamldep_transitive_closure.ml
rename to dev/ocamldep_transitive_closure.ml
diff --git a/devel_tools/size.ml b/dev/size.ml
similarity index 100%
rename from devel_tools/size.ml
rename to dev/size.ml
diff --git a/devel_tools/size.mli b/dev/size.mli
similarity index 100%
rename from devel_tools/size.mli
rename to dev/size.mli
diff --git a/devel_tools/size_states.ml b/dev/size_states.ml
similarity index 100%
rename from devel_tools/size_states.ml
rename to dev/size_states.ml
diff --git a/dune b/dune
index 5f80722cb4c32143ab369ee973edbbb397b3a6e3..8a20f109b8dfb2519252444963f97cc385f095f8 100644
--- a/dune
+++ b/dune
@@ -20,4 +20,4 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(dirs src ptests headers tests share bin)
+(dirs src tools tests headers share bin)
diff --git a/dune-project b/dune-project
index 25c7d8d3861402277fd5f80171c78b6613921bb7..acebea6b4983d92807c188bcd83d32ef624b4e98 100644
--- a/dune-project
+++ b/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/headers/dune b/headers/dune
index 769d8ae8711541535935fd8e38b2ea856eb18295..6f261cf6c77f34f52070c1a375cd5d568ec3ce41 100644
--- a/headers/dune
+++ b/headers/dune
@@ -20,9 +20,7 @@
;; ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-(executable
- (public_name frama-c-hdrck)
- (name hdrck)
- (modules hdrck)
- (libraries unix str)
-)
+(install
+ (package frama-c)
+ (section (site (frama-c share)))
+ (files (headache_config.txt as headache_config.txt)))
diff --git a/headers/headache_config.txt b/headers/headache_config.txt
index 6d7fb6b7ee0fcefd6790a157081f1706737149f7..3c6299eab995ebeece9333b5329894ca69435b4c 100644
--- a/headers/headache_config.txt
+++ b/headers/headache_config.txt
@@ -159,6 +159,7 @@
#########
| ".*\.tex" -> frame open: "%" line: "%" close: "%"
| ".*\.sty" -> frame open: "%" line: "%" close: "%"
+| ".*\.bib" -> frame open: "%" line: "%" close: "%"
########
# HTML #
diff --git a/nix/build-proxy.sh b/nix/build-proxy.sh
new file mode 100755
index 0000000000000000000000000000000000000000..a71c04d4a67037f3710d491dbd1b3f60012404be
--- /dev/null
+++ b/nix/build-proxy.sh
@@ -0,0 +1,52 @@
+#!/usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# OCAML must be set to the right version of OCAML (format: N_MM or N.MM)
+
+if [[ $# != 1 ]];
+then
+ cat <<EOF
+usage: OCAML=N_MM $0 <nix-target>
+ $0 <nix-target> run the nix-build command for this target
+EOF
+ exit 2
+fi
+
+if [ -z ${OCAML+x} ]; then
+ echo "OCAML variable must be set to a version of OCaml"
+ exit 2
+fi
+
+# Normalize version for Nix
+OCAML=${OCAML/./_}
+
+OUTOPT=""
+if [ ! -z ${OUT+x} ]; then
+ OUTOPT="-o $OUT"
+fi
+
+if [ -z ${DIR+x} ]; then
+ DIR="."
+fi
+
+nix-build $OUTOPT $DIR/nix/pkgs.nix -A ocaml-ng.ocamlPackages_$OCAML.$1
diff --git a/nix/default.nix b/nix/default.nix
deleted file mode 100644
index 4e146ccd47d633f8737f0183882061de862ed84a..0000000000000000000000000000000000000000
--- a/nix/default.nix
+++ /dev/null
@@ -1,396 +0,0 @@
-# paramaterised derivation with dependencies injected (callPackage style)
-{ pkgs, stdenv, src ? ../., opam2nix, ocaml ? pkgs.ocaml-ng.ocamlPackages_4_08.ocaml, plugins ? { } }:
-
-let mydir = builtins.getEnv("PWD");
- mk-opam-selection = { name, opamSrc?{}, ... }: {
- inherit ocaml;
- src = opamSrc;
- selection = "${mydir}/${name}-${ocaml.version}-opam-selection.nix";
- };
- opamPackages =
- [ "ocamlfind=1.9.3" "zarith" "ocamlgraph" "yojson=1.7.0" "zmq"
- "ppx_import" "ppx_deriving" "ppx_deriving_yojson"
- "coq=8.13.0" "alt-ergo=2.2.0"
- "why3=1.5.0" "why3-coq=1.5.0"
- "menhir=20211012" "dune=2.9.1"
- "easy-format=1.3.2"
- "biniou=1.2.1"
- ];
- # only pure nix packages. See mk_deriv below for adding opam2nix packages
- mk_buildInputs = { nixPackages ? [] } :
- [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file pkgs.which pkgs.dos2unix] ++ nixPackages;
- # Extends the call to stdenv.mkDerivation with parameters common for all
- # frama-c derivations
- mk_deriv = args:
- let my_opam_packages =
- if args?opamPackages then
- opamPackages ++ args.opamPackages
- else opamPackages
- ;
- opam-selection = mk-opam-selection args;
- buildInputs = args.buildInputs ++ opam2nix.buildInputs opam-selection;
- in
- stdenv.mkDerivation (
- args //
- {
- # Disable Nix's GCC hardening
- hardeningDisable = [ "all" ];
- inherit buildInputs;
- })
- //
- { gen-opam-selection =
- opam2nix.resolve opam-selection my_opam_packages; }
- ;
-in
-
-pkgs.lib.makeExtensible
-(self: {
- inherit src mk_buildInputs opamPackages mk_deriv;
- buildInputs = mk_buildInputs {};
- installed = self.main.out;
- main = mk_deriv {
- name = "frama-c";
- src = self.src;
- buildInputs =self.buildInputs;
- outputs = [ "out" "build_dir" ];
- postPatch = ''
- patchShebangs .
- '';
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make -j 4
- '';
- installPhase = ''
- make install
- mkdir -p $build_dir
- tar -cf $build_dir/dir.tar .
- pwd > $build_dir/old_pwd
- '';
- setupHook = pkgs.writeText "setupHook.sh" ''
- addFramaCPath () {
- if test -d "$1/lib/frama-c/plugins"; then
- export FRAMAC_PLUGIN="''${FRAMAC_PLUGIN:-}''${FRAMAC_PLUGIN:+:}$1/lib/frama-c/plugins"
- export OCAMLPATH="''${OCAMLPATH:-}''${OCAMLPATH:+:}$1/lib/frama-c/plugins"
- fi
-
- if test -d "$1/lib/frama-c"; then
- export OCAMLPATH="''${OCAMLPATH:-}''${OCAMLPATH:+:}$1/lib/frama-c"
- fi
-
- if test -d "$1/share/frama-c/"; then
- export FRAMAC_EXTRA_SHARE="''${FRAMAC_EXTRA_SHARE:-}''${FRAMAC_EXTRA_SHARE:+:}$1/share/frama-c"
- fi
-
- }
-
- addEnvHooks "$targetOffset" addFramaCPath
- '';
- };
-
- lint = mk_deriv {
- name = "frama-c-lint";
- src = self.src;
- opamPackages = [ "ocp-indent=1.8.1" "headache=1.05"];
- buildInputs =
- self.mk_buildInputs { nixPackages = [ pkgs.bc pkgs.clang_10 ]; };
- outputs = [ "out" ];
- postPatch = ''
- patchShebangs .
- '';
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make lint
- make stats-lint
- STRICT_HEADERS=yes make check-headers
- '';
- installPhase = ''
- true
- '';
- };
-
- doc = mk_deriv {
- name = "frama-c-doc";
- buildInputs = self.buildInputs;
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postPatch = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make doc
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main";};
-
- tests = mk_deriv {
- name = "frama-c-test";
- buildInputs = self.buildInputs;
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- make tests -j4 PTESTS_OPTS="-error-code -j 4"
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- build-distrib-tarball = mk_deriv {
- name = "frama-c-build-distrib-tarball";
- src = self.src;
- buildInputs = self.buildInputs;
- opamPackages = [ "headache=1.05" ];
- outputs = [ "out" ];
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make DISTRIB="frama-c-archive" src-distrib
- tar -zcf frama-c-tests-archive.tar.gz tests src/plugins/*/tests
- '';
- installPhase = ''
- tar -C $out --strip-components=1 -xzf frama-c-archive.tar.gz
- tar -C $out -xzf frama-c-tests-archive.tar.gz
- '';
- };
-
- build-from-distrib-tarball = mk_deriv {
- name = "frama-c-build-from-distrib-tarball";
- doCheck = true;
- buildInputs = self.buildInputs;
- opamPackages = self.build-distrib-tarball.opamPackages;
- src = self.build-distrib-tarball.out ;
- outputs = [ "out" ];
- postPatch = ''
- patchShebangs .
- '';
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make -j 4
- '';
- checkPhase = ''
- make clean_share_link
- make create_share_link
- make tests -j4 PTESTS_OPTS="-error-code -j 4"
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "build-distrib-tarball"; };
-
- wp-qualif = mk_deriv {
- name = "frama-c-wp-qualif";
- buildInputs = self.mk_buildInputs { };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- make src/plugins/wp/tests/test_config_qualif
- export FRAMAC_WP_CACHE=replay
- export FRAMAC_WP_CACHEDIR=${plugins.wp-cache.src}
- bin/ptests.opt -error-code -config qualif src/plugins/wp/tests
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- aorai-prove = mk_deriv {
- name = "frama-c-aorai-prove";
- buildInputs = self.mk_buildInputs { };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "test_config*" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
-
- buildPhase = ''
- make clean_share_link
- make create_share_link
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- make src/plugins/aorai/tests/ptests_config
- export AORAI_WP_CACHE=replay
- export AORAI_WP_CACHEDIR=${plugins.wp-cache.src}
- make PTESTS_OPTS="-error-code" aorai-test-prove
- '';
-
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- eva-tests = mk_deriv {
- name = "frama-c-eva-tests";
- buildInputs = self.mk_buildInputs { };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- export CONFIGS="equality bitwise symblocs gauges octagon"
- src/plugins/value/vtests.sh -j 4 -error-code
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- e-acsl-tests-dev = mk_deriv {
- name = "frama-c-e-acsl-tests-dev";
- buildInputs = self.mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };
- build_dir = self.main.build_dir;
- src = self.main.build_dir + "/dir.tar";
- sourceRoot = ".";
- postUnpack = ''
- find . \( -name "Makefile*" -or -name ".depend" -o -name "ptests_config" -o -name "config.status" \) -exec bash -c "t=\$(stat -c %y \"\$0\"); sed -i -e \"s&$(cat $build_dir/old_pwd)&$(pwd)&g\" \"\$0\"; touch -d \"\$t\" \"\$0\"" {} \;
- '';
- configurePhase = ''
- true
- '';
- buildPhase = ''
- make clean_share_link
- make create_share_link
- make E_ACSL_TESTS PTESTS_OPTS="-error-code" DEV=yes
- '';
- installPhase = ''
- true
- '';
- } // { other-opam-selection = "main"; };
-
- internal = mk_deriv {
- name = "frama-c-internal";
- src = self.src;
- opamPackages = [ "xml-light" ];
- buildInputs =
- self.mk_buildInputs
- { nixPackages =
- [ pkgs.getopt pkgs.libxslt pkgs.libxml2 pkgs.autoPatchelfHook
- pkgs.swiProlog stdenv.cc.cc.lib ];
- };
- genassigns_src = plugins.genassigns.src;
- frama_clang_src = plugins.frama-clang.src;
- pathcrawler_src = plugins.pathcrawler.src;
- mthread_src = plugins.mthread.src;
- caveat_importer_src = plugins.caveat-importer.src;
- acsl_importer_src = plugins.acsl-importer.src;
- volatile_src = plugins.volatile.src;
- security_src = plugins.security.src;
- context_from_precondition_src = plugins.context-from-precondition.src;
- metacsl_src = plugins.meta.src;
- linea_cabs_src = plugins.linea-cabs.src;
- postPatch = ''
- patchShebangs .
- '';
- postUnpack = ''
- cp -r --preserve=mode "$genassigns_src" "$sourceRoot/src/plugins/genassigns"
- chmod -R u+w -- "$sourceRoot/src/plugins/genassigns"
- # cp -r --preserve=mode "$frama_clang_src" "$sourceRoot/src/plugins/frama-clang"
- # chmod -R u+w -- "$sourceRoot/src/plugins/frama-clang"
- cp -r --preserve=mode "$pathcrawler_src" "$sourceRoot/src/plugins/pathcrawler"
- chmod -R u+w -- "$sourceRoot/src/plugins/pathcrawler"
- cp -r --preserve=mode "$mthread_src" "$sourceRoot/src/plugins/mthread"
- chmod -R u+w -- "$sourceRoot/src/plugins/mthread"
- cp -r --preserve=mode "$caveat_importer_src" "$sourceRoot/src/plugins/caveat-importer"
- chmod -R u+w -- "$sourceRoot/src/plugins/caveat-importer"
- cp -r --preserve=mode "$volatile_src" "$sourceRoot/src/plugins/volatile"
- chmod -R u+w -- "$sourceRoot/src/plugins/volatile"
- cp -r --preserve=mode "$acsl_importer_src" "$sourceRoot/src/plugins/acsl-importer"
- chmod -R u+w -- "$sourceRoot/src/plugins/acsl-importer"
- echo IN_FRAMA_CI=yes > "$sourceRoot/in_frama_ci"
- cp -r --preserve=mode "$context_from_precondition_src" "$sourceRoot/src/plugins/context-from-precondition"
- chmod -R u+w -- "$sourceRoot/src/plugins/context-from-precondition"
- cp -r --preserve=mode "$linea_cabs_src" "$sourceRoot/src/plugins/linea-cabs"
- chmod -R u+w -- "$sourceRoot/src/plugins/linea-cabs"
- cp -r --preserve=mode "$security_src" "$sourceRoot/src/plugins/security"
- chmod -R u+w -- "$sourceRoot/src/plugins/security"
- '';
-
- configurePhase = ''
- unset CC
- autoconf
- ./configure --prefix=$out
- '';
- buildPhase = ''
- make unpack-eclipse
- sed -i src/plugins/pathcrawler/extern/eclipseCLP/RUNME -e "s/chmod 2755/chmod 755/g"
- rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/dbi_mysql.so
- rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/ic.so
- rm src/plugins/pathcrawler/extern/eclipseCLP/lib/x86_64_linux/bitmap.so
- rm -fr src/plugins/pathcrawler/extern/eclipseCLP/lib/i386_linux
- rm src/plugins/pathcrawler/src/generator/COLIBRI/float_util_sparc_sunos5.so
- rm src/plugins/pathcrawler/src/generator/COLIBRI/float_util_i386_linux.so.*
- rm src/plugins/pathcrawler/share/bin/float_util_sparc_sunos5.so
- find src/plugins/pathcrawler -name '*_i386_*.so' -delete
- autoPatchelf src/plugins/pathcrawler/
- make -j 4
- ln -sr src/plugins/pathcrawler/share share/pc
- # Setup Why3
- mkdir home
- HOME=$(pwd)/home
- why3 config detect
- # Setup WP related
- export CAVEAT_IMPORTER_NIX_MODE=yes
- export GENASSIGNS_NIX_MODE=yes
- export FRAMAC_WP_CACHE=replay
- export FRAMAC_WP_CACHEDIR=${plugins.wp-cache.src}
- make tests -j4 PTESTS_OPTS="-error-code -j 4"
- '';
- installPhase = ''
- make install
- '';
- };
-
-})
diff --git a/nix/empty b/nix/empty
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/nix/external-plugin-ci.sh b/nix/external-plugin-ci.sh
index c40d44679f7d397cb00e02d5da533cd1d7ed878d..fe3219be89b8bb107f6e82f7df4158ed590425ca 100755
--- a/nix/external-plugin-ci.sh
+++ b/nix/external-plugin-ci.sh
@@ -24,7 +24,7 @@
# DEFAULT variable can be configured to indicate reference branch when the
# current branch does not exist in a dependency or in Frama-C.
#
-# OCAML must be set to the right version of OCAML (format: N_MM)
+# OCAML must be set to the right version of OCAML (format: N_MM or N.MM)
set -euxo pipefail
@@ -42,6 +42,9 @@ if [ -z ${OCAML+x} ]; then
exit 2
fi
+# Normalize version for Nix
+OCAML=${OCAML/./_}
+
DEFAULT=${DEFAULT:-master}
# prints
diff --git a/nix/frama-c-hdrck.nix b/nix/frama-c-hdrck.nix
index 5c65409ca3e8873d1606d6d9eae352bfb7f6250f..e634a7742dc2b1127a1cac186cc3b8db11d4cee8 100644
--- a/nix/frama-c-hdrck.nix
+++ b/nix/frama-c-hdrck.nix
@@ -13,7 +13,7 @@ stdenv.mkDerivation rec {
(builtins.readFile ../VERSION));
slang = lib.strings.removeSuffix "\n" (builtins.readFile ../VERSION_CODENAME);
- src = gitignoreSource ./../headers ;
+ src = gitignoreSource ./../tools/hdrck ;
buildInputs = [
dune_3
diff --git a/nix/frama-c.nix b/nix/frama-c.nix
index 4703f6b739a10dcd31e0b83b3eada8b2b371e3d2..5616e9944a00658218741c726858d31c2a0befac 100644
--- a/nix/frama-c.nix
+++ b/nix/frama-c.nix
@@ -105,8 +105,8 @@ stdenvNoCC.mkDerivation rec {
buildPhase = ''
make config.sed
dune build -j2 --display short $release_mode @install
- make ptests/ptests.exe
- make ptests/wtests.exe
+ make tools/ptests/ptests.exe
+ make tools/ptests/wtests.exe
'';
installFlags = [
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
deleted file mode 100644
index eccc033949bb7b58902bedfcbf60a6d6555b59eb..0000000000000000000000000000000000000000
--- a/nix/frama-ci.nix
+++ /dev/null
@@ -1,16 +0,0 @@
-#To copy in other repository
-{ password}:
-
-let
- src = builtins.fetchGit {
- "url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
- "name" = "Frama-CI";
- "rev" = "ceea8c97fc127db159bfd92919eae404e2e67f18";
- "ref" = "master";
- };
- pkgs = import "${src}/pkgs.nix" {};
- in
- {
- src = src;
- compiled = pkgs.callPackage "${src}/compile.nix" { inherit pkgs; };
- }
diff --git a/nix/internal-tests.nix b/nix/internal-tests.nix
index 206c76fbbe5c51c51e37f1d0a1a754e54d19e64e..2df01e54b1631c95093e47581045eb01816bb029 100644
--- a/nix/internal-tests.nix
+++ b/nix/internal-tests.nix
@@ -111,8 +111,8 @@ stdenvNoCC.mkDerivation rec {
buildPhase = ''
make config.sed
dune build -j2 --display short @install
- make ptests/ptests.exe
- make ptests/wtests.exe
+ make tools/ptests/ptests.exe
+ make tools/ptests/wtests.exe
'';
wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git";
@@ -123,7 +123,7 @@ stdenvNoCC.mkDerivation rec {
mkdir home
HOME=$(pwd)/home
why3 config detect
- export FRAMAC_WP_CACHE=replay
+ export FRAMAC_WP_CACHE=offline
export FRAMAC_WP_CACHEDIR=$wp_cache
'';
diff --git a/nix/internal-tests.sh b/nix/internal-tests.sh
index b5653919b51fbcdb8dd7b5139401b6e2a04cd06c..aca2f3e814cb73d6244d780cbbb52a8cc7d6b293 100755
--- a/nix/internal-tests.sh
+++ b/nix/internal-tests.sh
@@ -24,7 +24,7 @@
# DEFAULT variable can be configured to indicate reference branch when the
# current branch does not exist in a plugin.
#
-# OCAML must be set to the right version of OCAML (format: N_MM)
+# OCAML must be set to the right version of OCAML (format: N_MM or N.MM)
set -euxo pipefail
@@ -33,6 +33,9 @@ if [ -z ${OCAML+x} ]; then
exit 2
fi
+# Normalize version for Nix
+OCAML=${OCAML/./_}
+
DEFAULT=${DEFAULT:-master}
# prints
diff --git a/nix/mk_plugin.nix b/nix/mk_plugin.nix
index df814796e5b523e5f40ab35485d601eb528be5a9..c5280b67f10b90d63d1230e1fb55aefbc930da6f 100644
--- a/nix/mk_plugin.nix
+++ b/nix/mk_plugin.nix
@@ -100,7 +100,7 @@ stdenv.mkDerivation {
mkdir home
HOME=$(pwd)/home
why3 config detect
- export FRAMAC_WP_CACHE=replay
+ export FRAMAC_WP_CACHE=offline
export FRAMAC_WP_CACHEDIR=$wp_cache
''
else "") ;
@@ -112,7 +112,7 @@ stdenv.mkDerivation {
'';
installFlags = [
- "FRAMAC_INSTALLDIR=$(out)"
+ "INSTALLDIR=$(out)"
];
postInstall = if install-opam then ''
diff --git a/nix/mk_tests.nix b/nix/mk_tests.nix
index b1b111238837785a4e0d3d3fe4abceb2ddcea893..4241026860bcff77cdc51a27b028e3a258de6257 100644
--- a/nix/mk_tests.nix
+++ b/nix/mk_tests.nix
@@ -70,7 +70,7 @@ stdenvNoCC.mkDerivation {
mkdir home
HOME=$(pwd)/home
why3 config detect
- export FRAMAC_WP_CACHE=replay
+ export FRAMAC_WP_CACHE=offline
export FRAMAC_WP_CACHEDIR=$wp_cache
''
else "" ;
diff --git a/nix/pkgs.nix b/nix/pkgs.nix
index 045a219ce00d511f0d43b05cd9925c23fa5c6310..f2750a73d4931be46008e6372d10dd8daf9bf8de 100644
--- a/nix/pkgs.nix
+++ b/nix/pkgs.nix
@@ -15,10 +15,13 @@ let
mk_tests = oself.callPackage ./mk_tests.nix {};
mk_plugin = oself.callPackage ./mk_plugin.nix {};
- # Shell containing checkers (hdrck, ocp-indent)
+ # Shells containing checkers (hdrck, ocp-indent, Frama-C for plugins)
frama-c-checkers-shell = oself.callPackage ./frama-c-checkers-shell.nix {
git = pkgs.git ;
};
+ plugin-checkers-shell = oself.callPackage ./plugin-checkers-shell.nix {
+ git = pkgs.git ;
+ };
# Builds
frama-c = oself.callPackage ./frama-c.nix {};
diff --git a/nix/plugin-checkers-shell.nix b/nix/plugin-checkers-shell.nix
new file mode 100644
index 0000000000000000000000000000000000000000..dfb0113011f38d97e8bd6d935846c3837132083f
--- /dev/null
+++ b/nix/plugin-checkers-shell.nix
@@ -0,0 +1,18 @@
+{ lib
+, stdenv
+, frama-c
+, git
+, gnumake
+, headache
+, ocp-indent
+} :
+stdenv.mkDerivation rec {
+ name = "plugin-checkers-shell";
+ buildInputs = [
+ frama-c
+ git
+ gnumake
+ headache
+ ocp-indent
+ ];
+}
diff --git a/nix/shell-checkers.sh b/nix/shell-checkers.sh
new file mode 100755
index 0000000000000000000000000000000000000000..c392a31787ec6def094c820d8e043b962a5b4f20
--- /dev/null
+++ b/nix/shell-checkers.sh
@@ -0,0 +1,36 @@
+#!/usr/bin/env bash
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2022 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# OCAML must be set to the right version of OCAML (format: N_MM or N.MM)
+
+set -euxo pipefail
+
+if [ -z ${OCAML+x} ]; then
+ echo "OCAML variable must be set to a version of OCaml"
+ exit 2
+fi
+
+# Normalize version for Nix
+OCAML=${OCAML/./_}
+
+nix-shell "./nix/pkgs.nix" -A ocaml-ng.ocamlPackages_$OCAML.frama-c-checkers-shell --run "$1"
diff --git a/nix/shell.nix b/nix/shell.nix
deleted file mode 100644
index 1eda48797e573f965fac0f432d345f04f5bdee8a..0000000000000000000000000000000000000000
--- a/nix/shell.nix
+++ /dev/null
@@ -1,13 +0,0 @@
-let
- pkgs = import ./pkgs.nix;
- ocamlPackages_for_shell = pkgs.ocaml-ng.ocamlPackages_4_12;
-in
-pkgs.mkShell {
- nativeBuildInputs = with pkgs; [
- niv
- ocamlPackages_for_shell.merlin
- ocamlPackages_for_shell.ocaml-lsp
- ocamlPackages_for_shell.utop
- ];
- inputsFrom = [ ocamlPackages_for_shell.frama-c ];
-}
diff --git a/nix/sources.json b/nix/sources.json
index 02425a2daaa63545f9c8f418f0ddd82129b3f305..bedb63ce514388d3a997df2c66cd1d46a9355352 100644
--- a/nix/sources.json
+++ b/nix/sources.json
@@ -29,10 +29,10 @@
"homepage": "https://github.com/NixOS/nixpkgs",
"owner": "NixOS",
"repo": "nixpkgs",
- "rev": "bc4b9eef3ce3d5a90d8693e8367c9cbfc9fc1e13",
- "sha256": "0mrpsl0554fzk04asz0nmyxf6ny1syd9qzrh37vz85bpq8wi21dx",
+ "rev": "f4dfed73ee886b115a99e5b85fdfbeb683290d83",
+ "sha256": "1scpisl06f9mc31khj0m2q21yvx108bi7l9s0n9aq8f1w4fjprg6",
"type": "tarball",
- "url": "https://github.com/NixOS/nixpkgs/archive/bc4b9eef3ce3d5a90d8693e8367c9cbfc9fc1e13.tar.gz",
+ "url": "https://github.com/NixOS/nixpkgs/archive/f4dfed73ee886b115a99e5b85fdfbeb683290d83.tar.gz",
"url_template": "https://github.com/<owner>/<repo>/archive/<rev>.tar.gz"
},
"why3": {
diff --git a/opam/opam b/opam/opam
index 8d9d456ce0ba2e92a52273b9f7a1eba376e00a7e..b4b37a5591cfa2df70110ca4c53eeeb3895f0f60 100644
--- a/opam/opam
+++ b/opam/opam
@@ -88,10 +88,9 @@ tags: [
build: [
["autoconf"] {dev}
- ["./configure" "--prefix" prefix
- "--mandir=%{man}%"
- ]
- [make "-j%{jobs}%"]
+ ["./configure"]
+ [make "config.sed"]
+ ["dune" "build" "-j%{jobs}%" "--release" "@install"]
[make "-C" "doc" "download"] {with-doc}
]
@@ -101,10 +100,10 @@ install: [
]
run-test: [
- [make "-j%{jobs}%" "PTESTS_OPTS=-error-code" "tests"] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
- # tests are disabled on PPC64 due to floating-point oracle differences
- # (some ULPs in libc trigonometric functions) and due to the lack of
- # available hardware to test them locally
+ ["dune" "exec" "--" "frama-c-ptests" "tests" "src/plugins/*/tests"
+ ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
+ ["dune" "build" "-j%{jobs}%" "@ptests_config"
+ ] { arch != "ppc64" & arch != "x86_32" & arch != "arm32" }
]
# Please keep depends and depopts sorted by package name
diff --git a/share/Makefile.headers b/share/Makefile.headers
index 74392e03e347b0479120008174ac3cf3b5da070c..12f55b36c3bbe6703a86587882c26220424f1ed2 100644
--- a/share/Makefile.headers
+++ b/share/Makefile.headers
@@ -79,10 +79,10 @@ HDRCK:= frama-c-hdrck
else
# HDRCK is internal
-HDRCK:= dune exec --root headers -- frama-c-hdrck
+HDRCK:= dune exec --root $(FRAMAC_HDRCK_SRC) -- frama-c-hdrck
-$(FRAMAC_HDRCK): headers/hdrck.ml
- dune build --root headers hdrck.exe
+$(FRAMAC_HDRCK): $(FRAMAC_HDRCK_SRC)/hdrck.ml
+ dune build --root $(FRAMAC_HDRCK_SRC) hdrck.exe
endif
@@ -224,4 +224,3 @@ headers.info:
# Local Variables:
# compile-command: "make"
# End:
-
diff --git a/share/Makefile.linting b/share/Makefile.linting
index e02bbe19b32e6caebb7f8819f25ebe7c3971bc8f..85911ad2b41d6c1528a5bfe34a22327b92db937b 100644
--- a/share/Makefile.linting
+++ b/share/Makefile.linting
@@ -33,8 +33,11 @@
# - make LINT_DIR=<subdir> <lint-target>
# It is possible to force the action to given files:
# - make LINT_FILE=<file> <lint-target>
+# or to the files modified between HEAD and a specific branch/commit:
+# - make LINT_DIFF=<branch/commit> <lint-target>
# Notes:
-# - when LINT_FILE is given, .gitattributes and LINT_DIR are ignored;
+# - when LINT_FILE is given, .gitattributes, LINT_DIFF and LINT_DIR are ignored;
+# - when LINT_DIFF is given, LINT_DIR is ignored (but .gitattributes is used);
# - to use fix-utf8 target, the variable LINT_FROM_ENCODING=<from-encoding-name>
# has to be set.
@@ -57,6 +60,8 @@ CLANG_FORMAT ?= clang-format
# Default values necessary for
# LINT_MAKEFILE=<this-makefile> make -f <this-makefile> <lint-target>`
# Otherwise theses variables are defined into share/Makefile.common
+GREP ?= grep
+TR ?= tr
SED ?= LC_ALL=C sed
ISED ?= sed -i
FIND ?= find
@@ -119,7 +124,7 @@ endif
echo "error: $(CLANG_FORMAT) must be installed"; \
exit 1; \
fi;
- mkdir -p $(dir $@)
+ $(MKDIR) $(dir $@)
$(TOUCH) $@
###############
@@ -178,6 +183,13 @@ ifeq ($(LINT_FILE),)
LINT.dir=$(wildcard $(LINT_DIR))
+ifeq ($(LINT_DIFF),)
+FILE_LIST=$(GIT) ls-files $(LINT.dir) -z
+else
+$(info [LINT] Looking at files modified from branch/commit: '$(LINT_DIFF)')
+FILE_LIST=$(GIT) diff --name-status --cached $(LINT_DIFF) | $(GREP) -v "^D" | $(SED) "s/^.[ \t]*//" | $(TR) '\n' '\000'
+endif
+
#### check-XXX targets
# Same list on both lines
@@ -188,7 +200,7 @@ LINT.check-targets= \
# Generic rule
$(LINT.check-targets):
echo "[LINT] Checking from GIT attribute $@..."
- $(GIT) ls-files $(LINT.dir) -z \
+ $(FILE_LIST) \
| $(GIT) check-attr --stdin -z $@ \
| $(SED) -zne 'x;n;n;s/^set$$//;t print;b;:print;x;p' \
| $(XARGS) -0 -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
@@ -203,7 +215,7 @@ LINT.fix-targets= \
# Generic rule
$(LINT.fix-targets):
echo "[LINT] Fixing from GIT attribute $(patsubst fix-%,check-%,$@)..."
- $(GIT) ls-files $(LINT.dir) -z \
+ $(FILE_LIST) \
| $(GIT) check-attr --stdin -z $(patsubst fix-%,check-%,$@) \
| $(SED) -zne 'x;n;n;s/^set$$//;t print;b;:print;x;p' \
| $(XARGS) -0 -IXX sh -c '$(LINT.make) LINT_FILE="XX" $@ || exit 255'
diff --git a/share/Makefile.testing b/share/Makefile.testing
index 0939754a0096a96e3ed3a1faaba16dc120172e38..121f88a0074f636910f7bc073e5104b3108e41fc 100644
--- a/share/Makefile.testing
+++ b/share/Makefile.testing
@@ -87,12 +87,12 @@ PTESTS=frama-c-ptests
else
# PTESTS is internal
-PTESTS=dune exec $(DUNE_BUILD_OPTS) --root ptests -- frama-c-ptests
-#PTESTS=dune exec $(DUNE_BUILD_OPTS) --root ptests -- frama-c-ptests -v
+PTESTS=dune exec $(DUNE_BUILD_OPTS) --root $(FRAMAC_PTESTS_SRC) -- frama-c-ptests
+#PTESTS=dune exec $(DUNE_BUILD_OPTS) --root $(FRAMAC_PTESTS_SRC) -- frama-c-ptests -v
# Note: the public name of ptest.exe is frama-c-ptests
-$(FRAMAC_PTESTS): ptests/ptests.ml
- dune build --root ptests ptests.exe
+$(FRAMAC_PTESTS): $(FRAMAC_PTESTS_SRC)/ptests.ml
+ dune build --root $(FRAMAC_PTESTS_SRC) ptests.exe
endif
@@ -117,11 +117,11 @@ WTESTS=frama-c-wtests
else
# WTESTS is internal to Frama-C
-WTESTS=dune exec $(DUNE_BUILD_OPTS) --root ptests -- frama-c-wtests
+WTESTS=dune exec $(DUNE_BUILD_OPTS) --root $(FRAMAC_PTESTS_SRC) -- frama-c-wtests
# Note: the public name of wtest.exe is frama-c-wtests
-$(FRAMAC_WTESTS): ptests/wtests.ml
- dune build --root ptests wtests.exe
+$(FRAMAC_WTESTS): $(FRAMAC_PTESTS_SRC)/wtests.ml
+ dune build --root $(FRAMAC_PTESTS_SRC) wtests.exe
endif
diff --git a/share/dune b/share/dune
index c04664ab741a6da8f383ae406e2f98e642a59dbd..b0f8d4ff74f61a15acc53797f0e7f6ee289ec82d 100644
--- a/share/dune
+++ b/share/dune
@@ -24,6 +24,11 @@
(package frama-c)
(section (site (frama-c share)))
(files
+; Useful Makefiles
+(Makefile.headers as Makefile.headers)
+(Makefile.linting as Makefile.linting)
+(Makefile.installation as Makefile.installation)
+(Makefile.testing as Makefile.testing)
; GUI Images
(frama-c.ico as frama-c.ico)
(frama-c.png as frama-c.png)
diff --git a/src/plugins/aorai/dune-project b/src/plugins/aorai/dune-project
index d7317b50ddbb90e03fc21e044cb2b8449ea987f3..6310f54128592bdb3969562b7a0000369b24fd76 100644
--- a/src/plugins/aorai/dune-project
+++ b/src/plugins/aorai/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Aorai plug-in of Frama-C. ;;
diff --git a/src/plugins/aorai/tests/ltl/goto.c b/src/plugins/aorai/tests/ltl/goto.c
index abaf6d16f737c744fb157a8d30f8b150e562dcef..b8685eec176b5ff0400d728af807018ade5571ee 100644
--- a/src/plugins/aorai/tests/ltl/goto.c
+++ b/src/plugins/aorai/tests/ltl/goto.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle.c b/src/plugins/aorai/tests/ltl/test_boucle.c
index 6325177b5bd437c00db0b8dfde3cf6e93afdfe76..242401c8d41a5c9b4a97646e6c6c5cebeae180d8 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
/*@ requires \true;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle1.c b/src/plugins/aorai/tests/ltl/test_boucle1.c
index b66e6a7c829a6641fee515eb30d1d5d629babb42..3f24248397ef975cbd10cb7b8f794b5735b7bdcd 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle1.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle1.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int cpt=3;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle2.c b/src/plugins/aorai/tests/ltl/test_boucle2.c
index 257a9a19b810a573fd18230f49c00c6d9eb04c2d..a37e79e10971fbe6ed463bf315bfa4fbcbc60704 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle2.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle2.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_boucle3.c b/src/plugins/aorai/tests/ltl/test_boucle3.c
index 1cdc2b029c0761d92a9581b3357538be358e2cfc..3cd384b94a561399d1536d315f09008026ec004e 100644
--- a/src/plugins/aorai/tests/ltl/test_boucle3.c
+++ b/src/plugins/aorai/tests/ltl/test_boucle3.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
diff --git a/src/plugins/aorai/tests/ltl/test_config b/src/plugins/aorai/tests/ltl/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..96c1d0d716a3ae949b1bd19b2fd92a2b13ccfbd8
--- /dev/null
+++ b/src/plugins/aorai/tests/ltl/test_config
@@ -0,0 +1,2 @@
+ENABLED_IF: %{bin-available:ltl2ba}
+STDOPT:
diff --git a/src/plugins/aorai/tests/ltl/test_config_prove b/src/plugins/aorai/tests/ltl/test_config_prove
new file mode 100644
index 0000000000000000000000000000000000000000..96c1d0d716a3ae949b1bd19b2fd92a2b13ccfbd8
--- /dev/null
+++ b/src/plugins/aorai/tests/ltl/test_config_prove
@@ -0,0 +1,2 @@
+ENABLED_IF: %{bin-available:ltl2ba}
+STDOPT:
diff --git a/src/plugins/aorai/tests/ltl/test_factorial.c b/src/plugins/aorai/tests/ltl/test_factorial.c
index 313ecfbaa750192ad1cdd36a783fbcb75034e141..009b6db869a7439b1fcda0bd16ea439e39b00490 100644
--- a/src/plugins/aorai/tests/ltl/test_factorial.c
+++ b/src/plugins/aorai/tests/ltl/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl}
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion1.c b/src/plugins/aorai/tests/ltl/test_recursion1.c
index a3f69a89db840f6a582edc7e2c8eaec921b3354e..bed9bf66e83256498aae83e2faa46b693e5cb92c 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion1.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion1.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
diff --git a/src/plugins/aorai/tests/ltl/test_recursion2.c b/src/plugins/aorai/tests/ltl/test_recursion2.c
index 7effcb5bfed5a06821d505ee9632fce32bffdcc0..a51847f8c6b5473bd08eb35f9ffa995b2b6b11e6 100644
--- a/src/plugins/aorai/tests/ltl/test_recursion2.c
+++ b/src/plugins/aorai/tests/ltl/test_recursion2.c
@@ -1,6 +1,6 @@
/* run.config*
- STDOPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-acceptance
- STDOPT: -aorai-buchi %{dep:@PTEST_DIR@/test_recursion3.promela} -aorai-acceptance
+ STDOPT: -aorai-buchi %{dep:@PTEST_NAME@.promela} -aorai-acceptance
+ STDOPT: -aorai-buchi %{dep:test_recursion3.promela} -aorai-acceptance
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch2.c b/src/plugins/aorai/tests/ltl/test_switch2.c
index 637be79d815d361f9bfc46c8a9e4a5ed15a33768..77290f3f226e7c9f42bac747c78b41f648e1232b 100644
--- a/src/plugins/aorai/tests/ltl/test_switch2.c
+++ b/src/plugins/aorai/tests/ltl/test_switch2.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
int status=0;
diff --git a/src/plugins/aorai/tests/ltl/test_switch3.c b/src/plugins/aorai/tests/ltl/test_switch3.c
index 037f58fb2c440a7277b5aed83fb53308be15fde5..090c0769545f6092b0ef082458e88f1153e6059a 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
index 9ef5f759998d7cbc088c6db9030f90ee378ac2ca..9756ddb36ee09942926236b1920eb63db685071e 100644
--- a/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
/* run.config*
- STDOPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-acceptance
+ STDOPT: -aorai-ltl %{dep:@PTEST_NAME@.ltl} -aorai-acceptance
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/ptests_config b/src/plugins/aorai/tests/ptests_config
index 34b21cc61881d5f098943d7647fde26effacf51e..7fc044169e395ade683964186f5cbf36c046eea5 100644
--- a/src/plugins/aorai/tests/ptests_config
+++ b/src/plugins/aorai/tests/ptests_config
@@ -1,2 +1,2 @@
-DEFAULT_SUITES= ya
-prove_SUITES= ya
+DEFAULT_SUITES= ya ltl
+prove_SUITES= ya ltl
diff --git a/src/plugins/api-generator/dune-project b/src/plugins/api-generator/dune-project
index bbff6793075aec958bdc1f7458c3101b437a75a9..572790587d344dcbc049c3f6cabe6a6302532763 100644
--- a/src/plugins/api-generator/dune-project
+++ b/src/plugins/api-generator/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/callgraph/dune-project b/src/plugins/callgraph/dune-project
index 95a622cf6c73fea62d85b4f9a1ac1760f8448e7d..f0c8f918da8eee6f140dc0ccec184570c1d9fe56 100644
--- a/src/plugins/callgraph/dune-project
+++ b/src/plugins/callgraph/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/constant_propagation/dune-project b/src/plugins/constant_propagation/dune-project
index 874ac889d2378b673e657f86a0da41a0a59c60b1..e455736b22b6e7e1b7129d532ec861a17930799b 100644
--- a/src/plugins/constant_propagation/dune-project
+++ b/src/plugins/constant_propagation/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/dive/dune-project b/src/plugins/dive/dune-project
index 222120b30265a63e311a111f5e5d658ee7717549..0a45c5e58bba18590aa1c31aac005ddadca7a2f0 100644
--- a/src/plugins/dive/dune-project
+++ b/src/plugins/dive/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/e-acsl/dune-project b/src/plugins/e-acsl/dune-project
index ff6fc87f7ce11a88bdf8aaf7e2a1850c4512c6e4..0b479545c886aec70e2641247c72343264ed482a 100644
--- a/src/plugins/e-acsl/dune-project
+++ b/src/plugins/e-acsl/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of the Frama-C's E-ACSL plug-in. ;;
diff --git a/src/plugins/e-acsl/tests/concurrency/threads_debug.c b/src/plugins/e-acsl/tests/concurrency/threads_debug.c
index 75bf51d6121358b31fa55b3114b3d2b2ac5a6b12..31d748444a6be8d371c348153e7033886894b409 100644
--- a/src/plugins/e-acsl/tests/concurrency/threads_debug.c
+++ b/src/plugins/e-acsl/tests/concurrency/threads_debug.c
@@ -1,10 +1,10 @@
-/* run.config, run.config_dev
+/* run.config_dev
COMMENT: This test is identical to `parallel_thread.c` but with RTL debug code
COMMENT: activated.
MACRO: ROOT_EACSL_GCC_OPTS_EXT --rt-debug --rt-verbose --concurrency
-
COMMENT: Filter the addresses of the output so that the test is deterministic.
MACRO: ROOT_EACSL_EXEC_FILTER sed -e s_0x[0-9a-f-]*_0x0000-0000-0000_g | sed -e s_Offset:\s[0-9-]*_Offset:xxxxx_g | sed -e s/[0-9]*\skB/xxxkB/g | sed -e s/[0-9]*\sMB/xxxMB/g | sed -e s/Leaked.*bytes/Leakedxxxbytes/g
+ DONTRUN:
*/
// Include existing test
diff --git a/src/plugins/e-acsl/tests/memory/vdso.c b/src/plugins/e-acsl/tests/memory/vdso.c
index d71a88db11369c7445fd003b33abea36722ffd99..38cebaf2b4d428ba7294762a882c402a5fd20665 100644
--- a/src/plugins/e-acsl/tests/memory/vdso.c
+++ b/src/plugins/e-acsl/tests/memory/vdso.c
@@ -2,7 +2,7 @@
STDOPT: #"-e-acsl-full-mtracking"
*/
/* run.config_dev
- MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --rt-debug
+ DONTRUN: MACRO: ROOT_EACSL_GCC_OPTS_EXT --full-mtracking --rt-debug
*/
#include <time.h>
diff --git a/src/plugins/from/dune-project b/src/plugins/from/dune-project
index 0c2a0998893f740fb875bb5465efcd90823df8fe..4f636dba24bab4bb183a1195ea99fc23cc6f4490 100644
--- a/src/plugins/from/dune-project
+++ b/src/plugins/from/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/impact/dune-project b/src/plugins/impact/dune-project
index 8cde0454d8be5cdedef669b27b4eaffce756d8c6..3c590eff01801f722fdea3b386882e5c8b2924e0 100644
--- a/src/plugins/impact/dune-project
+++ b/src/plugins/impact/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/inout/dune-project b/src/plugins/inout/dune-project
index 3e4099fe3c8d2a19d708db3a80e3aec1a0e65d6c..f1e420b2977367d9680cb65fb4c61753b0ac4049 100644
--- a/src/plugins/inout/dune-project
+++ b/src/plugins/inout/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/instantiate/dune-project b/src/plugins/instantiate/dune-project
index 53c2c30c6ef2756e9369b0ac52a69b4559bc3689..21067e40127356e7414f2e693db558fa645cb0c8 100644
--- a/src/plugins/instantiate/dune-project
+++ b/src/plugins/instantiate/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/loop_analysis/dune-project b/src/plugins/loop_analysis/dune-project
index 5b2cde9de76f488f0fb8da759f3349920056d2e3..c7d0e2e99d61b1b5adfbf9a9d2dd5f741343e5f8 100644
--- a/src/plugins/loop_analysis/dune-project
+++ b/src/plugins/loop_analysis/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/markdown-report/dune-project b/src/plugins/markdown-report/dune-project
index 98b4a10aabdc0430efa57f0f63de3deaa9149852..2f95b35d7a3fffbca58549b1a31d884f3e10bcba 100644
--- a/src/plugins/markdown-report/dune-project
+++ b/src/plugins/markdown-report/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/metrics/dune-project b/src/plugins/metrics/dune-project
index a0c509088c21d1d5c883d7cdac93ae994ac4c1e9..507ccd298ba0e12e7906bc998ef38d344c7c88ba 100644
--- a/src/plugins/metrics/dune-project
+++ b/src/plugins/metrics/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/nonterm/dune-project b/src/plugins/nonterm/dune-project
index cee289176ac86670db2066aab38c5eb07f69b100..a91cdce8beaa366f997c06157a79ccc10e464b9c 100644
--- a/src/plugins/nonterm/dune-project
+++ b/src/plugins/nonterm/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/obfuscator/dune-project b/src/plugins/obfuscator/dune-project
index b5af7a24e43ea372916f5eec62993e256e950310..c74dfe1f855719718015f2986c9b183ebe09c4d5 100644
--- a/src/plugins/obfuscator/dune-project
+++ b/src/plugins/obfuscator/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/occurrence/dune-project b/src/plugins/occurrence/dune-project
index ea66e0e48be27b4e9384b9f5d46b895f5b5756a6..c4d46ce003e6e51858792b9f473077381506b0ac 100644
--- a/src/plugins/occurrence/dune-project
+++ b/src/plugins/occurrence/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/pdg/dune-project b/src/plugins/pdg/dune-project
index 1d13e366f656f5cac6d4e1179849b0c3b77f25ad..12ff9bf17de9a6ee74274b32b49f5fc6f4a1b7d2 100644
--- a/src/plugins/pdg/dune-project
+++ b/src/plugins/pdg/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/postdominators/dune-project b/src/plugins/postdominators/dune-project
index 269ba4e18cba9a1e48cf84f7b6ef99461f401ae2..db21480e1f5cffa508aabcf63e6c2c28be05ba01 100644
--- a/src/plugins/postdominators/dune-project
+++ b/src/plugins/postdominators/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/print_api/dune-project b/src/plugins/print_api/dune-project
index 75b5944a83a6a05215ca80168a07d34f889b8e13..f4887f33a78bd82e30ce3ed1c67d36a0ad3584e6 100644
--- a/src/plugins/print_api/dune-project
+++ b/src/plugins/print_api/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/qed/dune-project b/src/plugins/qed/dune-project
index db151b2fb0545c053eaec88989826467b64ec4f6..cc71f1946f8869a92c1a460d797f88b6d4e0c4e1 100644
--- a/src/plugins/qed/dune-project
+++ b/src/plugins/qed/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/reduc/dune-project b/src/plugins/reduc/dune-project
index e77db938c6df60b65e33c1a357f26fd9cb11a439..e9d7fc8b47138992aaad83218578bd65c7dc223c 100644
--- a/src/plugins/reduc/dune-project
+++ b/src/plugins/reduc/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/report/dune-project b/src/plugins/report/dune-project
index 2358c8daf8d46a33f77938ec0827539ac519df80..e58864153062c3c28c43d89445771e5481e80f77 100644
--- a/src/plugins/report/dune-project
+++ b/src/plugins/report/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/rte/dune-project b/src/plugins/rte/dune-project
index 517150a660e00f264aa9cd69ec7f2972d85b57e9..8faf68e3c1d0a623682081a1d83c1c1a85879abb 100644
--- a/src/plugins/rte/dune-project
+++ b/src/plugins/rte/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/scope/dune-project b/src/plugins/scope/dune-project
index cbd34d3aa5114c3af36dd380f4f6142ee00a674f..b2f3282105ebdb366cdec8b2901b7fc23c76e7ae 100644
--- a/src/plugins/scope/dune-project
+++ b/src/plugins/scope/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/security_slicing/dune-project b/src/plugins/security_slicing/dune-project
index bbbfc8dda3bc773e60531f53292d5cd1a40e0063..153f462fbfbca972919cb52b318ad1e5027bbbf2 100644
--- a/src/plugins/security_slicing/dune-project
+++ b/src/plugins/security_slicing/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/server/dune-project b/src/plugins/server/dune-project
index 3ab499b378067490ab2037dfd96e5a9df2f990fc..f9fc8ba242d6e1999f496ef5570b92e9bb62ba18 100644
--- a/src/plugins/server/dune-project
+++ b/src/plugins/server/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/slicing/dune-project b/src/plugins/slicing/dune-project
index 07b8be3ec010811cb28ee5a546d75925af68c25b..8f75251e779d289edc199385618c0eba0689d3e7 100644
--- a/src/plugins/slicing/dune-project
+++ b/src/plugins/slicing/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/sparecode/dune-project b/src/plugins/sparecode/dune-project
index 9967b38940a329207d1c7689408c95cb65c390db..99f06f41fd6cf50c41b7afc9534a29c862e6da01 100644
--- a/src/plugins/sparecode/dune-project
+++ b/src/plugins/sparecode/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/studia/dune-project b/src/plugins/studia/dune-project
index e9862343663fd58dcacc9361068df3ffb05c1538..2eedff1444093bc8ff4f7c1571a531842fa3ecdb 100644
--- a/src/plugins/studia/dune-project
+++ b/src/plugins/studia/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/users/dune-project b/src/plugins/users/dune-project
index 248478937b36c65300155fedc54933cfa597d606..757332f51263519c8544aea6b3ebbb0325f0c329 100644
--- a/src/plugins/users/dune-project
+++ b/src/plugins/users/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/value/dune-project b/src/plugins/value/dune-project
index 64ad5aeb1eca481599f8350259027afc89702fc1..11c27712d8fea2942b649cb15f48c6a5991a913e 100644
--- a/src/plugins/value/dune-project
+++ b/src/plugins/value/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/variadic/dune-project b/src/plugins/variadic/dune-project
index 49aa75b87ea1410ce4d46d7268b15163973ebdea..9b6a2b3bd3ab4519ad3857454a0cf5640526bef7 100644
--- a/src/plugins/variadic/dune-project
+++ b/src/plugins/variadic/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/src/plugins/wp/dune-project b/src/plugins/wp/dune-project
index 5142a747c3fc9c61e4e7aaebb0a89acbe93a2701..68f619f079bada578f1480cb7495a4f4dfc45706 100644
--- a/src/plugins/wp/dune-project
+++ b/src/plugins/wp/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/tests/spec/preprocess_dos.c b/tests/spec/preprocess_dos.c
new file mode 100644
index 0000000000000000000000000000000000000000..fad1137e4f47452a05fd11c815e5e59b7c673ad9
--- /dev/null
+++ b/tests/spec/preprocess_dos.c
@@ -0,0 +1,13 @@
+/* run.config*
+DEPS: preprocess_dos.sh
+ENABLED_IF: %{bin-available:unix2dos}
+OPT: -cpp-command="./@PTEST_NAME@.sh unix2dos %i %o" -cpp-frama-c-compliant -print
+*/
+
+int main() {
+ int a = 0;
+ /*@
+ assert a == 0;
+ */
+ return a;
+}
diff --git a/tests/spec/preprocess_dos.c.in b/tests/spec/preprocess_dos.c.in
deleted file mode 100644
index abae8ad374b159cd60043731308ac57df1f96498..0000000000000000000000000000000000000000
--- a/tests/spec/preprocess_dos.c.in
+++ /dev/null
@@ -1,13 +0,0 @@
-/* run.config*
-COMMENT: Don't edit directly preprocess_dos.c, but preprocess_dos.c.in
-@DONTRUN@
-OPT: -cpp-command="@PTEST_DIR@/@PTEST_NAME@.sh @UNIX2DOS@ %i %o" -cpp-frama-c-compliant -print
-*/
-
-int main() {
- int a = 0;
- /*@
- assert a == 0;
- */
- return a;
-}
diff --git a/headers/Makefile b/tools/hdrck/Makefile
similarity index 100%
rename from headers/Makefile
rename to tools/hdrck/Makefile
diff --git a/tools/hdrck/dune b/tools/hdrck/dune
new file mode 100644
index 0000000000000000000000000000000000000000..769d8ae8711541535935fd8e38b2ea856eb18295
--- /dev/null
+++ b/tools/hdrck/dune
@@ -0,0 +1,28 @@
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; ;;
+;; This file is part of Frama-C. ;;
+;; ;;
+;; Copyright (C) 2007-2022 ;;
+;; CEA (Commissariat à l'énergie atomique et aux énergies ;;
+;; alternatives) ;;
+;; ;;
+;; you can redistribute it and/or modify it under the terms of the GNU ;;
+;; Lesser General Public License as published by the Free Software ;;
+;; Foundation, version 2.1. ;;
+;; ;;
+;; It is distributed in the hope that it will be useful, ;;
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of ;;
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the ;;
+;; GNU Lesser General Public License for more details. ;;
+;; ;;
+;; See the GNU Lesser General Public License version 2.1 ;;
+;; for more details (enclosed in the file licenses/LGPLv2.1). ;;
+;; ;;
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(executable
+ (public_name frama-c-hdrck)
+ (name hdrck)
+ (modules hdrck)
+ (libraries unix str)
+)
diff --git a/headers/dune-project b/tools/hdrck/dune-project
similarity index 99%
rename from headers/dune-project
rename to tools/hdrck/dune-project
index fbf0f7596d7c6516f5ff8dfdf77da73007aa5b0a..3a50a77564ad624c2ef212b0448c2bc7e92281e3 100644
--- a/headers/dune-project
+++ b/tools/hdrck/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/headers/hdrck.ml b/tools/hdrck/hdrck.ml
similarity index 99%
rename from headers/hdrck.ml
rename to tools/hdrck/hdrck.ml
index cb620a850c1b874908afffc8d9b22a6ec064b00d..e8fd61024ec531b223e662b26ccf70d4aac4ae5d 100644
--- a/headers/hdrck.ml
+++ b/tools/hdrck/hdrck.ml
@@ -592,10 +592,6 @@ let check_headache_config_file () =
let set_opt (var:'a option ref) (value:'a) = var := Some value
-let get_opt = function
- | None -> assert false
- | Some v -> v
-
let executable_name = Sys.argv.(0)
let umsg =
diff --git a/ptests/.gitignore b/tools/ptests/.gitignore
similarity index 100%
rename from ptests/.gitignore
rename to tools/ptests/.gitignore
diff --git a/ptests/Makefile b/tools/ptests/Makefile
similarity index 100%
rename from ptests/Makefile
rename to tools/ptests/Makefile
diff --git a/ptests/check_oracles.sh b/tools/ptests/check_oracles.sh
similarity index 100%
rename from ptests/check_oracles.sh
rename to tools/ptests/check_oracles.sh
diff --git a/ptests/dune b/tools/ptests/dune
similarity index 100%
rename from ptests/dune
rename to tools/ptests/dune
diff --git a/ptests/dune-project b/tools/ptests/dune-project
similarity index 99%
rename from ptests/dune-project
rename to tools/ptests/dune-project
index f1d0ae6fb8abc78f00208e171b3534bb2ee0930a..c4f77831ca36459149f84d772cf80397a5c2c508 100644
--- a/ptests/dune-project
+++ b/tools/ptests/dune-project
@@ -1,4 +1,4 @@
-(lang dune 2.9)
+(lang dune 3.0)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; ;;
;; This file is part of Frama-C. ;;
diff --git a/ptests/ptests.ml b/tools/ptests/ptests.ml
similarity index 96%
rename from ptests/ptests.ml
rename to tools/ptests/ptests.ml
index 237390a125c21138f9a0165921223c76e89e6aa5..13254fdc71308c2a8615f2d77739283e874eb773 100644
--- a/ptests/ptests.ml
+++ b/tools/ptests/ptests.ml
@@ -62,6 +62,7 @@ module Filename = struct
fun a b -> cygpath (temp_file a b)
else
fun a b -> temp_file a b
+ [@@ warning "-32"]
let sanitize f = String.escaped f
@@ -107,8 +108,6 @@ let trim_right s =
(** the pattern that ends the parsing of options in a test file *)
let end_comment = Str.regexp ".*\\*/"
-let regex_cmxs = Str.regexp ("\\([^/]+\\)[.]cmxs\\($\\|[ \t]\\)")
-
let output_unix_error (exn : exn) =
match exn with
| Unix.Unix_error (error, _function, arg) ->
@@ -124,6 +123,7 @@ let mv src dest =
Unix.rename src dest
with Unix.Unix_error _ as e ->
output_unix_error e
+[@@ warning "-32"]
let unlink ?(silent = true) file =
let open Unix in
@@ -275,7 +275,7 @@ let example_msg =
let umsg = "Usage: frama-c-ptests [options] [names of test suites]"
let default_dune_alias = ref "ptests"
-let rec argspec =
+let argspec =
[
("-v", Arg.Unit (fun () -> incr verbosity),
"Increase verbosity (up to twice)") ;
@@ -317,7 +317,6 @@ let rec argspec =
("-dune-alias", Arg.String (fun s -> default_dune_alias := s),
" <name> Use @<name> as dune alias to exectute tests (defaults to "^ !default_dune_alias ^")");
]
-and help_msg () = Arg.usage (Arg.align argspec) umsg
let fail s =
Format.printf "Error: %s@.Aborting (CWD=%s).@." s (Sys.getcwd());
@@ -419,7 +418,6 @@ module SubDir: sig
Anyway, fails if the given dirname doesn't exists *)
val make_file: t -> string -> string
- val make_subdir: t -> string -> t
val oracle_subdir: env:env_t -> t -> t
val result_subdir: env:env_t -> t -> t
@@ -443,7 +441,6 @@ end = struct
let result_subdir ~env dir = Filename.concat dir (config_name ~env "result")
let make_file = Filename.concat
- let make_subdir = Filename.concat
let oracle_dir ~env = oracle_subdir ~env ".."
let get_oracle_dir = oracle_dir
@@ -474,8 +471,6 @@ module Macros = struct
let empty = StringMap.empty
- let macro_regex = Str.regexp "\\([^@]*\\)@\\([^@]*\\)@\\(.*\\)"
-
let pp_macros fmt macros =
Format.fprintf fmt "Macros (%d):@." (StringMap.cardinal macros);
StringMap.iter (fun key data -> Format.fprintf fmt "- %s -> %s@." key data) macros;
@@ -546,8 +541,10 @@ module Macros = struct
let s = expand ~file macros s in
if String.equal s "" then None else Some s) ls
- let get ?(default="") name macros =
- try StringMap.find name macros with Not_found -> default
+ let expand_enabled_if ~file (macros:t) enabled_if =
+ Option.map (fun s ->
+ let s = String.trim (expand ~file macros s) in
+ if s = "" then "true" else s) enabled_if
let add_list l map =
List.fold_left (fun acc (k,v) -> StringMap.add k v acc) map l
@@ -555,9 +552,6 @@ module Macros = struct
let add_expand ~file name def macros =
StringMap.add name (expand ~file macros def) macros
- let append_expand ~file name def macros =
- StringMap.add name (get name macros ^ expand ~file macros def) macros
-
let default_macros () = add_list
[ "frama-c-exe", !macro_frama_c_exe;
"frama-c-cmd", !macro_frama_c_cmd;
@@ -576,6 +570,7 @@ module Macros = struct
"PTEST_MODULE", "";
"PTEST_SCRIPT", "";
"PTEST_PLUGIN", "";
+ "PTEST_ENABLED_IF", "true";
] empty
end
@@ -586,6 +581,7 @@ type deps = {
load_libs: string list option;
load_module: string list option;
deps_cmd: string list option;
+ enabled_if: string option;
}
type execnow =
@@ -619,6 +615,7 @@ type config =
*)
dc_libs : string list option; (** libraries to compile *)
dc_deps : string list option ; (** deps *)
+ dc_enabled_if : string option ; (** enabled if condition *)
dc_plugin : string list option; (** only plugins to load *)
dc_module : string list option; (** module to load *)
dc_macros: Macros.t; (** existing macros. *)
@@ -670,11 +667,13 @@ end = struct
"PTEST_FILE", ptest_file;
"PTEST_NAME", ptest_name;
] in
- let subst = Macros.expand_list ~file
- (Macros.add_list ptest_vars Macros.empty)
+ let ptest_macros = Macros.add_list ptest_vars Macros.empty in
+ let subst = Macros.expand_list ~file ptest_macros in
+ let dc_enabled_if = Macros.expand_enabled_if ~file ptest_macros config.dc_enabled_if
in
ptest_name,
{ config with
+ dc_enabled_if;
dc_execnow = List.rev config.dc_execnow;
dc_deps = Option.map subst config.dc_deps ;
dc_plugin = Option.map subst config.dc_plugin;
@@ -698,6 +697,7 @@ end = struct
load_libs=None;
load_module=None;
deps_cmd=None;
+ enabled_if=None;
};
timeout=""
} ]
@@ -709,6 +709,7 @@ end = struct
dc_execnow = [];
dc_libs = None;
dc_deps = None;
+ dc_enabled_if = None;
dc_plugin = None;
dc_module = None;
dc_filter = None ;
@@ -788,7 +789,7 @@ end = struct
(* preserve options ordering *)
List.fold_right (fun x s -> s ^ " " ^ x) opts ""
- let deps_of_config ?(deps={load_module=None;load_libs=None;load_plugin=None;deps_cmd=None}) config =
+ let deps_of_config ?(deps={load_module=None;load_libs=None;load_plugin=None;deps_cmd=None;enabled_if=None}) config =
let select ~prev ~config = match config with
| None -> prev
| _ -> config
@@ -796,7 +797,8 @@ end = struct
{ load_module = select ~prev:deps.load_module ~config:config.dc_module;
load_plugin = select ~prev:deps.load_plugin ~config:config.dc_plugin;
load_libs= select ~prev:deps.load_libs ~config:config.dc_libs;
- deps_cmd = select ~prev:deps.deps_cmd ~config:config.dc_deps
+ deps_cmd = select ~prev:deps.deps_cmd ~config:config.dc_deps;
+ enabled_if = select ~prev:deps.enabled_if ~config:config.dc_enabled_if
}
let config_exec ~once ~drop:_ ~file ~dir s current =
@@ -828,6 +830,13 @@ end = struct
let _,_,res = (add "" acc) in
res
+ let config_enabled_if ~drop:_ ~file ~dir:_ s current =
+ let s = Macros.expand ~file current.dc_macros s in
+ let s = if s = "" then "true" else s in
+ { current with
+ dc_enabled_if = Some s;
+ dc_macros = Macros.add_list ["PTEST_ENABLED_IF", s] current.dc_macros }
+
let config_deps ~drop:_ ~file ~dir:_ s current =
let s = Macros.expand ~file current.dc_macros s in
let l = split_list s in
@@ -985,6 +994,7 @@ end = struct
"MACRO", config_macro;
"LIBS", config_libs;
"DEPS", config_deps;
+ "ENABLED_IF", config_enabled_if;
"MODULE", config_module "PTEST_MODULE";
"SCRIPT", config_module "PTEST_SCRIPT";
"PLUGIN", config_plugin;
@@ -1019,12 +1029,12 @@ end = struct
let r = ref { default with dc_commands = [] } in
let treat_line s =
try
- Scanf.sscanf s "%[ *]%[A-Za-z0-9]: %s@\n"
+ Scanf.sscanf s "%[ *]%[_A-Za-z0-9]: %s@\n"
(fun _ name opt ->
try
r := (List.assoc name config_options) ~drop ~file ~dir opt !r
with Not_found ->
- Format.eprintf "@[%s: unknown configuration option: %s@.@]" file name)
+ Format.eprintf "@[%s: unknown directive: %s@.@]" file name)
with
| Scanf.Scan_failure _ ->
if Str.string_match end_comment s 0
@@ -1143,21 +1153,6 @@ type toplevel_command =
deps: deps;
}
-type command =
- | Toplevel of toplevel_command
- | Target of execnow * command Queue.t
-
-type log = Err | Res
-
-type diff =
- | Command_error of toplevel_command * log
- | Target_error of execnow
- | Log_error of SubDir.t (* directory *) * string (* file *)
-
-type cmps =
- | Cmp_Toplevel of toplevel_command
- | Cmp_Log of SubDir.t (* directory *) * string (* file *)
-
let catenate_number nb_files prefix n =
if nb_files > 1
then prefix ^ "." ^ (string_of_int n)
@@ -1264,6 +1259,11 @@ let pp_list_deps fmt l =
(* kind={env_var,source_tree,glob_files,...} *)
Format.fprintf fmt " (%s %S)" kind deps) l
+let pp_enabled_if fmt deps =
+ Format.fprintf fmt "(and %s%a)"
+ (Option.value ~default:"true" deps.enabled_if)
+ Fmt.(list (var_libavailable framac_plugin)) (list_of_deps deps.load_plugin)
+
let pp_command_deps fmt command =
Format.fprintf fmt "%S %a (package frama-c) %a"
(* the test file *)
@@ -1408,7 +1408,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \
(targets %S %S %a %a)\n \
(deps %S %S %S %a %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (run %s %S %S %a))\n\
)@."
(* rule: *)
@@ -1427,7 +1427,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
pp_list (List.map (Filename.concat wtest.oracle_dir) command.log_files)
pp_command_deps command
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
!wrapper_cmd
wrapper_basename
@@ -1451,7 +1451,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(alias %S)\n \
(targets %S %S %a %a)\n \
(deps %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (with-stderr-to %S (with-stdout-to %S (%s (system %S)))))\n\
)@."
(* rule: *)
@@ -1466,7 +1466,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
pp_command_deps command
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
cmderrlog
cmdreslog
@@ -1478,7 +1478,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule ; FILTER %s #%d OF TEST FILE %S\n \
(deps %S)
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (with-stdout-to %S (with-accepted-exit-codes (or 0 1 2 125) (system %S))))\n\
)@."
(* rule: *)
@@ -1488,7 +1488,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
fin
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
fout cmd
in
@@ -1498,7 +1498,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule ; COMPARE TARGET #%d OF TEST #%d FOR TEST FILE %S\n \
(alias %s)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* rule: *)
@@ -1506,7 +1506,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* alias: *)
(ptests_alias ~env)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
(SubDir.make_file (SubDir.oracle_dir ~env) log)
log
@@ -1515,7 +1515,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; REPRODUCE TEST #%d OF TEST FILE %S\n \
(alias %S)\n \
(deps %a (universe))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (%s (system %S)))\n\
)@."
(* rule: *)
@@ -1525,7 +1525,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
pp_command_deps command
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
accepted_exit_code
command_string
@@ -1534,7 +1534,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
"(rule ; SHOW TEST COMMAND #%d OF TEST FILE %S\n \
(alias %S)\n \
(deps %a (universe))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1544,7 +1544,7 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
(* deps: *)
pp_command_deps command (* to get an updated build even in case of using the result *)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
("echo '" ^ show_cmd wtest.cmd ^"'");
@@ -1553,37 +1553,37 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* alias: *)
diff_alias
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
wtest.oracle_out
reslog;
Format.fprintf result_fmt
"(rule\n \
(alias %S)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* alias: *)
diff_alias
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
(* action: *)
wtest.oracle_err
errlog;
Format.fprintf result_fmt
"(alias (name %S)\n \
(deps (alias %S))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
)@."
(ptests_alias ~env)
diff_alias
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps command.deps.load_plugin)
+ pp_enabled_if command.deps
;
let oracle_subdir = SubDir.oracle_subdir ~env command.directory in
oracle_target oracle_fmt oracle_subdir (Filename.basename (oracle_prefix ^ ".err.oracle"));
@@ -1593,11 +1593,12 @@ let command_string ~env ~result_fmt ~oracle_fmt command =
let deps_command ~file macros deps =
let subst = Macros.expand_list ~file macros in
+ let enabled_if = Macros.expand_enabled_if ~file macros deps.enabled_if in
let load_plugin = Option.map subst deps.load_plugin in
let load_module = Option.map subst deps.load_module in
let load_libs = Option.map (fun libs -> List.map (fun s -> s^".cmxs") (subst libs)) deps.load_libs in
let deps_cmd = Option.map subst deps.deps_cmd in
- { load_plugin; load_module; load_libs;
+ { enabled_if; load_plugin; load_module; load_libs;
(* Merge LIBS: MODULE: and DEPS: directives as a dependency to files *)
deps_cmd = Some ((list_of_deps load_libs) @ (list_of_deps load_module) @ (list_of_deps deps_cmd));
}
@@ -1697,7 +1698,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \
(deps %a %a)\n \
(targets %a %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (run %s %%{dep:%s} %S))\n\
)@."
(* rule: *)
@@ -1711,7 +1712,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
pp_list wtest.log
pp_list wtest.bin
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
!wrapper_cmd
wrapper_basename
@@ -1731,7 +1732,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(alias %s)\n \
(deps (package frama-c)%a)\n \
(targets %a %a)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1744,7 +1745,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
pp_list wtest.log
pp_list wtest.bin
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
wtest.cmd
end;
@@ -1755,7 +1756,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
"(rule ; SHOW EXECNOW COMMAND #%d OF TEST FILE %S\n \
(alias %s)\n \
(deps %a (universe))\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (system %S))\n\
)@."
(* rule: *)
@@ -1765,7 +1766,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(* deps: *)
pp_command_deps cmd (* to get an updated build even in case of using the result *)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
("echo '" ^ show_cmd wtest.cmd ^"'");
;
@@ -1773,7 +1774,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
Format.fprintf result_fmt
"(rule ; COMPARE TARGET #%d OF EXECNOW #%d FOR TEST FILE %S\n \
(alias %s)\n \
- (enabled_if (and true %a))\n\
+ (enabled_if %a)\n\
(action (diff %S %S))\n\
)@."
(* rule: *)
@@ -1781,7 +1782,7 @@ let process_file ~env ~result_fmt ~oracle_fmt file directory config modules =
(* alias: *)
(ptests_alias ~env)
(* enabled_if: *)
- Fmt.(list (var_libavailable framac_plugin)) (list_of_deps cmd.deps.load_plugin)
+ pp_enabled_if cmd.deps
(* action: *)
(SubDir.make_file (SubDir.oracle_dir ~env) log)
log
diff --git a/ptests/tests/.gitignore b/tools/ptests/tests/.gitignore
similarity index 100%
rename from ptests/tests/.gitignore
rename to tools/ptests/tests/.gitignore
diff --git a/ptests/tests/cmd/README b/tools/ptests/tests/cmd/README
similarity index 100%
rename from ptests/tests/cmd/README
rename to tools/ptests/tests/cmd/README
diff --git a/ptests/tests/cmd/tests/ptests_config b/tools/ptests/tests/cmd/tests/ptests_config
similarity index 100%
rename from ptests/tests/cmd/tests/ptests_config
rename to tools/ptests/tests/cmd/tests/ptests_config
diff --git a/ptests/tests/cmd/tests/test_config b/tools/ptests/tests/cmd/tests/test_config
similarity index 100%
rename from ptests/tests/cmd/tests/test_config
rename to tools/ptests/tests/cmd/tests/test_config
diff --git a/ptests/tests/cmd/tests/without-test_config/README b/tools/ptests/tests/cmd/tests/without-test_config/README
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/README
rename to tools/ptests/tests/cmd/tests/without-test_config/README
diff --git a/ptests/tests/cmd/tests/without-test_config/config.i b/tools/ptests/tests/cmd/tests/without-test_config/config.i
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/config.i
rename to tools/ptests/tests/cmd/tests/without-test_config/config.i
diff --git a/ptests/tests/cmd/tests/without-test_config/empty.i b/tools/ptests/tests/cmd/tests/without-test_config/empty.i
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/empty.i
rename to tools/ptests/tests/cmd/tests/without-test_config/empty.i
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/config.0.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/config.0.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/config.0.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/config.0.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/config.1.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/config.1.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/config.1.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/config.1.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/config.2.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/config.2.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/config.2.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/config.2.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/config.3.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/config.3.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/config.3.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/config.3.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/config.4.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/config.4.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/config.4.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/config.4.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/empty.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/empty.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/empty.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/empty.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.0.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.0.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.0.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.0.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.1.res.oracle b/tools/ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.1.res.oracle
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.1.res.oracle
rename to tools/ptests/tests/cmd/tests/without-test_config/oracle/ptest-macros.1.res.oracle
diff --git a/ptests/tests/cmd/tests/without-test_config/ptest-macros.i b/tools/ptests/tests/cmd/tests/without-test_config/ptest-macros.i
similarity index 100%
rename from ptests/tests/cmd/tests/without-test_config/ptest-macros.i
rename to tools/ptests/tests/cmd/tests/without-test_config/ptest-macros.i
diff --git a/ptests/tests/nothing/README b/tools/ptests/tests/nothing/README
similarity index 100%
rename from ptests/tests/nothing/README
rename to tools/ptests/tests/nothing/README
diff --git a/ptests/tests/nothing/tests/basic/empty.i b/tools/ptests/tests/nothing/tests/basic/empty.i
similarity index 100%
rename from ptests/tests/nothing/tests/basic/empty.i
rename to tools/ptests/tests/nothing/tests/basic/empty.i
diff --git a/ptests/tests/nothing/tests/basic/opt.i b/tools/ptests/tests/nothing/tests/basic/opt.i
similarity index 100%
rename from ptests/tests/nothing/tests/basic/opt.i
rename to tools/ptests/tests/nothing/tests/basic/opt.i
diff --git a/ptests/tests/nothing/tests/basic/oracle/empty.res.oracle b/tools/ptests/tests/nothing/tests/basic/oracle/empty.res.oracle
similarity index 100%
rename from ptests/tests/nothing/tests/basic/oracle/empty.res.oracle
rename to tools/ptests/tests/nothing/tests/basic/oracle/empty.res.oracle
diff --git a/ptests/tests/nothing/tests/basic/oracle/opt.0.res.oracle b/tools/ptests/tests/nothing/tests/basic/oracle/opt.0.res.oracle
similarity index 100%
rename from ptests/tests/nothing/tests/basic/oracle/opt.0.res.oracle
rename to tools/ptests/tests/nothing/tests/basic/oracle/opt.0.res.oracle
diff --git a/ptests/tests/nothing/tests/basic/oracle/opt.1.res.oracle b/tools/ptests/tests/nothing/tests/basic/oracle/opt.1.res.oracle
similarity index 100%
rename from ptests/tests/nothing/tests/basic/oracle/opt.1.res.oracle
rename to tools/ptests/tests/nothing/tests/basic/oracle/opt.1.res.oracle
diff --git a/ptests/tests/nothing/tests/basic/oracle/opt.execnow.0 b/tools/ptests/tests/nothing/tests/basic/oracle/opt.execnow.0
similarity index 100%
rename from ptests/tests/nothing/tests/basic/oracle/opt.execnow.0
rename to tools/ptests/tests/nothing/tests/basic/oracle/opt.execnow.0
diff --git a/ptests/tests/nothing/tests/basic/oracle/opt.execnow.1 b/tools/ptests/tests/nothing/tests/basic/oracle/opt.execnow.1
similarity index 100%
rename from ptests/tests/nothing/tests/basic/oracle/opt.execnow.1
rename to tools/ptests/tests/nothing/tests/basic/oracle/opt.execnow.1
diff --git a/ptests/tests/nothing/tests/basic/oracle/opt.execnow.2 b/tools/ptests/tests/nothing/tests/basic/oracle/opt.execnow.2
similarity index 100%
rename from ptests/tests/nothing/tests/basic/oracle/opt.execnow.2
rename to tools/ptests/tests/nothing/tests/basic/oracle/opt.execnow.2
diff --git a/ptests/tests/nothing/tests/ptests_config b/tools/ptests/tests/nothing/tests/ptests_config
similarity index 100%
rename from ptests/tests/nothing/tests/ptests_config
rename to tools/ptests/tests/nothing/tests/ptests_config
diff --git a/ptests/tests/nothing/tests/test_config b/tools/ptests/tests/nothing/tests/test_config
similarity index 100%
rename from ptests/tests/nothing/tests/test_config
rename to tools/ptests/tests/nothing/tests/test_config
diff --git a/ptests/wtests.ml b/tools/ptests/wtests.ml
similarity index 100%
rename from ptests/wtests.ml
rename to tools/ptests/wtests.ml