From 9b95c12584b940970c8962783f6ed6eb49be4eb5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 26 Apr 2021 17:14:11 +0200
Subject: [PATCH] [CI] add pipeline stage for Eva alternative configs; improve
vtests script
---
.gitlab-ci.yml | 8 ++++++++
nix/default.nix | 21 +++++++++++++++++++++
src/plugins/value/vtests | 27 +++++++++++++++------------
3 files changed, 44 insertions(+), 12 deletions(-)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 1587d00f7d5..51eb4ef5182 100644
--- a/.gitlab-ci.yml
+++ b/.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:
diff --git a/nix/default.nix b/nix/default.nix
index 8ce82489000..769c6bbebcc 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -223,6 +223,27 @@ 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 = ''
+ export CONFIGS="equality bitwise symblocs gauges octagon"
+ src/plugins/value/vtests
+ '';
+ installPhase = ''
+ true
+ '';
+ };
+
e-acsl-tests-dev = mk_deriv {
name = "frama-c-e-acsl-tests-dev";
buildInputs = self.mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };
diff --git a/src/plugins/value/vtests b/src/plugins/value/vtests
index 03d9e24b6d1..d3fa638f3fc 100755
--- a/src/plugins/value/vtests
+++ b/src/plugins/value/vtests
@@ -1,9 +1,12 @@
#!/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
--
GitLab