Merge branch 'e-acsl-import/feature/julien/tests_dev_for_ci' into 'master'

[ci] ajout de la config dev à CI

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

.gitlab-ci.yml

@@ -212,7 +212,14 @@ pathcrawler:
   tags:
    - nix
 
-
+e-acsl-tests-dev:
+  stage: tests
+  variables:
+    OCAML: "4_05"
+  script:
+   - nix/frama-ci.sh build -A frama-c.e-acsl-tests-dev
+  tags:
+   - nix
 
 make_public:
   stage: make_public
@@ -224,4 +231,4 @@ make_public:
   tags:
   - nix
   only:
-  - schedules
\ No newline at end of file
+  - schedules

nix/default.nix

@@ -178,10 +178,32 @@ rec {
         '';
   };
 
+  e-acsl-tests-dev = stdenv.mkDerivation {
+        name = "frama-c-e-acsl-tests-dev";
+        buildInputs = mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };
+        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 "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
+               make E_ACSL_TESTS PTESTS_OPTS="-error-code" DEV=yes
+        '';
+        installPhase = ''
+               true
+        '';
+  };
+
   internal = stdenv.mkDerivation {
         name = "frama-c-internal";
         inherit src;
-        buildInputs = (mk_buildInputs { opamPackages = [ "xml-light" ];} ) ++
+        buildInputs = (mk_buildInputs { opamPackages = [ "xml-light" ]; } ) ++
                     [ pkgs.getopt pkgs.which
                       pkgs.libxslt pkgs.libxml2 pkgs.autoPatchelfHook stdenv.cc.cc.lib
         ];

src/plugins/e-acsl/.gitlab-ci.yml

-stages:
- - git-update
- - build
- - tests
-
-variables:
-    CURRENT: $CI_COMMIT_REF_NAME
-    DEFAULT: "master"
-    OCAML: "4_05"
-    FRAMA_CI_OPT: "--override e-acsl:$CI_COMMIT_REF_NAME,$CI_COMMIT_SHA"
-
-
-#avoid a nix error https://github.com/NixOS/nix/issues/2087
-git-update:
-  stage: git-update
-  script:
-   - nix/frama-ci.sh instantiate --eval -A e-acsl.src.outPath
-  tags:
-   - nix
-
-E-ACSL:
-  stage: build
-  script:
-   - nix/frama-ci.sh build -A e-acsl.installed
-  tags:
-   - nix
-
-CheckHeaders:
-  stage: build
-  script:
-   - nix/frama-ci.sh build -A genassigns.checkHeaders
-  tags:
-   - nix
-
-Tests:
-  stage: tests
-  script:
-   - nix/frama-ci.sh build -A e-acsl.tests
-  tags:
-   - nix
-
-Cfp:
-  stage: tests
-  script:
-   - nix/frama-ci.sh build -A context-from-precondition.tests
-  tags:
-   - nix
-
-Security:
-  stage: tests
-  script:
-   - nix/frama-ci.sh build -A security.tests
-  tags:
-   - nix

src/plugins/e-acsl/Makefile.in

@@ -175,12 +175,14 @@ else
 endif
 PLUGIN_PTESTS_OPTS:=-config $(EACSL_TEST_CONFIG)
 
-E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: \
+TEST_DEPENDENCIES:= \
 	$(EACSL_PLUGIN_DIR)/tests/ptests_config \
 	$(EACSL_PLUGIN_DIR)/tests/test_config_$(EACSL_TEST_CONFIG) \
 	$(EACSL_PLUGIN_DIR)/tests/print.cmxs \
 	$(EACSL_PLUGIN_DIR)/tests/print.cmo
 
+E_ACSL_TESTS E_ACSL_DEFAULT_TESTS: $(TEST_DEPENDENCIES)
+tests:: $(TEST_DEPENDENCIES)
 
 $(EACSL_PLUGIN_DIR)/tests/test_config_ci: \
 		$(EACSL_PLUGIN_DIR)/tests/test_config_ci.in \
@@ -194,8 +196,6 @@ $(EACSL_PLUGIN_DIR)/tests/test_config_dev: \
 	$(PRINT_MAKING) $@
 	$(SED) -e "s|@SEDCMD@|`which sed `|g" $< > $@
 
-tests:: $(EACSL_PLUGIN_DIR)/tests/ptests_config
-
 clean::
 	for d in $(E_ACSL_EXTRA_DIRS); do \
 	  $(RM) $$d/*~; \
@@ -254,7 +254,9 @@ clean::
 
 EACSL_CLEANFILES = doc/doxygen/doxygen.cfg \
 	Makefile config.log config.status configure .depend autom4te.cache/* \
-	META.frama-c-e_acsl Makefile.plugin.generated src/local_config.ml top/*
+	META.frama-c-e_acsl Makefile.plugin.generated src/local_config.ml \
+	top/* \
+	$(TEST_DEPENDENCIES)
 
 e-acsl-distclean: clean
 	$(PRINT_RM) generated project files

src/plugins/e-acsl/nix/default.nix

-# 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
-    '';
-  }

src/plugins/e-acsl/nix/frama-ci.nix

-#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" = "cea0f2d2872e59fd3e6fe4634891a3765c7036e8";
-            "ref" = "master";
-    };
- in
- {
-  src = src;
-  compiled = pkgs.callPackage "${src}/compile.nix" { inherit pkgs; };
- }

src/plugins/e-acsl/nix/frama-ci.sh

-#!/bin/sh -eu
-
-DIR=$(dirname $0)
-
-export FRAMA_CI_NIX=$DIR/frama-ci.nix
-
-export FRAMA_CI=$(nix-instantiate --eval -E "((import <nixos-19.03> {}).callPackage $FRAMA_CI_NIX  { password = \"$TOKEN_FOR_API\";}).src.outPath")
-
-FRAMA_CI=${FRAMA_CI#\"}
-FRAMA_CI=${FRAMA_CI%\"}
-
-$FRAMA_CI/compile.sh $@

src/plugins/e-acsl/tests/bts/bts1398.c

-/* run.config
+/* run.config_dev
+   COMMENT: issue with printf on CI
+   DONTRUN:
+*/
+/* run.config_ci
    COMMENT: variadic function call
 */
 

src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/bts/bts1398.c:12: Warning: 
+[kernel:annot:missing-spec] tests/bts/bts1398.c:16: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype

src/plugins/e-acsl/tests/builtin/test_config_dev

 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
-EXEC: ./scripts/e-acsl-gcc.sh --libc-replacements -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
+EXEC: ./scripts/e-acsl-gcc.sh --libc-replacements -I @frama-c@ -D -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.out.e-acsl > /dev/null

src/plugins/e-acsl/tests/format/test_config_dev

 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
-EXEC: ./scripts/e-acsl-gcc.sh --validate-format-strings -q -c -X --frama-c-extra="-verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
+EXEC: ./scripts/e-acsl-gcc.sh --validate-format-strings -I @frama-c@ -q -c -X --frama-c-extra="-verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.out.e-acsl > /dev/null

src/plugins/e-acsl/tests/full-mmodel/addrOf.i

-/* run.config
+/* run.config_dev
+   COMMENT: issue with function pointers on CI
+   DONTRUN:
+*/
+/* run.config_ci
    COMMENT: addrOf
 */
 

src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c

@@ -19,7 +19,7 @@ void f(void)
     int __gen_e_acsl_initialized;
     __gen_e_acsl_initialized = __e_acsl_initialized((void *)p,sizeof(int));
     __e_acsl_assert(__gen_e_acsl_initialized,(char *)"Assertion",(char *)"f",
-                    (char *)"\\initialized(p)",10);
+                    (char *)"\\initialized(p)",14);
   }
   /*@ assert \initialized(p); */ ;
   __e_acsl_delete_block((void *)(& p));
