diff --git a/src/plugins/e-acsl/.gitlab-ci.yml b/src/plugins/e-acsl/.gitlab-ci.yml index 30c46b8eacaacb1cbd8a4b411ba4c40bb100c189..cc5f22f76e3c5ca2f5c393f0aa643f349ca2246f 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 8b58780133736fc4bd884e31b5455971d05d7d04..e5f2b74f3c0fd24db54a81ae9b0c958386f1a9ef 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 0000000000000000000000000000000000000000..6c41960f846c6e6ed7cc5b386ba6ae683cb0189c --- /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 0000000000000000000000000000000000000000..d90edd7caf5d5d946acf2df948b2f359f2cfbf00 --- /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 0000000000000000000000000000000000000000..b4a69f90154968218273a70d50be6173a2909841 --- /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 $@