From 8efcc298a86bf82a0feb136c80dbfd8fdc6c7be6 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 24 Oct 2018 11:36:25 +0200
Subject: [PATCH] [nix] compacted update
---
src/plugins/e-acsl/.gitlab-ci.yml | 55 +++++++++++++++++++++++------
src/plugins/e-acsl/Makefile.in | 17 ++++++---
src/plugins/e-acsl/nix/default.nix | 11 ++++++
src/plugins/e-acsl/nix/frama-ci.nix | 15 ++++++++
src/plugins/e-acsl/nix/frama-ci.sh | 12 +++++++
5 files changed, 96 insertions(+), 14 deletions(-)
create mode 100644 src/plugins/e-acsl/nix/default.nix
create mode 100644 src/plugins/e-acsl/nix/frama-ci.nix
create mode 100755 src/plugins/e-acsl/nix/frama-ci.sh
diff --git a/src/plugins/e-acsl/.gitlab-ci.yml b/src/plugins/e-acsl/.gitlab-ci.yml
index 30c46b8eaca..cc5f22f76e3 100644
--- a/src/plugins/e-acsl/.gitlab-ci.yml
+++ b/src/plugins/e-acsl/.gitlab-ci.yml
@@ -1,20 +1,55 @@
+stages:
+ - build
+ - tests
+
+E-ACSL:
+ stage: build
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "test-nix"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
+ script:
+ - nix/frama-ci.sh build -A e-acsl.installed
+ tags:
+ - nix
+ retry: 2
+
Tests:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "test-nix"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME E-ACSL --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A e-acsl.tests
tags:
- except:
- - tags
+ - nix
+ retry: 2
-context-from-precondition:
+Cfp:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "test-nix"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME context-from-precondition --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A context-from-precondition.tests
tags:
- except:
- - tags
+ - nix
+ retry: 2
Security:
+ stage: tests
+ variables:
+ CURRENT: $CI_COMMIT_REF_NAME
+ DEFAULT: "test-nix"
+ OCAML: "4_05"
+ FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
script:
- - ~oci/oci/bin/bf_client.native run --socket ~oci/data/oci-data/oci.socket --E-ACSL $CI_BUILD_REF --branch $CI_BUILD_REF_NAME Security --cppo 07d2bcee50670aecae7e094d92f68fd18314073a --ocamlgraph 9286b375c005d1d504a1def0c5986f54c7f12251 --url ocamlfind,git@git.frama-c.com:bobot/ocamlfind.git
+ - nix/frama-ci.sh build -A security.tests
tags:
- except:
- - tags
+ - nix
+ retry: 2
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 8b587801337..e5f2b74f3c0 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/src/plugins/e-acsl/Makefile.in
@@ -133,6 +133,16 @@ $(EACSL_PLUGIN_DIR)/local_config.ml: $(EACSL_PLUGIN_DIR)/Makefile.in $(VERSION_F
ifeq (@MAY_RUN_TESTS@,yes)
+-include in_frama_ci
+
+ifeq ($(IN_FRAMA_CI),yes)
+
+PLUGIN_TESTS_DIRS := \
+ gmp \
+ no-main
+
+else
+
PLUGIN_TESTS_DIRS := \
format \
reject \
@@ -141,11 +151,10 @@ PLUGIN_TESTS_DIRS := \
gmp \
no-main \
full-mmodel \
- temporal
+ temporal \
+ builtin
-# the following test suite is deactivated for the time being:
-# uncompatible with OCI
-# builtin
+endif
PLUGIN_TESTS_LIB := $(EACSL_PLUGIN_DIR)/tests/print.ml
E_ACSL_TESTS: $(EACSL_PLUGIN_DIR)/tests/test_config
diff --git a/src/plugins/e-acsl/nix/default.nix b/src/plugins/e-acsl/nix/default.nix
new file mode 100644
index 00000000000..6c41960f846
--- /dev/null
+++ b/src/plugins/e-acsl/nix/default.nix
@@ -0,0 +1,11 @@
+# paramaterised derivation with dependencies injected (callPackage style)
+{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocamlPackages_latest.ocaml", plugins ? { } }:
+
+plugins.helpers.simple_plugin
+ { inherit pkgs stdenv src opam2nix ocaml_version plugins;
+ deps = [ pkgs.getopt pkgs.which ];
+ name = "e-acsl";
+ preBuild = ''
+ echo IN_FRAMA_CI=yes > in_frama_ci
+ '';
+ }
diff --git a/src/plugins/e-acsl/nix/frama-ci.nix b/src/plugins/e-acsl/nix/frama-ci.nix
new file mode 100644
index 00000000000..d90edd7caf5
--- /dev/null
+++ b/src/plugins/e-acsl/nix/frama-ci.nix
@@ -0,0 +1,15 @@
+#To copy in other repository
+{ pkgs ? import <nixpkgs> {}, password}:
+
+let
+ src = builtins.fetchGit {
+ "url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
+ "name" = "Frama-CI";
+ "rev" = "d8d527e3716e3190aa89b48ee417a0618c0f3408";
+ "ref" = "master";
+ };
+ in
+ {
+ src = src;
+ compiled = pkgs.callPackage "${src}/compile.nix" { inherit pkgs; };
+ }
diff --git a/src/plugins/e-acsl/nix/frama-ci.sh b/src/plugins/e-acsl/nix/frama-ci.sh
new file mode 100755
index 00000000000..b4a69f90154
--- /dev/null
+++ b/src/plugins/e-acsl/nix/frama-ci.sh
@@ -0,0 +1,12 @@
+#!/bin/sh -eu
+
+DIR=$(dirname $0)
+
+export FRAMA_CI_NIX=$DIR/frama-ci.nix
+
+export FRAMA_CI=$(nix-instantiate --eval -E "((import <nixpkgs> {}).callPackage $FRAMA_CI_NIX { password = \"$TOKEN_FOR_API\";}).src.outPath")
+
+FRAMA_CI=${FRAMA_CI#\"}
+FRAMA_CI=${FRAMA_CI%\"}
+
+$FRAMA_CI/compile.sh $@
--
GitLab