@@ -68,7 +68,7 @@ int main(void)
   __e_acsl_full_init((void *)(& x));
   f();
   __e_acsl_assert(& x == & x,(char *)"Assertion",(char *)"main",
-                  (char *)"&x == &x",16);
+                  (char *)"&x == &x",20);
   /*@ assert &x ≡ &x; */ ;
   __e_acsl_full_init((void *)(& __retres));
   __retres = 0;

src/plugins/e-acsl/tests/full-mmodel/test_config_dev

 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
-EXEC: ./scripts/e-acsl-gcc.sh --full-mmodel -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
+EXEC: ./scripts/e-acsl-gcc.sh --full-mmodel -I @frama-c@ -D -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.out.e-acsl > /dev/null

src/plugins/e-acsl/tests/gmp-only/test_config_dev

 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
-EXEC: ./scripts/e-acsl-gcc.sh --gmp -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
+EXEC: ./scripts/e-acsl-gcc.sh --gmp -I @frama-c@ -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.out.e-acsl > /dev/null

src/plugins/e-acsl/tests/memory/constructor.c

-/* run.config
+/* run.config_dev
+   COMMENT: issue with printf on CI
+   DONTRUN:
+*/
+/* run.config_ci
    COMMENT: bts #2405. Memory not initialized for code executed before main.
 */
 
