Merge branch 'feature/andre/ci-eva-alternative-configs' into 'master'

[CI] add pipeline stage for Eva alternative configs

See merge request frama-c/frama-c!3155

.gitlab-ci.yml

@@ -121,6 +121,14 @@ CFP:
   tags:
    - nix
 
+eva-tests:
+  stage: tests
+  script:
+   - nix/frama-ci.sh build -A frama-c.eva-tests
+  tags:
+   - nix
+  allow_failure: true
+
 build-distrib-tarball:
   stage: build
   script:

nix/default.nix

@@ -223,6 +223,29 @@ pkgs.lib.makeExtensible
         '';
   };
 
+  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 -j 4
+        '';
+        installPhase = ''
+               true
+        '';
+  };
+
   e-acsl-tests-dev = mk_deriv {
         name = "frama-c-e-acsl-tests-dev";
         buildInputs = self.mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };

src/plugins/value/vtests

 #!/bin/bash -eu
 
-DEFAULT_TESTS=(float value idct builtins)
-CONFIGS=(apron equality bitwise symblocs gauges octagon)
-
-ARGS=("${@-}")
+if [ -z ${TARGETS+x} ]; then
+    TARGETS="float value idct builtins"
+fi
+if [ -z ${CONFIGS+x} ]; then
+    CONFIGS="apron equality bitwise symblocs gauges octagon"
+fi
+ARGS="${@-}"
 
 # has_target returns 0 if at least one of the arguments is a target
 # (i.e. not an option such as "-j 8"). If so, do not run tests
@@ -15,7 +18,7 @@ function has_target() {
     for f in $@; do
         __re="\\b$f\\b" # match argument as whole word
         if [[ "$f" =~ \.[ci]$ || \
-            ( "$f" =~ ^[A-Za-z] && "${DEFAULT_TESTS[@]}" =~ $__re ) ]]; then
+            ( "$f" =~ ^[A-Za-z] && "${TARGETS[@]}" =~ $__re ) ]]; then
             __has_target=0
         fi
     done
@@ -24,15 +27,15 @@ function has_target() {
 
 
 if has_target ${ARGS[@]}; then
-    TESTS=("${ARGS[@]}")
+    TARGETS="${ARGS[@]}"
 else
-    TESTS="${DEFAULT_TESTS[@]} ${ARGS[@]}"
+    TARGETS="${TARGETS[@]} ${ARGS[@]}"
 fi
 
-echo Testing ${TESTS[@]}
-
-for A in ${CONFIGS[@]}
+echo "CONFIGS: ${CONFIGS[@]}"
+echo "Testing: ${TARGETS[@]}"
+for config in ${CONFIGS[@]}
 do
-    echo $A
-    ./bin/ptests.opt -config $A ${TESTS[@]}
+    echo $config
+    ./bin/ptests.opt -error-code -config $config ${TARGETS[@]}
 done