Merge branch 'bugfix/basile/eacsl-67-always-inline' into 'master'

[tests] Deactivate Nix's GCC hardening for all frama-c derivations

Closes #710 and e-acsl#67

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

nix/default.nix

@@ -15,13 +15,20 @@ let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
            ocamlAttr = ocaml_version;
         };
 
+    # Extends the call to stdenv.mkDerivation with parameters common for all
+    # frama-c derivations
+    mk_deriv = args:
+        stdenv.mkDerivation ({
+            # Disable Nix's GCC hardening
+            hardeningDisable = [ "all" ];
+        } // args);
 in
 
 rec {
   inherit src mk_buildInputs;
   buildInputs = mk_buildInputs {};
   installed = main.out;
-  main = stdenv.mkDerivation {
+  main = mk_deriv {
         name = "frama-c";
         inherit src buildInputs;
         outputs = [ "out" "build_dir" ];
@@ -63,7 +70,7 @@ rec {
         '';
   };
 
-  lint = stdenv.mkDerivation {
+  lint = mk_deriv {
         name = "frama-c-lint";
         inherit src;
         buildInputs = (mk_buildInputs { opamPackages = [ { name = "ocp-indent"; constraint = "=1.7.0"; } ];} )
@@ -87,7 +94,7 @@ rec {
         '';
   };
 
-  tests = stdenv.mkDerivation {
+  tests = mk_deriv {
         name = "frama-c-test";
         inherit buildInputs;
         build_dir = main.build_dir;
@@ -109,7 +116,7 @@ rec {
         '';
   };
 
-  build-distrib-tarball = stdenv.mkDerivation {
+  build-distrib-tarball = mk_deriv {
         name = "frama-c-build-distrib-tarball";
         inherit src;
         buildInputs = buildInputs ++ [ plugins.headache.installed ];
@@ -132,7 +139,7 @@ rec {
         '';
   };
 
-  build-from-distrib-tarball = stdenv.mkDerivation {
+  build-from-distrib-tarball = mk_deriv {
         name = "frama-c-build-from-distrib-tarball";
         inherit buildInputs;
         src = build-distrib-tarball.out ;
@@ -150,7 +157,7 @@ rec {
         '';
   };
 
-  wp-qualif = stdenv.mkDerivation {
+  wp-qualif = mk_deriv {
         name = "frama-c-wp-qualif";
         buildInputs = mk_buildInputs { opamPackages = [
                     { name = "alt-ergo"; constraint = "=2.0.0"; }
@@ -180,7 +187,7 @@ rec {
         '';
   };
 
-  e-acsl-tests-dev = stdenv.mkDerivation {
+  e-acsl-tests-dev = mk_deriv {
         name = "frama-c-e-acsl-tests-dev";
         buildInputs = mk_buildInputs { nixPackages = [ pkgs.gmp pkgs.getopt ]; };
         build_dir = main.build_dir;
@@ -202,7 +209,7 @@ rec {
         '';
   };
 
-  internal = stdenv.mkDerivation {
+  internal = mk_deriv {
         name = "frama-c-internal";
         inherit src;
         buildInputs = (mk_buildInputs { opamPackages = [ "xml-light" ]; } ) ++

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

-/* 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:16: Warning: 
+[kernel:annot:missing-spec] tests/bts/bts1398.c:12: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype

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

-/* 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,"Assertion","f",
-                    "\\initialized(p)","tests/full-mmodel/addrOf.i",14);
+                    "\\initialized(p)","tests/full-mmodel/addrOf.i",10);
   }
   /*@ assert \initialized(p); */ ;
   __e_acsl_delete_block((void *)(& p));
@@ -82,7 +82,7 @@ int main(void)
   __e_acsl_full_init((void *)(& x));
   f();
   __e_acsl_assert(& x == & x,"Assertion","main","&x == &x",
-                  "tests/full-mmodel/addrOf.i",20);
+                  "tests/full-mmodel/addrOf.i",16);
   /*@ assert &x ≡ &x; */ ;
   __e_acsl_full_init((void *)(& __retres));
   __retres = 0;

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

-/* run.config_dev
-   COMMENT: issue with printf on CI
-   DONTRUN:
-*/
 /* run.config_ci
    COMMENT: bts #2405. Memory not initialized for code executed before main.
 */

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

-/* 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_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:20: Warning: 
+[kernel:annot:missing-spec] tests/memory/constructor.c:16: 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,"Assertion","main","\\valid(&a)",
-                      "tests/memory/local_goto.c",29);
+                      "tests/memory/local_goto.c",25);
     }
     /*@ 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,"Assertion","main","\\valid(&b)",
-                      "tests/memory/local_goto.c",40);
+                      "tests/memory/local_goto.c",36);
     }
     /*@ 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:15: Warning: 
+[kernel:typing:implicit-function-declaration] tests/memory/hidden_malloc.c:11: 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:15: Warning: 
+[kernel:annot:missing-spec] tests/memory/hidden_malloc.c:11: Warning: 
   Neither code nor specification for function realpath, generating default assigns from the prototype
-[eva:invalid-assigns] tests/memory/hidden_malloc.c:15: 
+[eva:invalid-assigns] tests/memory/hidden_malloc.c:11: 
   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:41: Warning: 
+[kernel:annot:missing-spec] tests/memory/local_goto.c:37: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype

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

@@ -6,7 +6,7 @@ MACRO: EACSL_ERR @PTEST_NAME@.e-acsl.err.log
 COMMENT: Define the following macro to "no" in a test to stop the execution of `e-acsl-gcc.sh`
 MACRO: ROOT_EACSL_GCC_ENABLE yes
 COMMENT: Default options for `e-acsl-gcc.sh`
-MACRO: ROOT_EACSL_GCC_MISC_OPTS -D -q -X
+MACRO: ROOT_EACSL_GCC_MISC_OPTS -q -X
 COMMENT: Default options for the frama-c invocation
 MACRO: ROOT_EACSL_GCC_FC_EXTRA -journal-disable -verbose 0 -kernel-warn-key *=inactive
 COMMENT: Define the following macro in a test to pass extra options to the frama-c invocation