diff --git a/nix/default.nix b/nix/default.nix
index c8e4966f3f26110ec5cfa96fd6629275292a6864..0121a1d19f4c87a04e15fa7da4876daede52c45c 100644
--- a/nix/default.nix
+++ b/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" ]; } ) ++
diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
index 408d069e4ee4d948e31e4575b133f57d414df23b..9dbd83d269e0b636508a91221f8dfbb292c62a9f 100644
--- a/src/plugins/e-acsl/tests/bts/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with printf on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: variadic function call
*/
diff --git a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
index a9c9e5c65e98d3f5f69ee0dbb2df47c1a5488782..196be478e598103ead236a8d08d82218bc6d0d9d 100644
--- a/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
+++ b/src/plugins/e-acsl/tests/bts/oracle_ci/bts1398.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
index c3726404e6f8607953c074eb6a0ce06307dc1867..281703719852d97b3b865510c8ea8d67c049a045 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
+++ b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with function pointers on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: addrOf
*/
diff --git a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c b/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
index ca3a611c9bd240c6dba0d59cbea332b76cbe4f44..e7da245320f44ca617784993e0bf842400a92cff 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/oracle_ci/gen_addrOf.c
+++ b/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;
diff --git a/src/plugins/e-acsl/tests/memory/constructor.c b/src/plugins/e-acsl/tests/memory/constructor.c
index 32e630a32788679eb2571379587ebad512b111fe..8530264c83f3dff89a26d3dc0beaa254942795a8 100644
--- a/src/plugins/e-acsl/tests/memory/constructor.c
+++ b/src/plugins/e-acsl/tests/memory/constructor.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue with printf on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: bts #2405. Memory not initialized for code executed before main.
*/
diff --git a/src/plugins/e-acsl/tests/memory/hidden_malloc.c b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
index 3900421de1c7da2824fd45627ebcfb7fc1c453b8..7d220a59517efd7bd62e13946568cae3d0b613fd 100644
--- a/src/plugins/e-acsl/tests/memory/hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
@@ -1,7 +1,3 @@
-/* run.config_dev
- COMMENT: issue on CI
- DONTRUN:
-*/
/* run.config_ci
COMMENT: Malloc executed by a library function
*/
diff --git a/src/plugins/e-acsl/tests/memory/local_goto.c b/src/plugins/e-acsl/tests/memory/local_goto.c
index 397f145cc16cd6eb5cdcdce28a0e0a103f03921a..a5448bf07063eeaa318549d0c51931ddf7357998 100644
--- a/src/plugins/e-acsl/tests/memory/local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/local_goto.c
@@ -1,7 +1,3 @@
-/* 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
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
index c660eb1a183b3770435f15404e2c620d30c13493..850186d110a852c7deff7b8cb2ed345dd9a3abe3 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/constructor.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c b/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
index 707853628e0809429f024754938dc89d741936cc..2cf1cc44c0cd0dd389bce183c8fa9c4fdb3ef873 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/gen_local_goto.c
+++ b/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);
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
index 7bb9d547bffed4a48e6a08788bb7ec3e12e802c2..cecec801d917584a0d8bcf334b1f14c947fb38a8 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/hidden_malloc.res.oracle
@@ -1,9 +1,9 @@
-[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.
diff --git a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
index 74588e72426d633d658a62543d219708afb71011..142c3f2be0104e92d2deba3a08cd8d2a0b4b1f10 100644
--- a/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle_ci/local_goto.res.oracle
@@ -1,4 +1,4 @@
[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
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index 8a01dabc2fff701b297a64e5ca32911b5fc81414..b425a92ef845aa9c2b780656c0a153c19f48ee3b 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/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