diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index eb537b5f5efbcce287a5faf2f3a2cb5d8ea9b153..f7637e3d1d8a00b596be9bd9400de0bb35411136 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -76,10 +76,24 @@ genassigns: tags: - nix -main-tests: +e-acsl-tests: stage: tests script: - - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.main-tests + - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.e-acsl-tests + tags: + - nix + +eva-tests: + stage: tests + script: + - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.eva-tests + tags: + - nix + +kernel-tests: + stage: tests + script: + - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.kernel-tests tags: - nix @@ -118,6 +132,14 @@ volatile: tags: - nix +wp-tests: + stage: tests + script: + - nix-build nix/pkgs.nix -A ocaml-ng.ocamlPackages_4_12.wp-tests + tags: + - nix + + ################################################################################ ### DISTRIB diff --git a/nix/e-acsl-tests.nix b/nix/e-acsl-tests.nix new file mode 100644 index 0000000000000000000000000000000000000000..98edfa6fcaeb17653ec2da9774e5ff22a26307a0 --- /dev/null +++ b/nix/e-acsl-tests.nix @@ -0,0 +1,45 @@ +{ lib +, stdenvNoCC +, frama-c +, perl +, pkgs +, time +, which +}: + +stdenvNoCC.mkDerivation rec { + pname = "e-acsl-tests"; + version = frama-c.version; + slang = frama-c.slang; + + build_dir = frama-c.build_dir; + src = build_dir + "/dir.tar"; + sourceRoot = "."; + + buildInputs = frama-c.buildInputs ++ [ + frama-c + perl + pkgs.getopt + time + which + ]; + + postPatch = '' + patchShebangs . + '' ; + + # Keep main configuration + configurePhase = '' + true + ''; + + buildPhase = '' + dune exec -- frama-c-ptests tests src/plugins/*/tests + dune build -j1 --display short @src/plugins/e-acsl/tests/ptests + ''; + + # No installation required + installPhase = '' + touch $out + ''; +} diff --git a/nix/main-tests.nix b/nix/eva-tests.nix similarity index 73% rename from nix/main-tests.nix rename to nix/eva-tests.nix index 1c4c3d60e2fd39c63fc19bcf4f6222db901fa0a8..ff192302ecd9a5a05fba63d6437f4590d5ead753 100644 --- a/nix/main-tests.nix +++ b/nix/eva-tests.nix @@ -7,7 +7,7 @@ }: stdenvNoCC.mkDerivation rec { - pname = "main-tests"; + pname = "eva-tests"; version = frama-c.version; slang = frama-c.slang; @@ -33,7 +33,12 @@ stdenvNoCC.mkDerivation rec { buildPhase = '' dune exec -- frama-c-ptests tests - dune build -j1 --display short @tests/ptests + dune build -j1 --display short \ + @tests/builtins/ptests \ + @tests/float/ptests \ + @tests/idct/ptests \ + @tests/value/ptests \ + @tests/value/traces/ptests ''; # No installation required diff --git a/nix/frama-c.nix b/nix/frama-c.nix index 347ca1f1225f16a076bd463f305311197f51af10..34d0802ce288a8f63d33b0a58d16a5fca606b806 100644 --- a/nix/frama-c.nix +++ b/nix/frama-c.nix @@ -84,6 +84,8 @@ stdenvNoCC.mkDerivation rec { preConfigure = '' autoconf + patchShebangs src/plugins/value/gen-api.sh + chmod +x src/plugins/value/gen-api.sh ''; # Do not use default parallel building, but allow 2 cores for Frama-C build diff --git a/nix/kernel-tests.nix b/nix/kernel-tests.nix new file mode 100644 index 0000000000000000000000000000000000000000..5d85217fb0e8fc6cbf768f6e7f53927868d67c9c --- /dev/null +++ b/nix/kernel-tests.nix @@ -0,0 +1,53 @@ +{ lib +, stdenv +, frama-c +, perl +, time +, which +}: + +stdenv.mkDerivation rec { + pname = "kernel-tests"; + version = frama-c.version; + slang = frama-c.slang; + + build_dir = frama-c.build_dir; + src = build_dir + "/dir.tar"; + sourceRoot = "."; + + buildInputs = frama-c.buildInputs ++ [ + frama-c + perl + time + which + ]; + + postPatch = '' + patchShebangs . + '' ; + + # Keep main configuration + configurePhase = '' + true + ''; + + buildPhase = '' + dune exec -- frama-c-ptests tests + dune build -j1 --display short \ + @tests/cil/ptests \ + @tests/compliance/ptests \ + @tests/jcdb/ptests \ + @tests/libc/ptests \ + @tests/misc/ptests \ + @tests/pretty_printing/ptests \ + @tests/saveload/ptests \ + @tests/spec/ptests \ + @tests/syntax/ptests \ + @tests/test/ptests + ''; + + # No installation required + installPhase = '' + touch $out + ''; +} diff --git a/nix/pkgs.nix b/nix/pkgs.nix index 410524ec23f89f3a2b943b15f4d0969a90d037d5..9ad873a8e05ef05ba66ea97621c0d6c8e89e241e 100644 --- a/nix/pkgs.nix +++ b/nix/pkgs.nix @@ -49,8 +49,11 @@ let frama-c = oself.callPackage ./frama-c.nix {}; lint = oself.callPackage ./lint.nix {}; # Tests - main-tests = oself.callPackage ./main-tests.nix {}; + e-acsl-tests = oself.callPackage ./e-acsl-tests.nix {}; + eva-tests = oself.callPackage ./eva-tests.nix {}; + kernel-tests = oself.callPackage ./kernel-tests.nix {}; plugins-tests = oself.callPackage ./plugins-tests.nix {}; + wp-tests = oself.callPackage ./wp-tests.nix {}; # Release manuals = oself.callPackage ./manuals.nix {}; }; diff --git a/nix/plugins-tests.nix b/nix/plugins-tests.nix index 2efa68eca20af3637ccb488a97c96df3c87b8ae1..aab6e9d288c6082f37da2ff585fa730136701d3d 100644 --- a/nix/plugins-tests.nix +++ b/nix/plugins-tests.nix @@ -3,12 +3,10 @@ , frama-c , alt-ergo , perl -, pkgs , time , which }: -# TODO: SPLIT THIS stdenvNoCC.mkDerivation rec { pname = "plugins-tests"; version = frama-c.version; @@ -16,14 +14,13 @@ stdenvNoCC.mkDerivation rec { build_dir = frama-c.build_dir; src = build_dir + "/dir.tar"; - wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"; # only for WP qualif / Aorai + wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"; # for Aorai sourceRoot = "."; buildInputs = frama-c.buildInputs ++ [ - alt-ergo # only for WP qualif / Aorai + alt-ergo # only for Aorai frama-c perl - pkgs.getopt # only for E-ACSL time which ]; @@ -33,7 +30,7 @@ stdenvNoCC.mkDerivation rec { '' ; # Keep main configuration - # Only for WP qualif / Aorai -> replace with true after split + # But for Aorai, configure Why3 configurePhase = '' mkdir home HOME=$(pwd)/home @@ -41,9 +38,29 @@ stdenvNoCC.mkDerivation rec { ''; buildPhase = '' - export FRAMAC_WP_CACHEDIR=$wp_cache # only for WP qualif / Aorai - dune exec -- frama-c-ptests src/plugins/*/tests - dune build -j1 --display short @src/plugins/ptests + export FRAMAC_WP_CACHEDIR=$wp_cache # for Aorai + dune exec -- frama-c-ptests tests src/plugins/*/tests + dune build -j1 --display short \ + @tests/callgraph/ptests \ + @tests/constant_propagation/ptests \ + @tests/impact/ptests \ + @tests/metrics/ptests \ + @tests/occurrence/ptests \ + @tests/pdg/ptests \ + @tests/slicing/ptests \ + @tests/rte/ptests \ + @tests/rte_manual/ptests \ + @tests/scope/ptests \ + @tests/sparecode/ptests \ + @src/plugins/aorai/tests/ptests \ + @src/plugins/dive/tests/ptests \ + @src/plugins/instantiate/tests/ptests \ + @src/plugins/loop_analysis/tests/ptests \ + @src/plugins/markdown-report/tests/ptests \ + @src/plugins/nonterm/tests/ptests \ + @src/plugins/report/tests/ptests \ + @src/plugins/server/tests/ptests \ + @src/plugins/variadic/tests/ptests ''; # No installation required diff --git a/nix/wp-tests.nix b/nix/wp-tests.nix new file mode 100644 index 0000000000000000000000000000000000000000..4dbd1d862751729de1ed95aa8fa13ed69b52bae5 --- /dev/null +++ b/nix/wp-tests.nix @@ -0,0 +1,48 @@ +{ lib +, stdenv +, frama-c +, alt-ergo +, perl +, time +, which +}: + +stdenv.mkDerivation rec { + pname = "wp-tests"; + version = frama-c.version; + slang = frama-c.slang; + + build_dir = frama-c.build_dir; + src = build_dir + "/dir.tar"; + wp_cache = fetchGit "git@git.frama-c.com:frama-c/wp-cache.git"; + sourceRoot = "."; + + buildInputs = frama-c.buildInputs ++ [ + alt-ergo + frama-c + perl + time + which + ]; + + postPatch = '' + patchShebangs . + '' ; + + configurePhase = '' + mkdir home + HOME=$(pwd)/home + why3 config detect + ''; + + buildPhase = '' + export FRAMAC_WP_CACHEDIR=$wp_cache + dune exec -- frama-c-ptests src/plugins/wp/tests + dune build -j1 --display short @src/plugins/wp/tests/ptests + ''; + + # No installation required + installPhase = '' + touch $out + ''; +} diff --git a/tests/ptests_config b/tests/ptests_config index 6bbe5b311927ab33916c4841a63725d885a4d790..70332483028713b96de034189156f90559f3f766 100644 --- a/tests/ptests_config +++ b/tests/ptests_config @@ -2,18 +2,24 @@ # todo: adds crowbar? Yes, but these tests do not use ptests # todo: adds journal? No, the journal suite directory will be removed later to master -DEFAULT_SUITES= builtins callgraph cil compliance constant_propagation dynamic -DEFAULT_SUITES= float idct impact jcdb libc metrics occurrence pdg pretty_printing -DEFAULT_SUITES= rte rte_manual saveload scope slicing sparecode spec syntax +### Tests of kernel -DEFAULT_SUITES= misc fc_script +DEFAULT_SUITES= cil compliance dynamic fc_script jcdb libc misc +DEFAULT_SUITES= pretty_printing saveload spec syntax test -DEFAULT_SUITES= value/traces value test +### Tests of small plugins + +DEFAULT_SUITES= callgraph constant_propagation impact metrics occurrence pdg +DEFAULT_SUITES= rte rte_manual scope slicing sparecode + +### Tests of EVA + +DEFAULT_SUITES= builtins float idct value value/traces # todo: adds value/numerors (requires opam package mlgmpidl and system libraries for MPFR) IGNORE= DEFAULT_SUITES= value/numerors -### tests of EVA domains +### Tests of EVA domains apron_SUITES = bitwise_SUITES = value builtins float idct equality_SUITES = value builtins float idct