From 8ff99de455b890346728a04df3ae714b776102b7 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Tue, 29 Sep 2020 08:39:04 +0200
Subject: [PATCH] =?UTF-8?q?[ci]=20add=20Aora=C3=AF's=20test=20config=20'pr?=
=?UTF-8?q?ove'=20to=20the=20CI=20(allowing=20failure=20for=20now)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
---
.gitlab-ci.yml | 8 ++++++++
nix/default.nix | 30 ++++++++++++++++++++++++++++++
2 files changed, 38 insertions(+)
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index 7e14dfd7ff3..b86b0826b80 100644
--- a/.gitlab-ci.yml
+++ b/.gitlab-ci.yml
@@ -57,6 +57,14 @@ wp-qualif:
- nix
allow_failure: true
+aorai-prove:
+ stage: tests
+ script:
+ - nix/frama-ci.sh build -A frama-c.aorai-prove
+ tags:
+ - nix
+ allow_failure: true
+
genassigns:
stage: tests
script:
diff --git a/nix/default.nix b/nix/default.nix
index b3e6929a292..7a4cc5ffedb 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -187,6 +187,36 @@ rec {
'';
};
+ aorai-prove = mk_deriv {
+ name = "frama-c-aorai-prove";
+ buildInputs = mk_buildInputs { opamPackages = [
+ { name = "alt-ergo"; constraint = "=2.0.0"; }
+ ]; };
+ build_dir = main.build_dir;
+ src = 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 --full-config
+ make src/plugins/aorai/tests/ptests_config
+ make PTESTS_OPTS="-config prove -error-code" Aorai_TESTS
+ '';
+
+ installPhase = ''
+ true
+ '';
+ };
+
e-acsl-tests-dev = mk_deriv {
name = "frama-c-e-acsl-tests-dev";
buildInputs = mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };
--
GitLab