@@ -15,4 +19,4 @@ void f() {
 int main() {
   printf("main\n");
   return 0;
-}
\ No newline at end of file
+}

src/plugins/e-acsl/tests/memory/hidden_malloc.c

-/* run.config
+/* run.config_dev
+   COMMENT: issue on CI
+   DONTRUN:
+*/
+/* run.config_ci
    COMMENT: Malloc executed by a library function
 */
 

src/plugins/e-acsl/tests/memory/local_goto.c

-/* run.config
+/* run.config_dev
+   COMMENT: issue with printf on CI
+   DONTRUN:
+*/
+/* run.config_ci
    COMMENT: Check that deleting statements before goto jumps takes into
    COMMENT: account variable declarations given via local inits
 */

src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/constructor.c:16: Warning: 
+[kernel:annot:missing-spec] tests/memory/constructor.c:20: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype

src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c

@@ -54,7 +54,7 @@ int main(int argc, char const **argv)
       __gen_e_acsl_valid = __e_acsl_valid((void *)(& a),sizeof(int),
                                           (void *)(& a),(void *)0);
       __e_acsl_assert(__gen_e_acsl_valid,(char *)"Assertion",(char *)"main",
-                      (char *)"\\valid(&a)",25);
+                      (char *)"\\valid(&a)",29);
     }
     /*@ assert \valid(&a); */ ;
     if (t == 2) {
@@ -71,7 +71,7 @@ int main(int argc, char const **argv)
       __gen_e_acsl_valid_2 = __e_acsl_valid((void *)(& b),sizeof(int),
                                             (void *)(& b),(void *)0);
       __e_acsl_assert(__gen_e_acsl_valid_2,(char *)"Assertion",
-                      (char *)"main",(char *)"\\valid(&b)",36);
+                      (char *)"main",(char *)"\\valid(&b)",40);
     }
     /*@ assert \valid(&b); */ ;
     printf(__gen_e_acsl_literal_string_2,t,__gen_e_acsl_literal_string_4);

src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle

-[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: Warning: 
+[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:15: Warning: 
   Calling undeclared function realpath. Old style K&R code?
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:11: Warning: 
+[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:15: Warning: 
   Neither code nor specification for function realpath, generating default assigns from the prototype
-[eva:invalid-assigns] tests/memory/hidden_malloc.c:11: 
+[eva:invalid-assigns] tests/memory/hidden_malloc.c:15: 
   Completely invalid destination for assigns clause *((char *)x_1 + (0 ..)).
   Ignoring.

src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle

 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] tests/memory/local_goto.c:37: Warning: 
+[kernel:annot:missing-spec] tests/memory/local_goto.c:41: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype

src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle

+[kernel] Parsing tests/memory/ghost_parameters.i (no preprocessing)

src/plugins/e-acsl/tests/temporal/test_config_dev

@@ -2,4 +2,4 @@ DONTRUN:
 MACRO: DEST @PTEST_RESULT@/gen_@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
-EXEC: ./scripts/e-acsl-gcc.sh --temporal -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
+EXEC: ./scripts/e-acsl-gcc.sh --temporal -I @frama-c@ -D -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.run.c -O @DEST@.out @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.out.e-acsl > /dev/null

src/plugins/e-acsl/tests/test_config_dev.in

 MACRO: DEST @PTEST_RESULT@/@PTEST_NAME@
 MACRO: OUT @PTEST_NAME@.res.log
 MACRO: ERR @PTEST_NAME@.err.log
-EXEC: BIN @DEST@.gcc.c ./scripts/e-acsl-gcc.sh -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null
+EXEC: ./scripts/e-acsl-gcc.sh -I @frama-c@ -D -q -c -X --frama-c-extra="-journal-disable -verbose 0 -kernel-warn-key *=inactive" -o @DEST@.gcc.c -O @DEST@ @PTEST_FILE@ > @PTEST_RESULT@/@OUT@ 2> @PTEST_RESULT@/@ERR@ && ./@DEST@.e-acsl > /dev/null