diff --git a/src/plugins/e-acsl/env.ml b/src/plugins/e-acsl/env.ml
index 8b78fece526df9d16281be07ae343d1932dbd2a1..15c68138375a6b21fb017fd79899fc242a69bca6 100644
--- a/src/plugins/e-acsl/env.ml
+++ b/src/plugins/e-acsl/env.ml
@@ -225,7 +225,7 @@ module Logic_binding = struct
 	Error.not_yet msg
     in
     let v, e, env = 
-      new_var env ~name:logic_v.lv_name None ty (fun ?loc:_ _ _ -> []) 
+      new_var env ~name:logic_v.lv_name None ty (fun _ _ -> []) 
     in
     v,
     e, 
diff --git a/src/plugins/e-acsl/quantif.ml b/src/plugins/e-acsl/quantif.ml
index 9aafddb0b3a60dc09613c8d8f0d88abe6d1684b4..88d8dece6f4ae8aa4a97060690d41521f39900c1 100644
--- a/src/plugins/e-acsl/quantif.ml
+++ b/src/plugins/e-acsl/quantif.ml
@@ -104,15 +104,13 @@ let convert env loc is_forall p bounded_vars hyps goal =
   let var_res, res, env =
     (* variable storing the result of the quantifier *)
     let name = if is_forall then "forall" else "exists" in
-    let init_loc = loc in
     Env.new_var
       ~loc
       ~name
       env
       None
       intType
