diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml
index afb73a778200b1f8d109e7b3fe4eacdbf4ff170c..ca360d48344a917435ac26d848ee6dc36f7d67a6 100644
--- a/.gitlab-ci.yml
+++ b/.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
diff --git a/nix/default.nix b/nix/default.nix
index f2c09d1e78b71d9a3494c400da5c98d1c172c1c6..9ad41577b52eececd5864c3ec0f441aa3a47e44f 100644
--- a/nix/default.nix
+++ b/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
];
diff --git a/src/plugins/e-acsl/.gitlab-ci.yml b/src/plugins/e-acsl/.gitlab-ci.yml
deleted file mode 100644
index b9be114170ac470939c88f545001c63633665d50..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/.gitlab-ci.yml
+++ /dev/null
@@ -1,54 +0,0 @@
-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
diff --git a/src/plugins/e-acsl/Makefile.in b/src/plugins/e-acsl/Makefile.in
index 3217ed21a1f00a3ef9700316b40609514416f95e..a1ba16861e7658e3d9e37cd3a3f8793e274cd010 100644
--- a/src/plugins/e-acsl/Makefile.in
+++ b/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
diff --git a/src/plugins/e-acsl/nix/default.nix b/src/plugins/e-acsl/nix/default.nix
deleted file mode 100644
index 6c41960f846c6e6ed7cc5b386ba6ae683cb0189c..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/nix/default.nix
+++ /dev/null
@@ -1,11 +0,0 @@
-# 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
deleted file mode 100644
index 112683c48489cb7773fd1c6fa8575ad00a83bd70..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/nix/frama-ci.nix
+++ /dev/null
@@ -1,15 +0,0 @@
-#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; };
- }
diff --git a/src/plugins/e-acsl/nix/frama-ci.sh b/src/plugins/e-acsl/nix/frama-ci.sh
deleted file mode 100755
index b331b057a8e8ec372a541e94d2af935a95b94f2a..0000000000000000000000000000000000000000
--- a/src/plugins/e-acsl/nix/frama-ci.sh
+++ /dev/null
@@ -1,12 +0,0 @@
-#!/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 $@
diff --git a/src/plugins/e-acsl/tests/bts/bts1398.c b/src/plugins/e-acsl/tests/bts/bts1398.c
index 9d299958c7e22790f9e6d218fc4343816a2bcebe..408d069e4ee4d948e31e4575b133f57d414df23b 100644
--- a/src/plugins/e-acsl/tests/bts/bts1398.c
+++ b/src/plugins/e-acsl/tests/bts/bts1398.c
@@ -1,4 +1,8 @@
-/* run.config
+/* 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 196be478e598103ead236a8d08d82218bc6d0d9d..a9c9e5c65e98d3f5f69ee0dbb2df47c1a5488782 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: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
diff --git a/src/plugins/e-acsl/tests/builtin/test_config_dev b/src/plugins/e-acsl/tests/builtin/test_config_dev
index 005fe8281f61d26966dd3001d194c045c994bd51..e193ace0766f9f0c9c8accc072c866be9fc86b8f 100644
--- a/src/plugins/e-acsl/tests/builtin/test_config_dev
+++ b/src/plugins/e-acsl/tests/builtin/test_config_dev
@@ -1,4 +1,4 @@
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
diff --git a/src/plugins/e-acsl/tests/format/test_config_dev b/src/plugins/e-acsl/tests/format/test_config_dev
index f8b17db695efee4a9fa9ba7fbad64c1211016eef..939fe34a86e205455ac05acd20fb607f7a5d20dc 100644
--- a/src/plugins/e-acsl/tests/format/test_config_dev
+++ b/src/plugins/e-acsl/tests/format/test_config_dev
@@ -1,4 +1,4 @@
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
diff --git a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
index c797facb0f9c1ea90d23dd783c7e380668314ce0..c3726404e6f8607953c074eb6a0ce06307dc1867 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
+++ b/src/plugins/e-acsl/tests/full-mmodel/addrOf.i
@@ -1,4 +1,8 @@
-/* run.config
+/* 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 5c90cc5a4660c6e058cb84dee9e915770f4c0347..389e8567843280c50c965a84c1a66374bfd53bef 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,(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;
diff --git a/src/plugins/e-acsl/tests/full-mmodel/test_config_dev b/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
index 47c27064d6a7cced263a412954d891030819eaf6..74d1429a832b08227c7e3790d0016f29af767e12 100644
--- a/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
+++ b/src/plugins/e-acsl/tests/full-mmodel/test_config_dev
@@ -1,4 +1,4 @@
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
diff --git a/src/plugins/e-acsl/tests/gmp-only/test_config_dev b/src/plugins/e-acsl/tests/gmp-only/test_config_dev
index 1c9f2ef180f697c6cc7dd5f278be6fe194a8d085..9133223039dd1bce1e6d18e4dcfbaa8351541ec5 100644
--- a/src/plugins/e-acsl/tests/gmp-only/test_config_dev
+++ b/src/plugins/e-acsl/tests/gmp-only/test_config_dev
@@ -1,4 +1,4 @@
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
diff --git a/src/plugins/e-acsl/tests/memory/constructor.c b/src/plugins/e-acsl/tests/memory/constructor.c
index 6600992870e3d1809cb467a56479b9060ad9bfdc..32e630a32788679eb2571379587ebad512b111fe 100644
--- a/src/plugins/e-acsl/tests/memory/constructor.c
+++ b/src/plugins/e-acsl/tests/memory/constructor.c
@@ -1,4 +1,8 @@
-/* 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
+}
diff --git a/src/plugins/e-acsl/tests/memory/hidden_malloc.c b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
index a33c036ea74cbcf53c637f434e6cb2af885841de..3900421de1c7da2824fd45627ebcfb7fc1c453b8 100644
--- a/src/plugins/e-acsl/tests/memory/hidden_malloc.c
+++ b/src/plugins/e-acsl/tests/memory/hidden_malloc.c
@@ -1,4 +1,8 @@
-/* run.config
+/* 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 2defb67029366fd074c7708a3103dc7431a9947e..397f145cc16cd6eb5cdcdce28a0e0a103f03921a 100644
--- a/src/plugins/e-acsl/tests/memory/local_goto.c
+++ b/src/plugins/e-acsl/tests/memory/local_goto.c
@@ -1,4 +1,8 @@
-/* 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
*/
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 850186d110a852c7deff7b8cb2ed345dd9a3abe3..c660eb1a183b3770435f15404e2c620d30c13493 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: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
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 a1d7f65f0b185f763dc6b6438d4acb0cd3d18a80..f75569727cb0a83584c21e41030834e5f2eac8c0 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,(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);
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 cecec801d917584a0d8bcf334b1f14c947fb38a8..7bb9d547bffed4a48e6a08788bb7ec3e12e802c2 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: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.
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 142c3f2be0104e92d2deba3a08cd8d2a0b4b1f10..74588e72426d633d658a62543d219708afb71011 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: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
diff --git a/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle b/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a076fcedfdb07a6e5dbd7554e48c110d6e0b1c0e
--- /dev/null
+++ b/src/plugins/e-acsl/tests/memory/oracle_dev/ghost_parameters.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/memory/ghost_parameters.i (no preprocessing)
diff --git a/src/plugins/e-acsl/tests/temporal/test_config_dev b/src/plugins/e-acsl/tests/temporal/test_config_dev
index 3e4efa8f66f6c143ffd1a88b850d8f87a29c7314..e30c0a77d618b283e8138911da31d45e85ad1d46 100644
--- a/src/plugins/e-acsl/tests/temporal/test_config_dev
+++ b/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
diff --git a/src/plugins/e-acsl/tests/test_config_dev.in b/src/plugins/e-acsl/tests/test_config_dev.in
index 3285052cca07ca1f06e1e0964335a5ebf139c797..131e1da19b5d9185668fdab2a4f4b9ac9acfae2c 100644
--- a/src/plugins/e-acsl/tests/test_config_dev.in
+++ b/src/plugins/e-acsl/tests/test_config_dev.in
@@ -1,4 +1,4 @@
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