-      (fun ?loc v _ ->
-	let loc = match loc with None -> init_loc | Some l -> l in
+      (fun v _ ->
 	let lv = var v in
 	[ mkStmtOneInstr ~valid_sid:true (Set(lv, init_val, loc)) ])
   in
diff --git a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
index 3808ff631d407f5508caa8e5fc11cff9bd01dcb3..c918f394fd63150e28ecf2115d35a05eb5cee83a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-reject/oracle/quantif.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-reject/quantif.i:6:[e-acsl] warning: E-ACSL construct `unguarded \forall quantification' is not yet supported.
                   Ignoring annotation.
 tests/e-acsl-reject/quantif.i:7:[e-acsl] warning: invalid E-ACSL construct
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
index 3ea089418275acee66d3a9d6503b105bcb4130e8..b8053e41b0778e9e889904920cf9cb35ff1ce8c6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
index 3ea089418275acee66d3a9d6503b105bcb4130e8..b8053e41b0778e9e889904920cf9cb35ff1ce8c6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/addrOf.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
index 1cd9850cf6beea0fadacaf09f72714dd841e0c75..c0f108c64f2d78d54a3b12fe437fdb11099f5bc3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
index 6674bed7ec1a691b368fd487eb8f62313e786e25..cd5419a975d8e4ba8284cef1c6c2d9aae2b6146c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/arith.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
index beedd1ba456627e1d9e422a8aec3b53b1bd92052..0ec5a305f9a8b10b1f2a720b02bb212a084552fe 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/array.i:15:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
 tests/e-acsl-runtime/array.i:15:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
 tests/e-acsl-runtime/array.i:16:[e-acsl] warning: missing guard for ensuring that 1 is a valid array index
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
index 01b66b87471a8a7120e0983fc691993fd30cb2dc..411e514dfc0ebbff5140567c2ce48e4a98f5091d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/array.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/array.i:15:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
 tests/e-acsl-runtime/array.i:15:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
 tests/e-acsl-runtime/array.i:16:[e-acsl] warning: missing guard for ensuring that 1 is a valid array index
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
index c353e0286707d0e7c6dc1c020ecc51e48cfbc3e0..6a8289a4f111bc94922e839c6eeb983486f3f56f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that q is a valid memory access
 tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid pointer
 tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid memory access
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
index 857294344b686d3d93864cc9cf57c38627e3f392..1d3f840b24ccdbdb9f4cb0bf694ba90e17efdfca 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/at.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that q is a valid memory access
 tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid pointer
 tests/e-acsl-runtime/at.i:32:[e-acsl] warning: missing guard for ensuring that p+\at(*q,L1) is a valid memory access
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
index ac0733681ddd611950a1419982676cf8d400d369..c61f487b1fff63f4de11e99a208d07bf2e671249 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/cast.i:18:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
 tests/e-acsl-runtime/cast.i:19:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
 [value] Analyzing a complete application starting at main
@@ -133,7 +133,7 @@ tests/e-acsl-runtime/cast.i:18:[value] Assertion got status valid.
 ./share/e-acsl/e_acsl_gmp.h:73:[value] Function __gmpz_init_set_str: postcondition got status unknown.
 [value] Done for function __gmpz_init_set_str
 [value] computing for function __gmpz_get_ui <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/cast.i:18.
 [value] using specification for function __gmpz_get_ui
 ./share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
 [value] Done for function __gmpz_get_ui
@@ -164,7 +164,7 @@ tests/e-acsl-runtime/cast.i:19:[value] Assertion got status valid.
         Called from tests/e-acsl-runtime/cast.i:19.
 [value] Done for function __gmpz_init_set_str
 [value] computing for function __gmpz_get_ui <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/cast.i:19.
 [value] Done for function __gmpz_get_ui
 [value] computing for function __gmpz_init_set_ui <- main.
         Called from tests/e-acsl-runtime/cast.i:19.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
index 7247fbfda740243b7f385da703d8ccc6eb1afd97..0647c58df18ed773ecf19a1db595ef6b373f557b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/cast.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
index d97709a8af256bf2839ae5c618e318d6801fd3c0..1bf13626ced272159ad8e2548633d5c2731b59ac 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
index 2a42229042d8e041b54f2063aa77856dba63f115..9f9a375d9e18c3d9ff58ca0e2f6a16fef9ab86ad 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/comparison.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
index 37cae494df87cd5dea0b6cb2f160fffe45f3241d..992c71d413b2e7acf4aaffaee22b8d89c9a4ddc8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 /* Generated by Frama-C */
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
index 37cae494df87cd5dea0b6cb2f160fffe45f3241d..992c71d413b2e7acf4aaffaee22b8d89c9a4ddc8 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/empty.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 /* Generated by Frama-C */
 struct __anonstruct___mpz_struct_1 {
    int _mp_alloc ;
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
index f38f40df06aa4d3f89debde7455a5c27d4fb46c7..179384917ce48abca97d7021b984105a9b12d6c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
index f38f40df06aa4d3f89debde7455a5c27d4fb46c7..179384917ce48abca97d7021b984105a9b12d6c2 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/false.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
index bc3df0be6e8bb945f1ebf07b1a84a153a335ff17..d615435be20314fe07911a2bae0e679cec61195f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
index 18de3006c51e40dd9ce54044dac2648766b3d601..7492b1aaa7b626d588bae6094b31e83fc9a520b7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/function_contract.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle
index 42cb5d9d6f29cf6e9a03a1fafdf484f99d966660..e75a3e340307d2832687544c514bbd18ad54e42b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/global_literal_string.i:15:[e-acsl] warning: missing guard for ensuring that T+G is a valid pointer
 tests/e-acsl-runtime/global_literal_string.i:15:[e-acsl] warning: missing guard for ensuring that T+G is a valid memory access
 tests/e-acsl-runtime/global_literal_string.i:25:[e-acsl] warning: missing guard for ensuring that S+G2 is a valid pointer
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle
index 36ec0cf4071de0b685d7554065fbdfc7ac978c97..a3d168e93166b08656c172d6f64ce64f9cb194b0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/global_literal_string.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/global_literal_string.i:15:[e-acsl] warning: missing guard for ensuring that T+G is a valid pointer
 tests/e-acsl-runtime/global_literal_string.i:15:[e-acsl] warning: missing guard for ensuring that T+G is a valid memory access
 tests/e-acsl-runtime/global_literal_string.i:25:[e-acsl] warning: missing guard for ensuring that S+G2 is a valid pointer
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
index 2cf65bc3a64bd5a901289828e5fb831cf1f41ea9..bb32856c4339974aa156127c8afb5ec87ac9a698 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
index ec34cdedfc630986169d0bf1ec3fb308b86bb8c0..2447e79f76369ac726b302d484b597dba569a117 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/integer_constant.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
index e2d3fc52006b1a01c3781ae4671cecfd81287659..dca5c055316583b99a0cdf9ab8abd5020bf4994d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
index acf69c9854b4df41c5204a71670fd84d2417d281..74729ad19dd3695d713be0e7b064513b9ed88525 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/invariant.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
index 6bccb7ebeadfe58cc5c2b74057020b0f4f56b53a..4d72f88376bf8b423c888c67bd29e144e90f46f5 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
index 98e101b08bfc3f0d47fd73657872cafbf1791f09..94411ca4cbc098c2bcdf1f40f203ff00d9b23d7a 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/labeled_stmt.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
index 3ace77aa7dd5ff190b38bdbb098356547a84d0fb..58b50c35ce8a1d9733c7ac40e059ae4b10b0a10f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
index 7d0946d7f073a85395e3625dd17ee4fa77e102c1..8620b6397cf3a3a50f6af786f667162cd776f48b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/lazy.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
index ee6a9d7048d30ed70deb186d9a1778686f0bf652..4d799b0fa49e2dbb67be264e4a8422a4e7385737 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/linear_search.i:9:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
 :0:[e-acsl] warning: missing guard for ensuring that i is a valid array index
 tests/e-acsl-runtime/linear_search.i:9:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
@@ -78,7 +78,7 @@ tests/e-acsl-runtime/linear_search.i:9:[value] entering loop for the first time
         Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] using specification for function __gmpz_get_ui
 ./share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
 [value] Done for function __gmpz_get_ui
@@ -100,7 +100,7 @@ tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds
 ./share/e-acsl/e_acsl_gmp.h:133:[value] Function __gmpz_add: precondition got status valid.
 [value] Done for function __gmpz_add
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_3 < 10;
 [value] computing for function __gmpz_init_set_si <- search <- main.
@@ -170,7 +170,7 @@ tests/e-acsl-runtime/linear_search.i:9:[kernel] warning: accessing out of bounds
         Called from tests/e-acsl-runtime/linear_search.i:14.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:14.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_4 < 10;
 [value] computing for function __gmpz_init_set_si <- search <- main.
@@ -231,7 +231,7 @@ tests/e-acsl-runtime/linear_search.i:14:[kernel] warning: accessing out of bound
         Called from tests/e-acsl-runtime/linear_search.i:11.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:11.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:11:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_j_2 < 10;
 [value] computing for function __gmpz_init_set_si <- search <- main.
@@ -361,7 +361,7 @@ tests/e-acsl-runtime/linear_search.i:33:[value] Assertion got status unknown.
         Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:9:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- search <- main.
@@ -377,7 +377,7 @@ tests/e-acsl-runtime/linear_search.i:9:[value] Assertion got status unknown.
         Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] Done for function __gmpz_add
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:9.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:9:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- search <- main.
@@ -445,7 +445,7 @@ tests/e-acsl-runtime/linear_search.i:9:[value] Assertion got status unknown.
         Called from tests/e-acsl-runtime/linear_search.i:14.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:14.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:14:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- search <- main.
@@ -506,7 +506,7 @@ tests/e-acsl-runtime/linear_search.i:14:[value] Assertion got status unknown.
         Called from tests/e-acsl-runtime/linear_search.i:11.
 [value] Done for function __gmpz_clear
 [value] computing for function __gmpz_get_ui <- search <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/linear_search.i:11.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/linear_search.i:11:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- search <- main.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
index 6ccdf9a8e2f0b29fd94fbd8308ecdb0c1fd339b6..ad3330b0ef7ee7d1f80171012d23e92d82519491 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/linear_search.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/linear_search.i:9:[e-acsl] warning: missing guard for ensuring that i is a valid array index
 tests/e-acsl-runtime/linear_search.i:9:[e-acsl] warning: missing guard for ensuring that i+1 is a valid array index
 tests/e-acsl-runtime/linear_search.i:27:[e-acsl] warning: E-ACSL construct `loop invariant' is not yet supported. Ignoring annotation.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
index 99e3598a69f6793768162af334eacb0b9f9acd14..92d422382bf1e23885dff20d59e10799789fc90b 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
index cf7805d44e4b15de5e49ea68511765b8973bcf16..bb00a62fe5bea1b8638dab5a26f05b853a8b293c 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/nested_code_annot.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
index 6239f68745a7b423d890bfb2cdffd3cd24beb349..29491da4ad706970cba245c18f5257834ef95681 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
index 5802096cca9cbefdeb396715e24611e238fcb022..2658fca6e433b8f8e68e6bb5523013ebc21c52ce 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/not.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
index de5ad78e89a8c78b8d108c7cba50e41986cf1a0a..9c8af6f2ef729ec5c7f435a10376ee06b9747c41 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
index de5ad78e89a8c78b8d108c7cba50e41986cf1a0a..9c8af6f2ef729ec5c7f435a10376ee06b9747c41 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/null.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
index 128134d780f04a2bd7199770a94085cb41c62d71..4b3a8db665088b21d9d14fc1c90cb08b8056e5b3 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
index 34f928ebfe6f630d48e95e000c07618eac7a27f2..271c6dcc74380c5199bd0e27c23d2552387d7d1d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/other_constants.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
index 10c18a17587b27ab6ecd862bd86b48a3f7dce6c8..f4a385949a08f2406808cebd530f60334a3479d7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/ptr.i:13:[e-acsl] warning: missing guard for ensuring that p is a valid memory access
 :0:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
 tests/e-acsl-runtime/ptr.i:15:[e-acsl] warning: missing guard for ensuring that 2 is a valid array index
@@ -152,7 +152,7 @@ tests/e-acsl-runtime/ptr.i:16:[value] Assertion got status valid.
 ./share/e-acsl/e_acsl_gmp.h:154:[value] Function __gmpz_tdiv_q: precondition got status valid.
 [value] Done for function __gmpz_tdiv_q
 [value] computing for function __gmpz_get_ui <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/ptr.i:16.
 [value] using specification for function __gmpz_get_ui
 ./share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
 [value] Done for function __gmpz_get_ui
@@ -252,7 +252,7 @@ tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status valid.
 ./share/e-acsl/e_acsl_gmp.h:140:[value] Function __gmpz_sub: precondition got status valid.
 [value] Done for function __gmpz_sub
 [value] computing for function __gmpz_get_ui <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/ptr.i:20.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/ptr.i:20:[kernel] warning: accessing out of bounds index [0..4294967295]. assert __e_acsl_15 < 3;
 [value] computing for function __gmpz_init_set_si <- main.
@@ -376,7 +376,7 @@ tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
         Called from tests/e-acsl-runtime/ptr.i:20.
 [value] Done for function __gmpz_sub
 [value] computing for function __gmpz_get_ui <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/ptr.i:20.
 [value] Done for function __gmpz_get_ui
 tests/e-acsl-runtime/ptr.i:20:[value] Assertion got status unknown.
 [value] computing for function __gmpz_init_set_si <- main.
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
index 91d629eb6418865b09cee5fa3dce9ba4731f482d..5fdf2778a5ea668b6393d28ce3432cd5be58e64f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/ptr.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/ptr.i:13:[e-acsl] warning: missing guard for ensuring that p is a valid memory access
 :0:[e-acsl] warning: missing guard for ensuring that 0 is a valid array index
 tests/e-acsl-runtime/ptr.i:15:[e-acsl] warning: missing guard for ensuring that 2 is a valid array index
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
index 6dc877770501d8f74ca529dbcafb6ca34d8d7cec..6ca6b2a012e92baaf53c6d7449eed8f9a2dd9cd6 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
index 4bc0acc9f3d01f9f0fb2c6086ece503b967deeb0..df217319448571e4293b860005d9c5c626c1e3ee 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/quantif.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
index f633f497ec2790cd5ab715ff56f1cce58502b572..1de5c9321a9712b8e48abe130cc16f29711bc84f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring that the given integer is C-representable
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -53,7 +53,7 @@ tests/e-acsl-runtime/result.i:7:[e-acsl] warning: missing guard for ensuring tha
 ./share/e-acsl/e_acsl_gmp.h:140:[value] Function __gmpz_sub: precondition got status valid.
 [value] Done for function __gmpz_sub
 [value] computing for function __gmpz_get_ui <- f <- main.
-        Called from :0.
+        Called from tests/e-acsl-runtime/result.i:7.
 [value] using specification for function __gmpz_get_ui
 ./share/e-acsl/e_acsl_gmp.h:185:[value] Function __gmpz_get_ui: precondition got status valid.
 [value] Done for function __gmpz_get_ui
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
index e460703d57d2abd5bc33b9916007e60be60b9d3e..af413f78f12a0769c8e5c3f20bd8183b7552cde0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/result.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
index 853c8639b665a282bb206c1f8832eed187993541..d77d574a812dc16713b3866cd908d66e1116dbc7 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
index 0ec23e0a3949d99e67fb9df5673fb683f2f19b71..bb76196090c326717ffc70696fcd258e451f6e6f 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/sizeof.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
index df77f68ba1c55debc4b25181cac0cb365175748b..05587248f2557122ec7eeca65787e7719ae53e84 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
index 25b4ad471a7a60018b2f8dee03d34fd6da40e846..724c303b2ab26e2f304a0b5bf814598c5b22ec30 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/stmt_contract.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
index a94a47b107cf807092ccdd2729dab4d008d79e91..d08c66ffb215f19d5f5eb5a6848df529383ff122 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
index a94a47b107cf807092ccdd2729dab4d008d79e91..d08c66ffb215f19d5f5eb5a6848df529383ff122 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/true.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
index 9da1946327b0c465384f096c9e0da82d5a3d9512..1544848a1525894693dac07e29c223fba94b81d0 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
index c17a4126c46fd263ad9ec770e861784021f73c15..1ffa444d173011cd227b1929daaff0073618f8ba 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/typedef.res.oracle
@@ -1,9 +1,9 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
index 81d0af0d4178adfad80cfa292ccb73ee6968477a..9786fc2247ec655966e966b1a8fdc4bc758de9ff 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.1.res.oracle
@@ -1,10 +1,10 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
-[kernel] preprocessing with "gcc -C -E -I.  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc tests/e-acsl-runtime/valid.c"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I.  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc tests/e-acsl-runtime/valid.c"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
@@ -138,7 +138,7 @@ tests/e-acsl-runtime/valid.c:31:[value] Non-termination in evaluation of functio
 [value] computing for function exit <- e_acsl_assert <- main.
         Called from ./share/e-acsl/e_acsl.h:43.
 [value] using specification for function exit
-/usr/local/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+/localhome/virgile/softs/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
index 81d0af0d4178adfad80cfa292ccb73ee6968477a..9786fc2247ec655966e966b1a8fdc4bc758de9ff 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid.res.oracle
@@ -1,10 +1,10 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
-[kernel] preprocessing with "gcc -C -E -I.  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc tests/e-acsl-runtime/valid.c"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I.  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc tests/e-acsl-runtime/valid.c"
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
 [value] Initial state computed
@@ -138,7 +138,7 @@ tests/e-acsl-runtime/valid.c:31:[value] Non-termination in evaluation of functio
 [value] computing for function exit <- e_acsl_assert <- main.
         Called from ./share/e-acsl/e_acsl.h:43.
 [value] using specification for function exit
-/usr/local/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+/localhome/virgile/softs/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
index d1b941be3c03549f36622e2d8bbd6cbb3215d963..167385189c2498e9f1ec7fba0e00adde4ad7e606 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.1.res.oracle
@@ -1,10 +1,10 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
-[kernel] preprocessing with "gcc -C -E -I.  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc tests/e-acsl-runtime/valid_alias.c"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I.  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc tests/e-acsl-runtime/valid_alias.c"
 tests/e-acsl-runtime/valid_alias.c:17:[e-acsl] warning: missing guard for ensuring that b is a valid memory access
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -98,7 +98,7 @@ tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 [value] computing for function exit <- e_acsl_assert <- main.
         Called from ./share/e-acsl/e_acsl.h:43.
 [value] using specification for function exit
-/usr/local/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+/localhome/virgile/softs/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
diff --git a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
index adc3af8bbb520fc490729d60aa42345b25e40bcd..f9a8c8f5e19e6d54c03561218ee7f81824e8975d 100644
--- a/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
+++ b/src/plugins/e-acsl/tests/e-acsl-runtime/oracle/valid_alias.res.oracle
@@ -1,10 +1,10 @@
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/e_acsl.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
-[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
-[kernel] preprocessing with "gcc -C -E -I.  -I/usr/local/share/frama-c/libc -I/usr/local/share/frama-c/libc tests/e-acsl-runtime/valid_alias.c"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp_types.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl_gmp.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/e_acsl.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel_api.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_bittree.h"
+[kernel] preprocessing with "gcc -C -E -I. -I./share/e-acsl  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc ./share/e-acsl/memory_model/e_acsl_mmodel.h"
+[kernel] preprocessing with "gcc -C -E -I.  -I/localhome/virgile/softs/share/frama-c/libc -I/localhome/virgile/softs/share/frama-c/libc tests/e-acsl-runtime/valid_alias.c"
 tests/e-acsl-runtime/valid_alias.c:17:[e-acsl] warning: missing guard for ensuring that b is a valid memory access
 [value] Analyzing a complete application starting at main
 [value] Computing initial state
@@ -98,7 +98,7 @@ tests/e-acsl-runtime/valid_alias.c:16:[value] Assertion got status valid.
 [value] computing for function exit <- e_acsl_assert <- main.
         Called from ./share/e-acsl/e_acsl.h:43.
 [value] using specification for function exit
-/usr/local/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
+/localhome/virgile/softs/share/frama-c/libc/stdlib.h:180:[value] Function exit: postcondition got status invalid.
 [value] Done for function exit
 [value] Recording results for e_acsl_assert
 [value] Done for function e_acsl_assert
diff --git a/src/plugins/e-acsl/typing.ml b/src/plugins/e-acsl/typing.ml
index 070fc710374216ac3dd400cba55b75043875e297..cb578f17bea3d0ca887e20187a14ef2410a0fc29 100644
--- a/src/plugins/e-acsl/typing.ml
+++ b/src/plugins/e-acsl/typing.ml
@@ -469,7 +469,7 @@ C-representable@]";
 	  env
 	  None
 	  new_ty
-	  (fun ?loc v _ -> 
+	  (fun v _ ->
 	    [ Misc.mk_call ?loc ~result:(Cil.var v) fname [ e ] ])
       in
       e, env