diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index 4a5816b86a6ae0b38e600e4e27e653fbed159261..67745c5779d052fc5f9d8e06f730b6de85791c61 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -158,7 +158,7 @@
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: Warning: 
+[kernel:annot:missing-spec] parallel_threads.c:121: Warning: 
   Neither code nor specification for function pthread_mutex_trylock,
    generating default assigns. See -generated-spec-* options for more info
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning: 
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index 4a5816b86a6ae0b38e600e4e27e653fbed159261..67745c5779d052fc5f9d8e06f730b6de85791c61 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -158,7 +158,7 @@
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning: 
   function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: Warning: 
+[kernel:annot:missing-spec] parallel_threads.c:121: Warning: 
   Neither code nor specification for function pthread_mutex_trylock,
    generating default assigns. See -generated-spec-* options for more info
 [eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning: 
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index a7964a7178444b83d18f141968cd2436c4717eb4..aa890a27d2eaf81204b2679e9b652c55f84e7505 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
@@ -1,5 +1,5 @@
 [e-acsl] beginning translation.
 [e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: Warning: 
+[kernel:annot:missing-spec] hidden_malloc.c:11: Warning: 
   Neither code nor specification for function realpath,
    generating default assigns. See -generated-spec-* options for more info
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
index 1583f80fac71fdb1219177bc5ae8845b5b6ee423..f6c71b561f1d57dda05ff590ad68ec28d4e2725f 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
@@ -27,7 +27,7 @@
 [eva:alarm] t_fun_lib.c:15: Warning: 
   function __e_acsl_assert_register_ulong: precondition data->values == \null ||
                                                         \valid(data->values) got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: Warning: 
+[kernel:annot:missing-spec] t_fun_lib.c:19: Warning: 
   Neither code nor specification for function realpath,
    generating default assigns. See -generated-spec-* options for more info
 [eva:alarm] t_fun_lib.c:22: Warning: 
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index 24dd64d6ef9df418baf84d5a0cb7eaf49fc20eb7..ee88bbdc58569980f49e7cbca5c5c539ca06cdeb 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -154,8 +154,13 @@ let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
 
 (* Returns the function specification of [kf], with generated assigns clauses
    if they are missing. *)
-let get_funspec kf =
-  Populate_spec.populate_funspec ~do_body:true kf [`Assigns];
+let get_funspec callsite kf =
+  let loc =
+    match callsite with
+    | Kglobal -> None
+    | Kstmt stmt -> Some (Cil_datatype.Stmt.loc stmt)
+  in
+  Populate_spec.populate_funspec ?loc ~do_body:true kf [`Assigns];
   Annotations.funspec kf
 
 let analysis_target ~recursion_depth callsite kf =
@@ -166,14 +171,14 @@ let analysis_target ~recursion_depth callsite kf =
     if recursion_depth >= Parameters.RecursiveUnroll.get ()
     then begin
       Recursion.check_spec callsite kf;
-      `Spec (get_funspec kf)
+      `Spec (get_funspec callsite kf)
     end
     else
       match kf.fundec with
-      | Declaration _ -> `Spec (get_funspec kf)
+      | Declaration _ -> `Spec (get_funspec callsite kf)
       | Definition (def, _) ->
         if Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
-        then `Spec (get_funspec kf)
+        then `Spec (get_funspec callsite kf)
         else `Body (def, save_results def)
 
 let define_analysis_target ?(recursion_depth = -1) callsite kf  =
diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
index 574cd52a0069be1934bf553a6c84a1a8705518d1..04e470cae084770d27509d7d77a08100446f0b4e 100644
--- a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
+++ b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[kernel:annot:missing-spec] n5.i:9: Warning: 
+[kernel:annot:missing-spec] n5.i:21: Warning: 
   Neither code nor explicit assigns for function may_not_terminate,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function may_not_terminate <- main.
@@ -13,7 +13,7 @@
 [eva] Done for function may_not_terminate
 [eva] computing for function f <- main.
   Called from n5.i:22.
-[kernel:annot:missing-spec] n5.i:5: Warning: 
+[kernel:annot:missing-spec] n5.i:12: Warning: 
   Neither code nor explicit assigns for function never_terminates,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function never_terminates <- f <- main.
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index 210bc3fcccd9d22840a20e01bb926ca77762e03c..1ad19f92ff2ead1802feb431b5e74cefa320c970 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -10,7 +10,7 @@
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
   Called from csv.c:55.
-[kernel:annot:missing-spec] csv.c:18: Warning: 
+[kernel:annot:missing-spec] csv.c:21: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f <- main2 <- main.
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
index 9a4ba24083246bfb3bc2604909ac060a1b753a3f..8856945b2de6fdfa24223f52d7f1a3cbf28cf0bc 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -2,7 +2,7 @@
 [variadic] empty-vpar-with-ghost.i:8: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] empty-vpar-with-ghost.i:5: Warning: 
+[kernel:annot:missing-spec] empty-vpar-with-ghost.i:8: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
index 72bb0792e2b205bfdcd7b0fd685a05064d38c409..f59a25caa33749eac1627834a0653f79e5f8432d 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
@@ -1,7 +1,7 @@
 [variadic] empty-vpar.i:1: Declaration of variadic function f.
 [variadic] empty-vpar.i:8: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] empty-vpar.i:5: Warning: 
+[kernel:annot:missing-spec] empty-vpar.i:8: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
index c3a46f89849a1e640932ea178a30c7216f3df892..c47d7de999a531a3245ac5691bfe0d1a10b210a3 100644
--- a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
@@ -2,7 +2,7 @@
 [variadic] function-ptr-with-ghost.i:2: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] function-ptr-with-ghost.i:4: Warning: 
+[kernel:annot:missing-spec] function-ptr-with-ghost.i:2: Warning: 
   Neither code nor specification for function va_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function va_f
diff --git a/src/plugins/variadic/tests/declared/oracle/label.res.oracle b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
index b77faefc9d613a0106df282b2ef5979964433b20..bc7ed6281c8f4f33bfc79c027ebc4c0a10ccb3d4 100644
--- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
@@ -1,7 +1,7 @@
 [variadic] label.i:4: Declaration of variadic function f.
 [variadic] label.i:8: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] label.i:4: Warning: 
+[kernel:annot:missing-spec] label.i:8: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index 3d7544a2bcc9e2209d69c52f5b35b51b595bf064..b2c0657c754f9d9d0032b7b71b7aa9cb78166113 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -3,11 +3,11 @@
 [variadic] multi.i:9: Generic translation of call to variadic function.
 [variadic] multi.i:18: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] multi.i:15: Warning: 
+[kernel:annot:missing-spec] multi.i:18: Warning: 
   Neither code nor explicit assigns for function g,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function g
-[kernel:annot:missing-spec] multi.i:6: Warning: 
+[kernel:annot:missing-spec] multi.i:9: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
index 5c1cc2988c42d317d063f920b774f25ede003a76..73007ab0ccb49e2c3c57f1386ad2f9c1bc0b4baf 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
@@ -1,5 +1,5 @@
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] no-va-with-ghost.i:1: Warning: 
+[kernel:annot:missing-spec] no-va-with-ghost.i:4: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
index a9c2ce7a4bf39fcfecfc3b8c378e394f247c6d3c..58717791f3583a56a1d5ed9efd929a3614c3f27c 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
@@ -1,5 +1,5 @@
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] no-va.i:1: Warning: 
+[kernel:annot:missing-spec] no-va.i:4: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
index a900ef19ea712935c05706281be977d7d7275378..5fbb9d01fa79fd95978b20155226b37111d641b8 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
@@ -2,7 +2,7 @@
 [variadic] rvalues-with-ghost.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] rvalues-with-ghost.i:1: Warning: 
+[kernel:annot:missing-spec] rvalues-with-ghost.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
index 0c9e683b20cbf32d474846a6aba8292cd3f4680d..3ffbfe423b847caaab95f29168927be1e2dc59a5 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
@@ -1,7 +1,7 @@
 [variadic] rvalues.i:1: Declaration of variadic function f.
 [variadic] rvalues.i:5: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] rvalues.i:1: Warning: 
+[kernel:annot:missing-spec] rvalues.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
index 8025cbd92d5a2054d0e5d95a26a083d0e3bc7512..6e687acfe0e60bad387485f5ab3e703bfad13aa9 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -2,7 +2,7 @@
 [variadic] simple-with-ghost.i:9: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] simple-with-ghost.i:6: Warning: 
+[kernel:annot:missing-spec] simple-with-ghost.i:9: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
index 54ea4910750e8d63276caab770ef90859aa68357..8725172d792b04b485a64cc11abcbe48da6f4d9c 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -1,7 +1,7 @@
 [variadic] simple.i:1: Declaration of variadic function f.
 [variadic] simple.i:9: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] simple.i:6: Warning: 
+[kernel:annot:missing-spec] simple.i:9: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
index bd5b5017ddb73a6a15fc3c8dc6add36a05d4dbc0..ab60728bd8eb478cf20ba97268972c6bd8a80227 100644
--- a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
@@ -1,7 +1,7 @@
 [variadic] struct.i:5: Declaration of variadic function f.
 [variadic] struct.i:10: Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] struct.i:5: Warning: 
+[kernel:annot:missing-spec] struct.i:10: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
index b0f695ca4af462d87d907df540d33461fcdc16a9..a9bee4f8d44eab51b8818d92839475b15e28066f 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
@@ -3,7 +3,7 @@
 [variadic] typedefed_function-with-ghost.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] typedefed_function-with-ghost.i:2: Warning: 
+[kernel:annot:missing-spec] typedefed_function-with-ghost.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
index 5d7bccf0c5814ace1caa8cbbde5aa950981a5041..2fa079d75a88f9f318196ed66399bcd884c14431 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
@@ -2,7 +2,7 @@
 [variadic] typedefed_function.i:5: 
   Generic translation of call to variadic function.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] typedefed_function.i:2: Warning: 
+[kernel:annot:missing-spec] typedefed_function.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function f
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index db382b8430b52d2ff580dccedea27581e62e376d..74ea04f2c8f1a5bfd993c56fc4632ae881ab3cb7 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -22,7 +22,7 @@
 [eva] using specification for function execve
 [eva] using specification for function execv
 [eva] using specification for function execvp
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/unistd.h:821: Warning: 
+[kernel:annot:missing-spec] exec.c:15: Warning: 
   Neither code nor specification for function execlp_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function execlp_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index c5b43790ae077d785ff5686b38e79d1decbd6728..da138c294e84e0e06e29e3c8f708054cd5cd47d3 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -37,7 +37,7 @@
 [eva] using specification for function __va_fcntl_void
 [eva] using specification for function __va_fcntl_int
 [eva] using specification for function __va_fcntl_flock
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:129: Warning: 
+[kernel:annot:missing-spec] fcntl.c:16: Warning: 
   Neither code nor specification for function fcntl_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function fcntl_fallback_1
@@ -45,7 +45,7 @@
   function __va_fcntl_void: precondition 'cmd_has_void_arg' got status invalid.
 [eva:alarm] fcntl.c:24: Warning: 
   function __va_fcntl_flock: precondition 'cmd_as_flock_arg' got status invalid.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:129: Warning: 
+[kernel:annot:missing-spec] fcntl.c:28: Warning: 
   Neither code nor specification for function fcntl_fallback_2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function fcntl_fallback_2
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 7814251c927f4204a00d3da286851e805f873c77..fd420fb5cefb91ed5483fef95dfad77e0c1dc24f 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -21,7 +21,7 @@
 [eva] Analyzing a complete application starting at main
 [eva] using specification for function __va_open_mode_t
 [eva] using specification for function __va_open_void
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:136: Warning: 
+[kernel:annot:missing-spec] open.c:9: Warning: 
   Neither code nor specification for function open_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function open_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index c45e5c55e42286d073d36c97efe49649e0278e39..6550a1739aa7e28d8ff5842aaa332d86dc229598 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -13,7 +13,7 @@
 [variadic] open_wrong.c:13: 
   Fallback translation of call open to a call to the specialized version open_fallback_1.
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:136: Warning: 
+[kernel:annot:missing-spec] open_wrong.c:13: Warning: 
   Neither code nor specification for function open_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function open_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index f332052289ba16f68075e0f3a99506af0ed3a7d8..b7ac263ec2058e01fc0fdded3128440de3340ec9 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -20,7 +20,7 @@
   Fallback translation of call openat to a call to the specialized version openat_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] using specification for function __va_openat_mode_t
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:143: Warning: 
+[kernel:annot:missing-spec] openat.c:10: Warning: 
   Neither code nor specification for function openat_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function openat_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index a6bd5f6a94dbe6176b9d68cd0d55f644fe489a8b..96c9680ea4b2dab373d1c3ef0f45d8451e8ee2f8 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -115,7 +115,7 @@
 [eva] using specification for function printf_va_24
 [eva] using specification for function printf_va_25
 [eva] using specification for function printf_va_26
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
+[kernel:annot:missing-spec] printf.c:71: Warning: 
   Neither code nor specification for function printf_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function printf_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index d89586c515938a81c024ae110fb64ae6f28a756e..4bc1b2c08cd50b61c5c8daf12624e722166eac3b 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -28,7 +28,7 @@
   Fallback translation of call printf to a call to the specialized version printf_va_2_fallback_1.
 [eva] Analyzing a complete application starting at main
 [eva] using specification for function printf_va_1
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
+[kernel:annot:missing-spec] printf_wrong_arity.c:9: Warning: 
   Neither code nor specification for function printf_va_2_fallback_1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function printf_va_2_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 83a51e8e270e8514626c540b1318d7c95991802e..24ae14ef3edf4177b13465a291293e5c01f92332 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -348,7 +348,7 @@ int main(void)
 
 
 [eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning: 
+[kernel:annot:missing-spec] printf_wrong_types.c:18: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] using specification for function printf
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 5ad0f3b323bec4976f7e66ce4c0913b73e6e4c44..bc169708e5bc2c84ecf6d7b2538ebbd7611b688d 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -129,7 +129,7 @@
 [eva] Done for function cast_address
 [eva] computing for function garbled_mix_null <- main.
   Called from imprecise.c:148.
-[kernel:annot:missing-spec] imprecise.c:72: Warning: 
+[kernel:annot:missing-spec] imprecise.c:75: Warning: 
   Neither code nor specification for function gm_f1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function gm_f1 <- garbled_mix_null <- main.
diff --git a/tests/constant_propagation/oracle/fct_ptr.res.oracle b/tests/constant_propagation/oracle/fct_ptr.res.oracle
index 15dda274f30c93b3e53ef8efc797f8e498cda9ae..a45058cb8989af726b3b2a7bf0a2c492dc9ebfb1 100644
--- a/tests/constant_propagation/oracle/fct_ptr.res.oracle
+++ b/tests/constant_propagation/oracle/fct_ptr.res.oracle
@@ -7,7 +7,7 @@
   pf ∈ {0}
 [eva] computing for function g <- main.
   Called from fct_ptr.i:15.
-[kernel:annot:missing-spec] fct_ptr.i:11: Warning: 
+[kernel:annot:missing-spec] fct_ptr.i:8: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- g <- main.
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
index 6e978274306531d7caac1812e92ad911a9f0854e..b64143a7e576c1148033632a3cd74eb5c60b700e 100644
--- a/tests/fc_script/make-wrapper.t/run.t
+++ b/tests/fc_script/make-wrapper.t/run.t
@@ -29,7 +29,7 @@ verbose output for Make.
             main
   [eva] using specification for function large_name_to_force_line_break_in_stack_msg
   [eva] using specification for function specified
-  [kernel:annot:missing-spec] make-wrapper.c:14: Warning: 
+  [kernel:annot:missing-spec] make-wrapper.c:29: Warning: 
     Neither code nor specification for function external,
      generating default assigns. See -generated-spec-* options for more info
   [kernel] User Error: warning annot:missing-spec treated as fatal error.
diff --git a/tests/float/oracle/alarms.0.res.oracle b/tests/float/oracle/alarms.0.res.oracle
index 30155d0cc1776fa23c3cd7ff162dd3e21689e1de..6d32745d1b02c8ceb79e92661cd9edcd9f5e2e39 100644
--- a/tests/float/oracle/alarms.0.res.oracle
+++ b/tests/float/oracle/alarms.0.res.oracle
@@ -37,7 +37,7 @@
   mvd ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
-[kernel:annot:missing-spec] alarms.i:11: Warning: 
+[kernel:annot:missing-spec] alarms.i:21: Warning: 
   Neither code nor specification for function fd,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function fd <- main1 <- main.
diff --git a/tests/float/oracle/alarms.1.res.oracle b/tests/float/oracle/alarms.1.res.oracle
index 69eb74ce4a3573000101f550cb1b72f670bc6ce8..7eb8cbc512c7dd7ab1147b4af4cd2b2f96c0cb07 100644
--- a/tests/float/oracle/alarms.1.res.oracle
+++ b/tests/float/oracle/alarms.1.res.oracle
@@ -34,7 +34,7 @@
   mvd ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
-[kernel:annot:missing-spec] alarms.i:11: Warning: 
+[kernel:annot:missing-spec] alarms.i:21: Warning: 
   Neither code nor specification for function fd,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function fd <- main1 <- main.
diff --git a/tests/float/oracle/alarms.2.res.oracle b/tests/float/oracle/alarms.2.res.oracle
index c8d7e2c4d4bf3a767ade19f8640f1d4d159ffe6a..111eb5994768076770f4d454cf8a250aaab34eb6 100644
--- a/tests/float/oracle/alarms.2.res.oracle
+++ b/tests/float/oracle/alarms.2.res.oracle
@@ -31,7 +31,7 @@
   mvd ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
-[kernel:annot:missing-spec] alarms.i:11: Warning: 
+[kernel:annot:missing-spec] alarms.i:21: Warning: 
   Neither code nor specification for function fd,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function fd <- main1 <- main.
diff --git a/tests/float/oracle/contract_special_float.1.res.oracle b/tests/float/oracle/contract_special_float.1.res.oracle
index 89383cc7912f957fcf57508bbfc238374816bf7c..4e3111b5d0022849d862d4e99052c71296088d30 100644
--- a/tests/float/oracle/contract_special_float.1.res.oracle
+++ b/tests/float/oracle/contract_special_float.1.res.oracle
@@ -16,7 +16,7 @@
 [eva] Done for function fun
 [eva:alarm] contract_special_float.c:93: Warning: 
   NaN double value. assert ¬\is_NaN(v);
-[kernel:annot:missing-spec] contract_special_float.c:48: Warning: 
+[kernel:annot:missing-spec] contract_special_float.c:94: Warning: 
   Neither code nor explicit assigns for function fun_no_default,
    generating default clauses from the specification. See -generated-spec-* options for more info
 [eva] computing for function fun_no_default <- main.
diff --git a/tests/float/oracle/contract_special_float.2.res.oracle b/tests/float/oracle/contract_special_float.2.res.oracle
index 1a83bef8646e5edabade9faf9fdaae9bfd547d77..5204d3ea928f2d8fbe653da4f87da396e2b61ff1 100644
--- a/tests/float/oracle/contract_special_float.2.res.oracle
+++ b/tests/float/oracle/contract_special_float.2.res.oracle
@@ -8,7 +8,7 @@
   Called from contract_special_float.c:92.
 [eva] using specification for function fun
 [eva] Done for function fun
-[kernel:annot:missing-spec] contract_special_float.c:48: Warning: 
+[kernel:annot:missing-spec] contract_special_float.c:94: Warning: 
   Neither code nor explicit assigns for function fun_no_default,
    generating default clauses from the specification. See -generated-spec-* options for more info
 [eva] computing for function fun_no_default <- main.
diff --git a/tests/float/oracle/s.res.oracle b/tests/float/oracle/s.res.oracle
index 97c595ce7123f275f517c8d29dfab4ddc0c33347..02edc7f29a86b826e15843e165912a83db6b1ad0 100644
--- a/tests/float/oracle/s.res.oracle
+++ b/tests/float/oracle/s.res.oracle
@@ -244,7 +244,7 @@
   G19 ∈ {0}
 [eva] computing for function F4 <- main.
   Called from s.i:260.
-[kernel:annot:missing-spec] s.i:9: Warning: 
+[kernel:annot:missing-spec] s.i:230: Warning: 
   Neither code nor specification for function F1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function F1 <- F4 <- main.
@@ -253,7 +253,7 @@
 [eva] Done for function F1
 [eva:alarm] s.i:231: Warning: accessing out of bounds index. assert 0 ≤ V4;
 [eva:alarm] s.i:231: Warning: accessing out of bounds index. assert V4 < 64;
-[kernel:annot:missing-spec] s.i:10: Warning: 
+[kernel:annot:missing-spec] s.i:233: Warning: 
   Neither code nor specification for function F2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function F2 <- F4 <- main.
@@ -267,7 +267,7 @@
 [eva] Done for function F2
 [eva:alarm] s.i:242: Warning: accessing out of bounds index. assert 0 ≤ V6;
 [eva:alarm] s.i:242: Warning: accessing out of bounds index. assert V6 < 64;
-[kernel:annot:missing-spec] s.i:12: Warning: 
+[kernel:annot:missing-spec] s.i:244: Warning: 
   Neither code nor specification for function F3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function F3 <- F4 <- main.
diff --git a/tests/impact/oracle/call.0.res.oracle b/tests/impact/oracle/call.0.res.oracle
index a246c6de55ace8eb47c79ef356569dad91fea2a1..7c1a8df24dfd5588a74ff523baecdf85e80cafae 100644
--- a/tests/impact/oracle/call.0.res.oracle
+++ b/tests/impact/oracle/call.0.res.oracle
@@ -12,7 +12,7 @@
   Called from call.i:16.
 [eva] using specification for function p1
 [eva] Done for function p1
-[kernel:annot:missing-spec] call.i:12: Warning: 
+[kernel:annot:missing-spec] call.i:16: Warning: 
   Neither code nor specification for function p2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function p2 <- test <- main.
diff --git a/tests/impact/oracle/call.1.res.oracle b/tests/impact/oracle/call.1.res.oracle
index ed164092a6a5636ee93f30314702c6152c6d3dd5..22222bc2aacbc192c237b75bdfeaab4314b2524d 100644
--- a/tests/impact/oracle/call.1.res.oracle
+++ b/tests/impact/oracle/call.1.res.oracle
@@ -14,7 +14,7 @@
   Called from call.i:16.
 [eva] using specification for function p1
 [eva] Done for function p1
-[kernel:annot:missing-spec] call.i:12: Warning: 
+[kernel:annot:missing-spec] call.i:16: Warning: 
   Neither code nor specification for function p2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function p2 <- test <- call_test <- main2.
diff --git a/tests/impact/oracle/call.2.res.oracle b/tests/impact/oracle/call.2.res.oracle
index ce3a3c2a489e3974a489992a3833c95b2a0c6f31..2d7016cb262fe25ca6633576337ee357d677d885 100644
--- a/tests/impact/oracle/call.2.res.oracle
+++ b/tests/impact/oracle/call.2.res.oracle
@@ -15,7 +15,7 @@
 [eva] using specification for function p3
 [eva] call.i:41: Warning: no \from part for clause 'assigns G;'
 [eva] Done for function p3
-[kernel:annot:missing-spec] call.i:12: Warning: 
+[kernel:annot:missing-spec] call.i:45: Warning: 
   Neither code nor specification for function p2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function p2 <- test3 <- call_test3 <- main3.
diff --git a/tests/impact/oracle/undef_function.res.oracle b/tests/impact/oracle/undef_function.res.oracle
index 9661edfc6e0768a0a4563b88216ef26f8a628299..94f614cca0a6e7b07b3f7808deae7b0815ca8f4d 100644
--- a/tests/impact/oracle/undef_function.res.oracle
+++ b/tests/impact/oracle/undef_function.res.oracle
@@ -5,7 +5,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   y ∈ {0}
-[kernel:annot:missing-spec] undef_function.i:5: Warning: 
+[kernel:annot:missing-spec] undef_function.i:10: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/impact/oracle/variadic.res.oracle b/tests/impact/oracle/variadic.res.oracle
index 6b28d3e6c56f30952dd9cc79d8ab36e362ad4e16..bd08bb92439b4a8d2587a467ada84ee624dad90e 100644
--- a/tests/impact/oracle/variadic.res.oracle
+++ b/tests/impact/oracle/variadic.res.oracle
@@ -6,7 +6,7 @@
 [eva:initial-state] Values of globals at initialization
   y ∈ {0}
   z ∈ {0}
-[kernel:annot:missing-spec] variadic.i:6: Warning: 
+[kernel:annot:missing-spec] variadic.i:12: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index 1e501dfc8b4f34b5641d32ab5a0392d4a07167fe..b4d4733d9174d88e24ffc687e25e4d15ddd5ee7d 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -35,7 +35,7 @@
 [eva] Done for function strcpy
 [eva:alarm] search_h.c:32: Warning: 
   out of bounds write. assert \valid(&elementptr->count);
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/search.h:61: Warning: 
+[kernel:annot:missing-spec] search_h.c:34: Warning: 
   Neither code nor specification for function tsearch,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function tsearch <- main.
@@ -55,7 +55,7 @@
 [eva] Done for function exit
 [eva:alarm] search_h.c:40: Warning: 
   out of bounds read. assert \valid_read((struct element **)node);
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/search.h:64: Warning: 
+[kernel:annot:missing-spec] search_h.c:46: Warning: 
   Neither code nor specification for function twalk,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function twalk <- main.
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 3809bf3497a8d3961e3dd33a0ebbd6ffd79c5716..01e765f74b0657f98adf4531504ffc36c9823a12 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -11,7 +11,7 @@
 [eva:garbled-mix:write] spawn_h.c:36: 
   Assigning imprecise value to opt.
   The imprecision originates from Library function {spawn_h.c:36}
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:72: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:43: Warning: 
   Neither code nor specification for function posix_spawn_file_actions_init,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawn_file_actions_init <- main.
@@ -28,7 +28,7 @@
   Called from spawn_h.c:45.
 [eva] using specification for function exit
 [eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:55: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:47: Warning: 
   Neither code nor specification for function posix_spawn_file_actions_addclose,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawn_file_actions_addclose <- main.
@@ -43,7 +43,7 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:50.
 [eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:97: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:60: Warning: 
   Neither code nor specification for function posix_spawnattr_init,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawnattr_init <- main.
@@ -58,7 +58,7 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:62.
 [eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:99: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:63: Warning: 
   Neither code nor specification for function posix_spawnattr_setflags,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawnattr_setflags <- main.
@@ -79,7 +79,7 @@
 [eva] spawn_h.c:67: 
   function sigfillset: precondition 'valid_set' got status valid.
 [eva] Done for function sigfillset
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:113: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:68: Warning: 
   Neither code nor specification for function posix_spawnattr_setsigmask,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawnattr_setsigmask <- main.
@@ -148,7 +148,7 @@
 [eva] Done for function exit
 [eva:alarm] spawn_h.c:82: Warning: 
   out of bounds read. assert \valid_read(argv + optind);
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:116: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:82: Warning: 
   Neither code nor specification for function posix_spawnp,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawnp <- main.
@@ -163,7 +163,7 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:85.
 [eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:75: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:90: Warning: 
   Neither code nor specification for function posix_spawnattr_destroy,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawnattr_destroy <- main.
@@ -178,7 +178,7 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:92.
 [eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:69: Warning: 
+[kernel:annot:missing-spec] spawn_h.c:96: Warning: 
   Neither code nor specification for function posix_spawn_file_actions_destroy,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function posix_spawn_file_actions_destroy <- main.
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 1c624742fba9506d0120b3bcd157ed8f875d7db2..110353a5ccae0759dc0d84687ede9424937008d5 100644
--- a/tests/pdg/oracle/bts1194.res.oracle
+++ b/tests/pdg/oracle/bts1194.res.oracle
@@ -213,7 +213,7 @@
   Y ∈ {0}
 [eva] computing for function f_slice_1 <- main.
   Called from bts1194.c:32.
-[kernel:annot:missing-spec] bts1194.c:9: Warning: 
+[kernel:annot:missing-spec] bts1194.c:13: Warning: 
   Neither code nor specification for function input,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function input <- f_slice_1 <- main.
diff --git a/tests/pdg/oracle/no_body.res.oracle b/tests/pdg/oracle/no_body.res.oracle
index 3c7b07486709c52c638820f8ba9a7fb060fc7218..64da29a0597d3ac282529251b632843281f4bc38 100644
--- a/tests/pdg/oracle/no_body.res.oracle
+++ b/tests/pdg/oracle/no_body.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ {0}
-[kernel:annot:missing-spec] no_body.c:13: Warning: 
+[kernel:annot:missing-spec] no_body.c:24: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/pdg/oracle/pb_infinite_loop.2.res.oracle b/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
index a65568abcc482a114b14543cd979eb1c64d2a69d..18b970df444e4038f62bb14eb64e5ec612adf242 100644
--- a/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
+++ b/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ [--..--]
-[kernel:annot:missing-spec] pb_infinite_loop.c:43: Warning: 
+[kernel:annot:missing-spec] pb_infinite_loop.c:48: Warning: 
   Neither code nor specification for function exit,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function exit <- test_exit.
diff --git a/tests/pdg/oracle/variadic.res.oracle b/tests/pdg/oracle/variadic.res.oracle
index 5f0af4fe428f4817ad8b2b0d766957331093244c..acf750f7fc7e2883c21e4d48825ddcb1e2ec726d 100644
--- a/tests/pdg/oracle/variadic.res.oracle
+++ b/tests/pdg/oracle/variadic.res.oracle
@@ -6,7 +6,7 @@
   
 [eva] computing for function f1 <- main.
   Called from variadic.c:37.
-[kernel:annot:missing-spec] variadic.c:20: Warning: 
+[kernel:annot:missing-spec] variadic.c:23: Warning: 
   Neither code nor specification for function lib_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/scope/oracle/bts383.res.oracle b/tests/scope/oracle/bts383.res.oracle
index ba7c315cccff32e487c7a13a20cbb5e51cfebfdc..975b6c1a98e84a8e0643d1da38f45494b0abc795 100644
--- a/tests/scope/oracle/bts383.res.oracle
+++ b/tests/scope/oracle/bts383.res.oracle
@@ -38,7 +38,7 @@
   Called from bts383.c:62.
 [eva:alarm] bts383.c:35: Warning: out of bounds read. assert \valid_read(value);
 [eva:alarm] bts383.c:36: Warning: out of bounds read. assert \valid_read(value);
-[kernel:annot:missing-spec] bts383.c:32: Warning: 
+[kernel:annot:missing-spec] bts383.c:36: Warning: 
   Neither code nor specification for function out_char,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function out_char <- out_string <- main.
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 0b6a82d32ee8b5c28fd50601fba918bf8633d474..9fd462bcb24a07984cbe4e86e1297a9fd5df86cd 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -10,7 +10,7 @@
   step ∈ {0}
 [eva] computing for function lecture <- main.
   Called from bts1768.i:45.
-[kernel:annot:missing-spec] bts1768.i:15: Warning: 
+[kernel:annot:missing-spec] bts1768.i:18: Warning: 
   Neither code nor explicit assigns for function choisir,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function choisir <- lecture <- main.
diff --git a/tests/slicing/oracle/bts709.res.oracle b/tests/slicing/oracle/bts709.res.oracle
index 0a690a35fb37b5d92740f20cee83a57a6976d9ee..cad1b0604013ea4845ec40726675fb0f82bbe53d 100644
--- a/tests/slicing/oracle/bts709.res.oracle
+++ b/tests/slicing/oracle/bts709.res.oracle
@@ -9,7 +9,7 @@
   var2 IN {0}
 [eva] computing for function inputsOf_testcase_func <- main.
   Called from bts709.c:47.
-[kernel:annot:missing-spec] bts709.c:54: Warning: 
+[kernel:annot:missing-spec] bts709.c:55: Warning: 
   Neither code nor specification for function nondet_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function nondet_int <- inputsOf_testcase_func <- main.
diff --git a/tests/slicing/oracle/combine.res.oracle b/tests/slicing/oracle/combine.res.oracle
index e77debabe4d2e33c529827d1aed3170b6ca86972..2cbd14ab48a28ebb45bb2cfe59ee6c74106e51fe 100644
--- a/tests/slicing/oracle/combine.res.oracle
+++ b/tests/slicing/oracle/combine.res.oracle
@@ -121,7 +121,7 @@ int main(int x)
   
 [eva] computing for function f <- main.
   Called from combine.i:24.
-[kernel:annot:missing-spec] combine.i:8: Warning: 
+[kernel:annot:missing-spec] combine.i:17: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- f <- main.
diff --git a/tests/slicing/oracle/filter.res.oracle b/tests/slicing/oracle/filter.res.oracle
index f6036ecc4faca35c662ee49c9362c3c865719fa9..073800f4115f851f671343769145367192e6bd12 100644
--- a/tests/slicing/oracle/filter.res.oracle
+++ b/tests/slicing/oracle/filter.res.oracle
@@ -11,7 +11,7 @@
 [eva] Done for function bts806
 [eva] computing for function unspec <- main.
   Called from filter.i:43.
-[kernel:annot:missing-spec] filter.i:6: Warning: 
+[kernel:annot:missing-spec] filter.i:36: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- unspec <- main.
diff --git a/tests/slicing/oracle/loops.15.res.oracle b/tests/slicing/oracle/loops.15.res.oracle
index dd18cad9e65de7931c553886d7c8d82281763e99..726662f7e0d78991f8844cfe11f1397ebcf12813 100644
--- a/tests/slicing/oracle/loops.15.res.oracle
+++ b/tests/slicing/oracle/loops.15.res.oracle
@@ -11,7 +11,7 @@
   Z ∈ [--..--]
 [eva] loops.i:68: assertion got status valid.
 [eva] loops.i:66: starting to merge loop iterations
-[kernel:annot:missing-spec] loops.i:61: Warning: 
+[kernel:annot:missing-spec] loops.i:70: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- stop_f1.
diff --git a/tests/slicing/oracle/loops.16.res.oracle b/tests/slicing/oracle/loops.16.res.oracle
index 0cda5b17cded23521736dd27086a8128142a0dad..5d4fe926d54fd6c5ae44a737db8e2b65b8d5677b 100644
--- a/tests/slicing/oracle/loops.16.res.oracle
+++ b/tests/slicing/oracle/loops.16.res.oracle
@@ -11,7 +11,7 @@
   Z ∈ [--..--]
 [eva] loops.i:68: assertion got status valid.
 [eva] loops.i:66: starting to merge loop iterations
-[kernel:annot:missing-spec] loops.i:61: Warning: 
+[kernel:annot:missing-spec] loops.i:70: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- stop_f1.
diff --git a/tests/slicing/oracle/loops.17.res.oracle b/tests/slicing/oracle/loops.17.res.oracle
index 4f0b797442e5aee255518da1bfd2ca6fd92c4632..04a864ff382a7e169421e1efe1e4401581e57c13 100644
--- a/tests/slicing/oracle/loops.17.res.oracle
+++ b/tests/slicing/oracle/loops.17.res.oracle
@@ -11,7 +11,7 @@
   Z ∈ [--..--]
 [eva:alarm] loops.i:82: Warning: signed overflow. assert c + 10 ≤ 2147483647;
 [eva:alarm] loops.i:88: Warning: assertion got status unknown.
-[kernel:annot:missing-spec] loops.i:61: Warning: 
+[kernel:annot:missing-spec] loops.i:89: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- stop_f2.
diff --git a/tests/slicing/oracle/loops.18.res.oracle b/tests/slicing/oracle/loops.18.res.oracle
index 5ea6c7a008e2ae116df40663fcb0f2af34757530..45e2e5b619105ffb3de4db6326acc4030ba4beec 100644
--- a/tests/slicing/oracle/loops.18.res.oracle
+++ b/tests/slicing/oracle/loops.18.res.oracle
@@ -11,7 +11,7 @@
   Z ∈ [--..--]
 [eva:alarm] loops.i:82: Warning: signed overflow. assert c + 10 ≤ 2147483647;
 [eva:alarm] loops.i:88: Warning: assertion got status unknown.
-[kernel:annot:missing-spec] loops.i:61: Warning: 
+[kernel:annot:missing-spec] loops.i:89: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- stop_f2.
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index 78aabc7629ff42349f136b72a65752af5436553b..87f3dae909c810ed7d3196bc2c408d991520897d 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -10,14 +10,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -58,7 +58,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/ptr_fct.res.oracle b/tests/slicing/oracle/ptr_fct.res.oracle
index 047a99c8e945a61c3d67d735fc227b6f54e1bb2c..6c3bee4acf315ca851431a8100aabe48967a83da 100644
--- a/tests/slicing/oracle/ptr_fct.res.oracle
+++ b/tests/slicing/oracle/ptr_fct.res.oracle
@@ -8,7 +8,7 @@
   ptf ∈ {0}
 [eva] computing for function g <- h.
   Called from ptr_fct.i:23.
-[kernel:annot:missing-spec] ptr_fct.i:11: Warning: 
+[kernel:annot:missing-spec] ptr_fct.i:17: Warning: 
   Neither code nor specification for function f2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f2 <- g <- h.
diff --git a/tests/slicing/oracle/select_by_annot.0.res.oracle b/tests/slicing/oracle/select_by_annot.0.res.oracle
index cde9b9ebdde2198a18aa75377bf1f6aeed29ef40..e5de9941760551310d3e1f26e7eaa08f9c620de0 100644
--- a/tests/slicing/oracle/select_by_annot.0.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.0.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index 63bfc9b7a277633c38d91090de66323fe8b341a4..9b4b2a0f20bc28ddc7bd898f667559691ded6fe4 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index 47a035a0d9f816ae1828c875bc9c37302cda39e0..178bb3278c02a3efd47381de335569cabf167d45 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.11.res.oracle b/tests/slicing/oracle/select_by_annot.11.res.oracle
index e3871fd3d87fc33e5d60e17c0ab00a0560c912c9..a394bebd6a6ab71789f0fd759e5a1c5525b68034 100644
--- a/tests/slicing/oracle/select_by_annot.11.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.11.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index fdcad002e61f1ecb7e2d2cffd19d925d9170c366..f466ab7ac093c409ed262244406e15fcaf842df4 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.13.res.oracle b/tests/slicing/oracle/select_by_annot.13.res.oracle
index a6bee706619a94a3b5c2bfcf3e84b364161772c2..a85c8c1ecd4694880e5d4949e0d4a5fa8a51dbe7 100644
--- a/tests/slicing/oracle/select_by_annot.13.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.13.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index cd9c16cbac368d3dc7d86067e46ca10b7e6a0fee..1f98d6f3ef1062090ecc386a21c7e46ef9898341 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.2.res.oracle b/tests/slicing/oracle/select_by_annot.2.res.oracle
index a0845a156c5d74f5deb8bbb903c2421f9eae1891..7918bf2ca4e2372101e792bb98d50a7251183de8 100644
--- a/tests/slicing/oracle/select_by_annot.2.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.2.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index b8d5147e8449383517a5a34c71853c661d8975a3..988211d29e3251d1434e265cc473a9b7a675e687 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 3b7aab4fe8567889ca90168d7d5ee8ec9d412842..769500d84d8314be9f397932a125b0d26fd6adf5 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index d8ef7a2822cc0dfbdc223681d986bb8871f77d91..feed01b3a62a32da6addde70735ad325af67505c 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index db410543427d0dcc1cc73e0c03caebf11985490f..75357eb578c2958a0b6622c63eb334667610ce94 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index 77d7282f7485e1238d8b6ffab084a13256e6d2e1..1c1c5920893b474fb648f90eb55916b0c4a134da 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index 0ebb63a19965f94b66189469f1fb162343dfd50c..2cf898dc5445295a4764781ccfcf2930d69ad397 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index e80af681484c8703d1d0f79ccb1b708e08f07893..9bab22454a4ca0a5c5d1eb898c853b19ee727335 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -18,7 +18,7 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning: 
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_calls.0.res.oracle b/tests/slicing/oracle/select_calls.0.res.oracle
index 3959136da4ceaebcadb17e718d3cd053d06d4ae5..04a122b64516b8f528ae86e0cf9450df1463929f 100644
--- a/tests/slicing/oracle/select_calls.0.res.oracle
+++ b/tests/slicing/oracle/select_calls.0.res.oracle
@@ -6,7 +6,7 @@
 [eva:initial-state] Values of globals at initialization
   c ∈ [--..--]
   d ∈ [--..--]
-[kernel:annot:missing-spec] select_calls.i:8: Warning: 
+[kernel:annot:missing-spec] select_calls.i:22: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f.
@@ -16,7 +16,7 @@
 [eva] computing for function send <- f.
   Called from select_calls.i:23.
 [eva] Done for function send
-[kernel:annot:missing-spec] select_calls.i:10: Warning: 
+[kernel:annot:missing-spec] select_calls.i:24: Warning: 
   Neither code nor specification for function crypt,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function crypt <- f.
@@ -29,7 +29,7 @@
 [eva] computing for function send <- f.
   Called from select_calls.i:28.
 [eva] Done for function send
-[kernel:annot:missing-spec] select_calls.i:12: Warning: 
+[kernel:annot:missing-spec] select_calls.i:30: Warning: 
   Neither code nor specification for function uncrypt,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function uncrypt <- f.
diff --git a/tests/slicing/oracle/select_calls.1.res.oracle b/tests/slicing/oracle/select_calls.1.res.oracle
index c3a0e8506c5b87e33fa4ac27b39f32177e443d32..fd1fa6b4d75cbdc0245114504702972c1b332b30 100644
--- a/tests/slicing/oracle/select_calls.1.res.oracle
+++ b/tests/slicing/oracle/select_calls.1.res.oracle
@@ -6,7 +6,7 @@
 [eva:initial-state] Values of globals at initialization
   c ∈ [--..--]
   d ∈ [--..--]
-[kernel:annot:missing-spec] select_calls.i:6: Warning: 
+[kernel:annot:missing-spec] select_calls.i:42: Warning: 
   Neither code nor specification for function nothing,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function nothing <- g.
diff --git a/tests/slicing/oracle/select_return.0.res.oracle b/tests/slicing/oracle/select_return.0.res.oracle
index b934f52d140f92573e6a4b0e1c79c3970af1e60c..e7783ec0de811be1c04a2ee8eebde4910c4d27f6 100644
--- a/tests/slicing/oracle/select_return.0.res.oracle
+++ b/tests/slicing/oracle/select_return.0.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.1.res.oracle b/tests/slicing/oracle/select_return.1.res.oracle
index 97efb95010b49572c6062ffb9ff76e6dc6c66472..333c77abdecacf5ac181f11235928ed98ab43e6a 100644
--- a/tests/slicing/oracle/select_return.1.res.oracle
+++ b/tests/slicing/oracle/select_return.1.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.10.res.oracle b/tests/slicing/oracle/select_return.10.res.oracle
index 3d590ac884dd22d217421a5250b3d0574efb2f47..35cd5e8e21eb83704a80a654c59603fbf3c1e96d 100644
--- a/tests/slicing/oracle/select_return.10.res.oracle
+++ b/tests/slicing/oracle/select_return.10.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.11.res.oracle b/tests/slicing/oracle/select_return.11.res.oracle
index 6d50c819a40bc6581d14d59398dec2b984d54a3e..25abd7c442aa93c7ad063c8e3989c3dc0674b07e 100644
--- a/tests/slicing/oracle/select_return.11.res.oracle
+++ b/tests/slicing/oracle/select_return.11.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.12.res.oracle b/tests/slicing/oracle/select_return.12.res.oracle
index 966959e2d01dcf4327d94bb4fd867d8f8f8bec14..71a60f4e33e15d0d464f1d2f159717960f91d55d 100644
--- a/tests/slicing/oracle/select_return.12.res.oracle
+++ b/tests/slicing/oracle/select_return.12.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.13.res.oracle b/tests/slicing/oracle/select_return.13.res.oracle
index c3a9979aff7c068c856b9714877be1f8a9bbcb20..374b5e578764b4891273f5c1627004a2bfa24f5f 100644
--- a/tests/slicing/oracle/select_return.13.res.oracle
+++ b/tests/slicing/oracle/select_return.13.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.14.res.oracle b/tests/slicing/oracle/select_return.14.res.oracle
index f7fe215fa0c78dea22e1ada7321be5a870123272..490fec9745427b9e85e9e5085cf96bb2da4654d0 100644
--- a/tests/slicing/oracle/select_return.14.res.oracle
+++ b/tests/slicing/oracle/select_return.14.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.15.res.oracle b/tests/slicing/oracle/select_return.15.res.oracle
index 03b193f4a42a76130e92d1e0c344abfbea4d9235..133365cf41b2999b102ee518bc1bdeda74a6a391 100644
--- a/tests/slicing/oracle/select_return.15.res.oracle
+++ b/tests/slicing/oracle/select_return.15.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.16.res.oracle b/tests/slicing/oracle/select_return.16.res.oracle
index 9db6296f5e25a3f6d0ab62dceb8f25d954ba4889..22f1c275ac6b52a593a0c791694839a8cde3e40c 100644
--- a/tests/slicing/oracle/select_return.16.res.oracle
+++ b/tests/slicing/oracle/select_return.16.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.17.res.oracle b/tests/slicing/oracle/select_return.17.res.oracle
index e8cb8185f8f10df8591e6e56d655b4610afbfc46..c2e59c2a9427289d81812b4d653f651f21ed1a8a 100644
--- a/tests/slicing/oracle/select_return.17.res.oracle
+++ b/tests/slicing/oracle/select_return.17.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.18.res.oracle b/tests/slicing/oracle/select_return.18.res.oracle
index da8a8c63d9bb0fc49f3b85f8cd7be3aea62ebc4a..76d57c2c3535dd9adb61d6a4f2b87df92fa4dba7 100644
--- a/tests/slicing/oracle/select_return.18.res.oracle
+++ b/tests/slicing/oracle/select_return.18.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.19.res.oracle b/tests/slicing/oracle/select_return.19.res.oracle
index 14dbc9a6b57a5b3e1f97981206234c9bf0be8e25..c4c03e484a928e1f29c50395046b0a7b9501550c 100644
--- a/tests/slicing/oracle/select_return.19.res.oracle
+++ b/tests/slicing/oracle/select_return.19.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.2.res.oracle b/tests/slicing/oracle/select_return.2.res.oracle
index f5f8270f8535643169d06dddf701d5512f816d89..30dee131fa871ac96f413368a1dfedf93387e935 100644
--- a/tests/slicing/oracle/select_return.2.res.oracle
+++ b/tests/slicing/oracle/select_return.2.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.20.res.oracle b/tests/slicing/oracle/select_return.20.res.oracle
index 1d1b7c31dd1c003de86a702e2aa30e01d47e7218..21d015132d357fc1d31c4f33db37966b38664d7a 100644
--- a/tests/slicing/oracle/select_return.20.res.oracle
+++ b/tests/slicing/oracle/select_return.20.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.21.res.oracle b/tests/slicing/oracle/select_return.21.res.oracle
index e80ecd16453c91a18b427268fff08470fc5b80f6..1aedb324dc395086c2a3b9b7270efde9edee146e 100644
--- a/tests/slicing/oracle/select_return.21.res.oracle
+++ b/tests/slicing/oracle/select_return.21.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.3.res.oracle b/tests/slicing/oracle/select_return.3.res.oracle
index c992fa8daa7b0bd9bbcf6c01a6838394d065b1be..512580d248886fb56b1842c5db96c01a31b74a47 100644
--- a/tests/slicing/oracle/select_return.3.res.oracle
+++ b/tests/slicing/oracle/select_return.3.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.4.res.oracle b/tests/slicing/oracle/select_return.4.res.oracle
index dea84380dbf6320266d3ddccee608f4b43673542..0bdd4613f7806fd5e1e2fdca4118bcc864b80afa 100644
--- a/tests/slicing/oracle/select_return.4.res.oracle
+++ b/tests/slicing/oracle/select_return.4.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.5.res.oracle b/tests/slicing/oracle/select_return.5.res.oracle
index 5d06e5888064e3c7a8d8f6d40fdaeb76e44e81ae..b9b128bad9c1cbda8f696b28830c677e356c37e0 100644
--- a/tests/slicing/oracle/select_return.5.res.oracle
+++ b/tests/slicing/oracle/select_return.5.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.6.res.oracle b/tests/slicing/oracle/select_return.6.res.oracle
index 045c7b13ff6ea63b03b0cee3cabf8b425d29c411..2a25d0ccc9411c94fdac081176c72eec32317b15 100644
--- a/tests/slicing/oracle/select_return.6.res.oracle
+++ b/tests/slicing/oracle/select_return.6.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.7.res.oracle b/tests/slicing/oracle/select_return.7.res.oracle
index 80595d9f5e0ddc33267673b1da87cb65c238a1a1..4f6a431dcc0bbeebf9682b6d4a9328ea1100950b 100644
--- a/tests/slicing/oracle/select_return.7.res.oracle
+++ b/tests/slicing/oracle/select_return.7.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.8.res.oracle b/tests/slicing/oracle/select_return.8.res.oracle
index a77fac918a0cffd1dc285664d6d43804c77036e6..24560b33d23b5d67824a153a3a76014d300dc0c2 100644
--- a/tests/slicing/oracle/select_return.8.res.oracle
+++ b/tests/slicing/oracle/select_return.8.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.9.res.oracle b/tests/slicing/oracle/select_return.9.res.oracle
index beffeb890cd9c55950639b78e7e33dd0f15a9d0f..1aff238e6d11794e8df6f5bb26a74905e86e1015 100644
--- a/tests/slicing/oracle/select_return.9.res.oracle
+++ b/tests/slicing/oracle/select_return.9.res.oracle
@@ -11,14 +11,14 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning: 
+[kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
   Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning: 
+[kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning: 
+[kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.0.res.oracle b/tests/slicing/oracle/select_return_bis.0.res.oracle
index eb0059d622e8779783da09ecaaced90068b84bdf..1986a1f5e3acae8a42ccbfff0539ce6e58d672af 100644
--- a/tests/slicing/oracle/select_return_bis.0.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.0.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.1.res.oracle b/tests/slicing/oracle/select_return_bis.1.res.oracle
index a810b5fdfcf631eb56a67e3e5296cc523352c949..0b66bb17ec39fc3aef7101f8b3216057365a516f 100644
--- a/tests/slicing/oracle/select_return_bis.1.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.1.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.10.res.oracle b/tests/slicing/oracle/select_return_bis.10.res.oracle
index 64ca689f84f1885fe97d11c9d5ca9730e19d08c2..0a9c10c832f9694dc26c279a627e8db65ecfa4de 100644
--- a/tests/slicing/oracle/select_return_bis.10.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.10.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.2.res.oracle b/tests/slicing/oracle/select_return_bis.2.res.oracle
index 7850686158e8a9f0b08215169999c5ce7e781c02..77cabccd7a93c56b2af0ebead53f5ae64093c6b4 100644
--- a/tests/slicing/oracle/select_return_bis.2.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.2.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.3.res.oracle b/tests/slicing/oracle/select_return_bis.3.res.oracle
index 6d026acbd80d0d0db1232c13b51a8371ef6e625d..66d2c8939ba6cc1a5e72a993939498f530b7922c 100644
--- a/tests/slicing/oracle/select_return_bis.3.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.3.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.4.res.oracle b/tests/slicing/oracle/select_return_bis.4.res.oracle
index ce7ae154cf42007a31d32068ce415fd770b27fdb..5b6b79c6c3273b7b0181ba75668b10a753852bd7 100644
--- a/tests/slicing/oracle/select_return_bis.4.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.4.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.5.res.oracle b/tests/slicing/oracle/select_return_bis.5.res.oracle
index 42af2bc05208f6640bc25f832c101960482a944d..fb4196860a838d812844a6f7f39e0e4689f8dd63 100644
--- a/tests/slicing/oracle/select_return_bis.5.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.5.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.6.res.oracle b/tests/slicing/oracle/select_return_bis.6.res.oracle
index a709300a7c3c960240afb3b83b6cd441c9fceb73..f2a805d61ebcab10eb8ffed699629f3d5d4db38a 100644
--- a/tests/slicing/oracle/select_return_bis.6.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.6.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.7.res.oracle b/tests/slicing/oracle/select_return_bis.7.res.oracle
index 02c2717dbd5bc41c8b91d54ae103cef10aff51a7..8543cd69f0576d2e3509e25d28eeead1781fc0d6 100644
--- a/tests/slicing/oracle/select_return_bis.7.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.7.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.8.res.oracle b/tests/slicing/oracle/select_return_bis.8.res.oracle
index 3e445d2ee61d9004c2bb38673b8dcb3042cd63bc..bfe24c784f68a522a6c45c3eeb6d8f346f579a0e 100644
--- a/tests/slicing/oracle/select_return_bis.8.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.8.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.9.res.oracle b/tests/slicing/oracle/select_return_bis.9.res.oracle
index 8b0e71e1beae5867d5e70d8664a9fb82cc1e9ba4..e0d303d726da106b32b701381aaf68fd1b1eeb53 100644
--- a/tests/slicing/oracle/select_return_bis.9.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.9.res.oracle
@@ -11,7 +11,7 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning: 
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/slice_no_body.res.oracle b/tests/slicing/oracle/slice_no_body.res.oracle
index 41ec5343c9080aa8e73ec770609a0459e3e36eac..7363f61184e4ad68104452285ae3331fe8fbe153 100644
--- a/tests/slicing/oracle/slice_no_body.res.oracle
+++ b/tests/slicing/oracle/slice_no_body.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ [--..--]
-[kernel:annot:missing-spec] slice_no_body.i:9: Warning: 
+[kernel:annot:missing-spec] slice_no_body.i:21: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- h.
diff --git a/tests/slicing/oracle/unravel-flavors.0.res.oracle b/tests/slicing/oracle/unravel-flavors.0.res.oracle
index ae79b26d9eba6c5fe60e613fa7b6d51e46dc3636..9e74fb164a5a63cc7ad12e92e361720fe5b30f93 100644
--- a/tests/slicing/oracle/unravel-flavors.0.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.0.res.oracle
@@ -61,7 +61,7 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning: 
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-flavors.1.res.oracle b/tests/slicing/oracle/unravel-flavors.1.res.oracle
index 8dc524e75733120acf9050dd1bbc19ca46cbd4e0..f16981aa5190127039b88f0addd54103c6223579 100644
--- a/tests/slicing/oracle/unravel-flavors.1.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.1.res.oracle
@@ -61,7 +61,7 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning: 
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-flavors.2.res.oracle b/tests/slicing/oracle/unravel-flavors.2.res.oracle
index fd303d6963633fe30f901799fe59bbe12a1e9746..a8135ee708771ca78a171d66ef670fc1c381e99b 100644
--- a/tests/slicing/oracle/unravel-flavors.2.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.2.res.oracle
@@ -61,7 +61,7 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning: 
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-flavors.3.res.oracle b/tests/slicing/oracle/unravel-flavors.3.res.oracle
index a439aa19915f68afe48ae2604870f08e530db0b4..9a83feb26ecab703c3a44dd68bce6420826dfb93 100644
--- a/tests/slicing/oracle/unravel-flavors.3.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.3.res.oracle
@@ -61,7 +61,7 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning: 
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.0.res.oracle b/tests/slicing/oracle/unravel-point.0.res.oracle
index 8a3f0ff6239bad95fa818992cf182f29751854d9..37844d3957e7991eb0b2e6a9372e847eef0557d6 100644
--- a/tests/slicing/oracle/unravel-point.0.res.oracle
+++ b/tests/slicing/oracle/unravel-point.0.res.oracle
@@ -36,7 +36,7 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning: 
+[kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.1.res.oracle b/tests/slicing/oracle/unravel-point.1.res.oracle
index a8e1db664dd129b3cb83d33ad805eb8b3ee809a3..97703a34e75a4f48cd0ca75a4c9322a08532979e 100644
--- a/tests/slicing/oracle/unravel-point.1.res.oracle
+++ b/tests/slicing/oracle/unravel-point.1.res.oracle
@@ -36,7 +36,7 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning: 
+[kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.2.res.oracle b/tests/slicing/oracle/unravel-point.2.res.oracle
index 5a7ab392ed5ab4805ae09ac79e7d9a99db9a2e75..985169fe22a2d69004506302c2567c9ef8e124f1 100644
--- a/tests/slicing/oracle/unravel-point.2.res.oracle
+++ b/tests/slicing/oracle/unravel-point.2.res.oracle
@@ -36,7 +36,7 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning: 
+[kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.3.res.oracle b/tests/slicing/oracle/unravel-point.3.res.oracle
index bf41616d75ef10bde14b689e1ddd064222ab2d42..1a4a5c83d40bd85634809e53317f239f4869268f 100644
--- a/tests/slicing/oracle/unravel-point.3.res.oracle
+++ b/tests/slicing/oracle/unravel-point.3.res.oracle
@@ -36,7 +36,7 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning: 
+[kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.4.res.oracle b/tests/slicing/oracle/unravel-point.4.res.oracle
index 675b48c03ef063b32784a520ebcb7b115e241632..e0f32464a55fa4ff846a3de523c421e046cb6e15 100644
--- a/tests/slicing/oracle/unravel-point.4.res.oracle
+++ b/tests/slicing/oracle/unravel-point.4.res.oracle
@@ -36,7 +36,7 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning: 
+[kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf <- send1 <- main.
@@ -140,7 +140,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] unravel-point.i:22: Warning: 
+[kernel:annot:missing-spec] unravel-point.i:59: Warning: 
   Neither code nor specification for function scanf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function scanf <- main.
diff --git a/tests/slicing/oracle/unravel-variance.0.res.oracle b/tests/slicing/oracle/unravel-variance.0.res.oracle
index 513c091207216e9ae380f0886948c57eda519f49..e9aae04102cf11c25c4360d0765e4289e730a57a 100644
--- a/tests/slicing/oracle/unravel-variance.0.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.0.res.oracle
@@ -5,7 +5,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.1.res.oracle b/tests/slicing/oracle/unravel-variance.1.res.oracle
index 3c0aeed56124850440c8b4824a99113fa77f5e7e..2deb200cd14fa733adb3adaa914f5d8afa878cab 100644
--- a/tests/slicing/oracle/unravel-variance.1.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.1.res.oracle
@@ -5,7 +5,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.2.res.oracle b/tests/slicing/oracle/unravel-variance.2.res.oracle
index 5f609480148ac5fe0f9f5a6d6a32863b73f4d214..f6734df8ff538b1ce63fbaedd30545ddd52fe50e 100644
--- a/tests/slicing/oracle/unravel-variance.2.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.2.res.oracle
@@ -5,7 +5,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.3.res.oracle b/tests/slicing/oracle/unravel-variance.3.res.oracle
index 15cdd9f542007368e215c2cdd80119efb78f5f7d..dfb4b2c3bd69eec1ad6d2126ae79b54f4b7c6f85 100644
--- a/tests/slicing/oracle/unravel-variance.3.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.3.res.oracle
@@ -5,7 +5,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.4.res.oracle b/tests/slicing/oracle/unravel-variance.4.res.oracle
index 556f2cf86e09b57274d59a1aeef92d3c151b0ce1..60f4918fed83591558a3c37f5878d032927a55cc 100644
--- a/tests/slicing/oracle/unravel-variance.4.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.4.res.oracle
@@ -5,7 +5,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning: 
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle
index 9606c29d72d93c1ed25a7b4fa52b3739ace74462..8c405ab8eb899726c07780bab2c2089e2033a4cb 100644
--- a/tests/slicing/oracle/variadic.0.res.oracle
+++ b/tests/slicing/oracle/variadic.0.res.oracle
@@ -8,7 +8,7 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning: 
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.1.res.oracle b/tests/slicing/oracle/variadic.1.res.oracle
index 14aaddde6b5543582b5319c9f6f497e8d0201ae3..532c28c20668a2d58a952e25c9379c6172a0f9c2 100644
--- a/tests/slicing/oracle/variadic.1.res.oracle
+++ b/tests/slicing/oracle/variadic.1.res.oracle
@@ -8,7 +8,7 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning: 
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.2.res.oracle b/tests/slicing/oracle/variadic.2.res.oracle
index b0835a0cf758aefdceb7288ac0f385f4ba48d562..8650b514d9c9e1748034d9d4b547e795ca8d87c6 100644
--- a/tests/slicing/oracle/variadic.2.res.oracle
+++ b/tests/slicing/oracle/variadic.2.res.oracle
@@ -8,7 +8,7 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning: 
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.3.res.oracle b/tests/slicing/oracle/variadic.3.res.oracle
index aa3e4f78d17cf2f32ef1feb087b2ccaecfaa7b98..c8160927ebcc4cdb540c643528cc75c9bad3d4d2 100644
--- a/tests/slicing/oracle/variadic.3.res.oracle
+++ b/tests/slicing/oracle/variadic.3.res.oracle
@@ -8,7 +8,7 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning: 
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.4.res.oracle b/tests/slicing/oracle/variadic.4.res.oracle
index aa3e4f78d17cf2f32ef1feb087b2ccaecfaa7b98..c8160927ebcc4cdb540c643528cc75c9bad3d4d2 100644
--- a/tests/slicing/oracle/variadic.4.res.oracle
+++ b/tests/slicing/oracle/variadic.4.res.oracle
@@ -8,7 +8,7 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning: 
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index c23af3da53b7376765cc26d3c74e96b534f1ad5e..046c3ca1741d5bc1d9dcbcc01efa4b654984b5ef 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -12,7 +12,7 @@
   s1 ∈ {0}
   si[0..1] ∈ {0}
   so[0..1] ∈ {0}
-[kernel:annot:missing-spec] bts334.i:61: Warning: 
+[kernel:annot:missing-spec] bts334.i:66: Warning: 
   Neither code nor explicit assigns for function init,
    generating default clauses from the specification. See -generated-spec-* options for more info
 [eva] computing for function init <- main_init.
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 28c6ec682d7781f9212b7023ad44692eeeb1633f..2f9cd06339971284b46828e43f46b1e27d071083 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -12,7 +12,7 @@
   s1 ∈ {0}
   si[0..1] ∈ {0}
   so[0..1] ∈ {0}
-[kernel:annot:missing-spec] bts334.i:61: Warning: 
+[kernel:annot:missing-spec] bts334.i:66: Warning: 
   Neither code nor explicit assigns for function init,
    generating default clauses from the specification. See -generated-spec-* options for more info
 [eva] computing for function init <- main_init.
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index 961924551365472a8bcf0098b2755db738189a4e..d88f06cdf7383cf35330ccce0e3350561587299f 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -11,7 +11,7 @@
   s1 ∈ {0}
   si[0..1] ∈ {0}
   so[0..1] ∈ {0}
-[kernel:annot:missing-spec] bts334.i:61: Warning: 
+[kernel:annot:missing-spec] bts334.i:66: Warning: 
   Neither code nor explicit assigns for function init,
    generating default clauses from the specification. See -generated-spec-* options for more info
 [eva] computing for function init <- main_init.
diff --git a/tests/sparecode/oracle/intra.0.res.oracle b/tests/sparecode/oracle/intra.0.res.oracle
index f8b3fcdd6311cec46e955d01b47e8fdb3ff007a1..88889b31a6ebb87782521310d609136c564fb618 100644
--- a/tests/sparecode/oracle/intra.0.res.oracle
+++ b/tests/sparecode/oracle/intra.0.res.oracle
@@ -49,7 +49,7 @@
   Called from intra.i:88.
 [eva] Recording results for assign
 [eva] Done for function assign
-[kernel:annot:missing-spec] intra.i:73: Warning: 
+[kernel:annot:missing-spec] intra.i:91: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- main.
diff --git a/tests/sparecode/oracle/intra.1.res.oracle b/tests/sparecode/oracle/intra.1.res.oracle
index 4dc9557ce91aa5534d0f3b16117d192181580495..340b1dc3072098bf7696d0552e94c0fd40938195 100644
--- a/tests/sparecode/oracle/intra.1.res.oracle
+++ b/tests/sparecode/oracle/intra.1.res.oracle
@@ -48,7 +48,7 @@
   Called from intra.i:88.
 [eva] Recording results for assign
 [eva] Done for function assign
-[kernel:annot:missing-spec] intra.i:73: Warning: 
+[kernel:annot:missing-spec] intra.i:91: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- main.
diff --git a/tests/sparecode/oracle/top.1.res.oracle b/tests/sparecode/oracle/top.1.res.oracle
index f2b7c7957835d7f1b921728b116f24f56501fb95..63bea7f723a610d40fe8c49a5a6d9eebb8e81509 100644
--- a/tests/sparecode/oracle/top.1.res.oracle
+++ b/tests/sparecode/oracle/top.1.res.oracle
@@ -16,7 +16,7 @@
 [eva] Done for function main_top
 [eva] computing for function not_used_in_main_top <- main_call_top.
   Called from top.i:27.
-[kernel:annot:missing-spec] top.i:7: Warning: 
+[kernel:annot:missing-spec] top.i:10: Warning: 
   Neither code nor specification for function print,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function print <- not_used_in_main_top <- main_call_top.
diff --git a/tests/spec/oracle/assigns_void.1.res.oracle b/tests/spec/oracle/assigns_void.1.res.oracle
index c3356f555eed6716403169166315e5a00f7547d3..b978ce8605c38f7a96761359bc6ed8d186a2f4eb 100644
--- a/tests/spec/oracle/assigns_void.1.res.oracle
+++ b/tests/spec/oracle/assigns_void.1.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] assigns_void.c:7: Warning: 
+[kernel:annot:missing-spec] assigns_void.c:11: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- g.
diff --git a/tests/spec/oracle/default_assigns_bts0966.res.oracle b/tests/spec/oracle/default_assigns_bts0966.res.oracle
index 5e34aa21316d28649bf142b8cfa6524e349eb07d..728ce51af93543be68e905a91274e29a393ded31 100644
--- a/tests/spec/oracle/default_assigns_bts0966.res.oracle
+++ b/tests/spec/oracle/default_assigns_bts0966.res.oracle
@@ -2,7 +2,7 @@
 [eva] Analyzing a complete application starting at main
 [eva:initial-state] Values of globals at initialization
   auto_states[0..3] ∈ {0}
-[kernel:annot:missing-spec] default_assigns_bts0966.i:27: Warning: 
+[kernel:annot:missing-spec] default_assigns_bts0966.i:34: Warning: 
   Neither code nor explicit assigns for function copy,
    generating default clauses from the specification. See -generated-spec-* options for more info
 [eva] using specification for function copy
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index aeb161d74fb1c943a0c6498837de72dabf40ae2d..744d7aab558ef0bcada92ce5326773be1186e880 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -102,21 +102,21 @@
 [eva] using specification for function ff3
 [eva] assigns.i:68: Warning: no \from part for clause 'assigns y1, y3;'
 [eva] Done for function ff3
-[kernel:annot:missing-spec] assigns.i:71: Warning: 
+[kernel:annot:missing-spec] assigns.i:79: Warning: 
   Neither code nor specification for function ff4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function ff4 <- main2 <- main.
   Called from assigns.i:79.
 [eva] using specification for function ff4
 [eva] Done for function ff4
-[kernel:annot:missing-spec] assigns.i:73: Warning: 
+[kernel:annot:missing-spec] assigns.i:80: Warning: 
   Neither code nor specification for function ff5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function ff5 <- main2 <- main.
   Called from assigns.i:80.
 [eva] using specification for function ff5
 [eva] Done for function ff5
-[kernel:annot:missing-spec] assigns.i:62: Warning: 
+[kernel:annot:missing-spec] assigns.i:82: Warning: 
   Neither code nor specification for function ff2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function ff2 <- main2 <- main.
@@ -133,7 +133,7 @@
   pointer comparison. assert \pointer_comparable((void *)p, (void *)(&x));
 [eva] Recording results for main2
 [eva] Done for function main2
-[kernel:annot:missing-spec] assigns.i:92: Warning: 
+[kernel:annot:missing-spec] assigns.i:112: Warning: 
   Neither code nor specification for function main3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function main3 <- main.
diff --git a/tests/value/oracle/assigns_from.res.oracle b/tests/value/oracle/assigns_from.res.oracle
index d149f5e7fee3176c7bac0fb21cc75b712919aa94..002087f31ba8abd39638d82d19e0589a787a698a 100644
--- a/tests/value/oracle/assigns_from.res.oracle
+++ b/tests/value/oracle/assigns_from.res.oracle
@@ -186,7 +186,7 @@
 [eva] Done for function main9
 [eva] computing for function main10 <- main.
   Called from assigns_from.i:244.
-[kernel:annot:missing-spec] assigns_from.i:150: Warning: 
+[kernel:annot:missing-spec] assigns_from.i:152: Warning: 
   Neither code nor specification for function c,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function c <- main10 <- main.
diff --git a/tests/value/oracle/automalloc.res.oracle b/tests/value/oracle/automalloc.res.oracle
index d2d671709e27d2725f41508e714dd8e75508a4db..d7a242da6622f0d09f81179c562781b550a91ec5 100644
--- a/tests/value/oracle/automalloc.res.oracle
+++ b/tests/value/oracle/automalloc.res.oracle
@@ -4,14 +4,14 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] automalloc.i:6: Warning: 
+[kernel:annot:missing-spec] automalloc.i:14: Warning: 
   Neither code nor specification for function malloc,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function malloc <- main.
   Called from automalloc.i:14.
 [eva] using specification for function malloc
 [eva] Done for function malloc
-[kernel:annot:missing-spec] automalloc.i:7: Warning: 
+[kernel:annot:missing-spec] automalloc.i:15: Warning: 
   Neither code nor specification for function realloc,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function realloc <- main.
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 1124da3762a7e24c52124cf328fe41cf71268b53..980bd317335a3fc4d47b65acd11b2e391f2e1c3b 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -337,7 +337,7 @@
 [eva] Done for function test_assigns2
 [eva] computing for function test_small1 <- main.
   Called from behaviors1.i:649.
-[kernel:annot:missing-spec] behaviors1.i:502: Warning: 
+[kernel:annot:missing-spec] behaviors1.i:506: Warning: 
   Neither code nor explicit assigns for function f3,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f3 <- test_small1 <- main.
@@ -352,7 +352,7 @@
 [eva] Done for function test_small1
 [eva] computing for function test_small2 <- main.
   Called from behaviors1.i:650.
-[kernel:annot:missing-spec] behaviors1.i:517: Warning: 
+[kernel:annot:missing-spec] behaviors1.i:521: Warning: 
   Neither code nor explicit assigns for function f4,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f4 <- test_small2 <- main.
@@ -371,7 +371,7 @@
 [eva] Done for function test_small2
 [eva] computing for function test_small3 <- main.
   Called from behaviors1.i:651.
-[kernel:annot:missing-spec] behaviors1.i:531: Warning: 
+[kernel:annot:missing-spec] behaviors1.i:534: Warning: 
   Neither code nor explicit assigns for function f5,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f5 <- test_small3 <- main.
@@ -382,7 +382,7 @@
 [eva] Done for function test_small3
 [eva] computing for function test_small4 <- main.
   Called from behaviors1.i:652.
-[kernel:annot:missing-spec] behaviors1.i:545: Warning: 
+[kernel:annot:missing-spec] behaviors1.i:548: Warning: 
   Neither code nor explicit assigns for function f6,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f6 <- test_small4 <- main.
@@ -393,7 +393,7 @@
 [eva] Done for function test_small4
 [eva] computing for function test_small5 <- main.
   Called from behaviors1.i:653.
-[kernel:annot:missing-spec] behaviors1.i:558: Warning: 
+[kernel:annot:missing-spec] behaviors1.i:561: Warning: 
   Neither code nor explicit assigns for function f7,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f7 <- test_small5 <- main.
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 4562b5e6847a1f10ecf340b74606e3067d46b318..45acf78958063456e7bd3d636503dc555b6f337a 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -99,7 +99,7 @@
   locals {v} escaping the scope of main_old through h
 [eva] computing for function imprecise_bts_1671 <- main.
   Called from bitfield.i:165.
-[kernel:annot:missing-spec] bitfield.i:61: Warning: 
+[kernel:annot:missing-spec] bitfield.i:70: Warning: 
   Neither code nor specification for function leaf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function leaf <- imprecise_bts_1671 <- main.
diff --git a/tests/value/oracle/bts0506.0.res.oracle b/tests/value/oracle/bts0506.0.res.oracle
index f627390df62fbac9456554edead6233f2054895b..c372fd704f02d2887858b5cef8cbacb7dfdc6538 100644
--- a/tests/value/oracle/bts0506.0.res.oracle
+++ b/tests/value/oracle/bts0506.0.res.oracle
@@ -10,7 +10,7 @@
 [eva] Done for function f
 [eva] computing for function main2 <- main.
   Called from bts0506.i:49.
-[kernel:annot:missing-spec] bts0506.i:6: Warning: 
+[kernel:annot:missing-spec] bts0506.i:15: Warning: 
   Neither code nor specification for function f1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f1 <- main2 <- main.
@@ -26,7 +26,7 @@
 [eva] computing for function f1 <- main2 <- main.
   Called from bts0506.i:18.
 [eva] Done for function f1
-[kernel:annot:missing-spec] bts0506.i:7: Warning: 
+[kernel:annot:missing-spec] bts0506.i:20: Warning: 
   Neither code nor specification for function f2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f2 <- main2 <- main.
@@ -39,7 +39,7 @@
 [eva] computing for function f2 <- main2 <- main.
   Called from bts0506.i:22.
 [eva] Done for function f2
-[kernel:annot:missing-spec] bts0506.i:8: Warning: 
+[kernel:annot:missing-spec] bts0506.i:24: Warning: 
   Neither code nor specification for function f3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f3 <- main2 <- main.
@@ -49,7 +49,7 @@
 [eva] computing for function f3 <- main2 <- main.
   Called from bts0506.i:25.
 [eva] Done for function f3
-[kernel:annot:missing-spec] bts0506.i:9: Warning: 
+[kernel:annot:missing-spec] bts0506.i:27: Warning: 
   Neither code nor specification for function f4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f4 <- main2 <- main.
@@ -65,7 +65,7 @@
 [eva:alarm] bts0506.i:28: Warning: 
   non-finite float value. assert \is_finite(tmp_9);
                           (tmp_9 from f4())
-[kernel:annot:missing-spec] bts0506.i:10: Warning: 
+[kernel:annot:missing-spec] bts0506.i:30: Warning: 
   Neither code nor specification for function f5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f5 <- main2 <- main.
@@ -84,7 +84,7 @@
 [eva:alarm] bts0506.i:31: Warning: 
   non-finite double value. assert \is_finite(tmp_11);
                            (tmp_11 from f5())
-[kernel:annot:missing-spec] bts0506.i:11: Warning: 
+[kernel:annot:missing-spec] bts0506.i:33: Warning: 
   Neither code nor specification for function f6,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f6 <- main2 <- main.
@@ -97,7 +97,7 @@
 [eva] computing for function f6 <- main2 <- main.
   Called from bts0506.i:35.
 [eva] Done for function f6
-[kernel:annot:missing-spec] bts0506.i:12: Warning: 
+[kernel:annot:missing-spec] bts0506.i:37: Warning: 
   Neither code nor specification for function f7,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f7 <- main2 <- main.
diff --git a/tests/value/oracle/bts0506.1.res.oracle b/tests/value/oracle/bts0506.1.res.oracle
index 468b9221629aaff380c30367b5fe62d1f3cba505..715ab663ac3f5bd499eda86d27aeb439fd4c55f2 100644
--- a/tests/value/oracle/bts0506.1.res.oracle
+++ b/tests/value/oracle/bts0506.1.res.oracle
@@ -10,7 +10,7 @@
 [eva] Done for function f
 [eva] computing for function main2 <- main.
   Called from bts0506.i:49.
-[kernel:annot:missing-spec] bts0506.i:6: Warning: 
+[kernel:annot:missing-spec] bts0506.i:15: Warning: 
   Neither code nor specification for function f1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f1 <- main2 <- main.
@@ -26,7 +26,7 @@
 [eva] computing for function f1 <- main2 <- main.
   Called from bts0506.i:18.
 [eva] Done for function f1
-[kernel:annot:missing-spec] bts0506.i:7: Warning: 
+[kernel:annot:missing-spec] bts0506.i:20: Warning: 
   Neither code nor specification for function f2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f2 <- main2 <- main.
@@ -39,7 +39,7 @@
 [eva] computing for function f2 <- main2 <- main.
   Called from bts0506.i:22.
 [eva] Done for function f2
-[kernel:annot:missing-spec] bts0506.i:8: Warning: 
+[kernel:annot:missing-spec] bts0506.i:24: Warning: 
   Neither code nor specification for function f3,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f3 <- main2 <- main.
@@ -49,7 +49,7 @@
 [eva] computing for function f3 <- main2 <- main.
   Called from bts0506.i:25.
 [eva] Done for function f3
-[kernel:annot:missing-spec] bts0506.i:9: Warning: 
+[kernel:annot:missing-spec] bts0506.i:27: Warning: 
   Neither code nor specification for function f4,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f4 <- main2 <- main.
@@ -62,7 +62,7 @@
 [eva:alarm] bts0506.i:28: Warning: 
   non-finite float value. assert \is_finite(tmp_9);
                           (tmp_9 from f4())
-[kernel:annot:missing-spec] bts0506.i:10: Warning: 
+[kernel:annot:missing-spec] bts0506.i:30: Warning: 
   Neither code nor specification for function f5,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f5 <- main2 <- main.
@@ -78,7 +78,7 @@
 [eva] computing for function f5 <- main2 <- main.
   Called from bts0506.i:31.
 [eva] Done for function f5
-[kernel:annot:missing-spec] bts0506.i:11: Warning: 
+[kernel:annot:missing-spec] bts0506.i:33: Warning: 
   Neither code nor specification for function f6,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f6 <- main2 <- main.
@@ -91,7 +91,7 @@
 [eva] computing for function f6 <- main2 <- main.
   Called from bts0506.i:35.
 [eva] Done for function f6
-[kernel:annot:missing-spec] bts0506.i:12: Warning: 
+[kernel:annot:missing-spec] bts0506.i:37: Warning: 
   Neither code nor specification for function f7,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f7 <- main2 <- main.
diff --git a/tests/value/oracle/bug0223.0.res.oracle b/tests/value/oracle/bug0223.0.res.oracle
index 07c96593eb86d7332b68ff7008d1e91c8ed21904..2621ac4b4de53272c25dbca64d9e597927472140 100644
--- a/tests/value/oracle/bug0223.0.res.oracle
+++ b/tests/value/oracle/bug0223.0.res.oracle
@@ -7,7 +7,7 @@
   ch2 ∈ {{ NULL ; &S_ch2[0] }}
   S_ch1[0..1] ∈ [--..--]
   S_ch2[0..1] ∈ [--..--]
-[kernel:annot:missing-spec] bug0223.i:9: Warning: 
+[kernel:annot:missing-spec] bug0223.i:33: Warning: 
   Neither code nor specification for function F,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function F <- main.
@@ -19,7 +19,7 @@
 [eva] Done for function F
 [eva] computing for function h2 <- main.
   Called from bug0223.i:35.
-[kernel:annot:missing-spec] bug0223.i:11: Warning: 
+[kernel:annot:missing-spec] bug0223.i:16: Warning: 
   Neither code nor specification for function my_strcnmp,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function my_strcnmp <- h2 <- main.
diff --git a/tests/value/oracle/bug0223.1.res.oracle b/tests/value/oracle/bug0223.1.res.oracle
index 07c96593eb86d7332b68ff7008d1e91c8ed21904..2621ac4b4de53272c25dbca64d9e597927472140 100644
--- a/tests/value/oracle/bug0223.1.res.oracle
+++ b/tests/value/oracle/bug0223.1.res.oracle
@@ -7,7 +7,7 @@
   ch2 ∈ {{ NULL ; &S_ch2[0] }}
   S_ch1[0..1] ∈ [--..--]
   S_ch2[0..1] ∈ [--..--]
-[kernel:annot:missing-spec] bug0223.i:9: Warning: 
+[kernel:annot:missing-spec] bug0223.i:33: Warning: 
   Neither code nor specification for function F,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function F <- main.
@@ -19,7 +19,7 @@
 [eva] Done for function F
 [eva] computing for function h2 <- main.
   Called from bug0223.i:35.
-[kernel:annot:missing-spec] bug0223.i:11: Warning: 
+[kernel:annot:missing-spec] bug0223.i:16: Warning: 
   Neither code nor specification for function my_strcnmp,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function my_strcnmp <- h2 <- main.
diff --git a/tests/value/oracle/bug_023.res.oracle b/tests/value/oracle/bug_023.res.oracle
index c6369e819e15f9ec3e0c235c7c776b43bcde96ea..ab536314a0fea188dd3003ff411aca43274b0bf4 100644
--- a/tests/value/oracle/bug_023.res.oracle
+++ b/tests/value/oracle/bug_023.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   i ∈ {0}
   x ∈ {0}
-[kernel:annot:missing-spec] bug_023.i:4: Warning: 
+[kernel:annot:missing-spec] bug_023.i:8: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/call.res.oracle b/tests/value/oracle/call.res.oracle
index 71179e982ca3c33b180bad82a9fef8156e79e77c..c81599c1696fd0f2b15e0b6e7c4e2e99f82cdf04 100644
--- a/tests/value/oracle/call.res.oracle
+++ b/tests/value/oracle/call.res.oracle
@@ -11,7 +11,7 @@
 [eva:alarm] call.i:19: Warning: out of bounds read. assert \valid_read(v + 1);
 [eva:alarm] call.i:19: Warning: 
   pointer downcast. assert (unsigned int)*(v + 1) ≤ 2147483647;
-[kernel:annot:missing-spec] call.i:10: Warning: 
+[kernel:annot:missing-spec] call.i:19: Warning: 
   Neither code nor specification for function leaf_fun_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function leaf_fun_int <- main.
@@ -19,7 +19,7 @@
 [eva] using specification for function leaf_fun_int
 [eva] Done for function leaf_fun_int
 [eva:alarm] call.i:20: Warning: out of bounds read. assert \valid_read(v + 1);
-[kernel:annot:missing-spec] call.i:11: Warning: 
+[kernel:annot:missing-spec] call.i:20: Warning: 
   Neither code nor specification for function leaf_fun_charp,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function leaf_fun_charp <- main.
diff --git a/tests/value/oracle/copy_stdin.res.oracle b/tests/value/oracle/copy_stdin.res.oracle
index 8ad9af9913f57f1a546f3d30cce4f88ce96ec707..2535d55b3d4599d9c46d52d07d8f890d1fc21d60 100644
--- a/tests/value/oracle/copy_stdin.res.oracle
+++ b/tests/value/oracle/copy_stdin.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] copy_stdin.i:1: Warning: 
+[kernel:annot:missing-spec] copy_stdin.i:4: Warning: 
   Neither code nor specification for function leaf,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function leaf <- main.
diff --git a/tests/value/oracle/empty_struct.6.res.oracle b/tests/value/oracle/empty_struct.6.res.oracle
index 506b771445b86bf078569652c5e7bd712d00b59f..c67a99bfed4c23f7e2f3276860441cc21fd2ad5f 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -12,7 +12,7 @@
 [eva:garbled-mix:write] empty_struct.c:99: 
   Assigning imprecise value to r.
   The imprecision originates from Library function {empty_struct.c:99}
-[kernel:annot:missing-spec] empty_struct.c:96: Warning: 
+[kernel:annot:missing-spec] empty_struct.c:100: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main4.
diff --git a/tests/value/oracle/f1.res.oracle b/tests/value/oracle/f1.res.oracle
index b34af5411275132527ff82b086087bc33548de07..fef780748fe34299784b7ffd26a2c428f1efadc7 100644
--- a/tests/value/oracle/f1.res.oracle
+++ b/tests/value/oracle/f1.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] f1.i:2: Warning: 
+[kernel:annot:missing-spec] f1.i:5: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/false.res.oracle b/tests/value/oracle/false.res.oracle
index 20f02f2e4449d7a8787b9580fb5606253bc5fe79..7ea38337fafe1df2dc07348e408bb561903658a0 100644
--- a/tests/value/oracle/false.res.oracle
+++ b/tests/value/oracle/false.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] false.i:8: Warning: 
+[kernel:annot:missing-spec] false.i:18: Warning: 
   Neither code nor explicit assigns for function f,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index c466d2d8ad711cca58ae20346ddaaf4da479bc1b..88c6c5d8c6d416983f927de6f9655687531bbebf 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -44,7 +44,7 @@
   f_previous ∈ {{ &a }}
 [eva] computing for function f <- main.
   Called from from_call.i:81.
-[kernel:annot:missing-spec] from_call.i:13: Warning: 
+[kernel:annot:missing-spec] from_call.i:20: Warning: 
   Neither code nor specification for function h,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function h <- f <- main.
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index da40280de1d449c499d3cc363c11c5f972ea7a78..560d21d929a84ba7eec01b95ef43454445de32a5 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -44,7 +44,7 @@
   f_previous ∈ {{ &a }}
 [eva] computing for function f <- main.
   Called from from_call.i:81.
-[kernel:annot:missing-spec] from_call.i:13: Warning: 
+[kernel:annot:missing-spec] from_call.i:20: Warning: 
   Neither code nor specification for function h,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function h <- f <- main.
diff --git a/tests/value/oracle/ineq.res.oracle b/tests/value/oracle/ineq.res.oracle
index c2f6e5229f4e7e9610249663eb48e4323342853d..38ed36b32a0f241d5ae8041f18fc436abe50c118 100644
--- a/tests/value/oracle/ineq.res.oracle
+++ b/tests/value/oracle/ineq.res.oracle
@@ -12,7 +12,7 @@
   l ∈ {1}
   m ∈ {-1}
   n ∈ {-1}
-[kernel:annot:missing-spec] ineq.c:1: Warning: 
+[kernel:annot:missing-spec] ineq.c:6: Warning: 
   Neither code nor specification for function any_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function any_int <- main.
diff --git a/tests/value/oracle/infinite.res.oracle b/tests/value/oracle/infinite.res.oracle
index 127ab211d4dbaf3d185c6ab9f36ea73bbe7fdf8c..e43d5267297845bfc74c8316c725f4dcf71806c7 100644
--- a/tests/value/oracle/infinite.res.oracle
+++ b/tests/value/oracle/infinite.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ {0}
-[kernel:annot:missing-spec] infinite.i:1: Warning: 
+[kernel:annot:missing-spec] infinite.i:9: Warning: 
   Neither code nor specification for function pause,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function pause <- main.
diff --git a/tests/value/oracle/initialized_copy.0.res.oracle b/tests/value/oracle/initialized_copy.0.res.oracle
index 7320a7432c759f299172509931b87ffccdf76974..fec4520ecd5e94367e2890286d05e3ac8c299baa 100644
--- a/tests/value/oracle/initialized_copy.0.res.oracle
+++ b/tests/value/oracle/initialized_copy.0.res.oracle
@@ -96,7 +96,7 @@
   ==END OF DUMP==
 [eva:alarm] initialized_copy.i:151: Warning: 
   accessing uninitialized left-value. assert \initialized(&a_8);
-[kernel:annot:missing-spec] initialized_copy.i:22: Warning: 
+[kernel:annot:missing-spec] initialized_copy.i:151: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/initialized_copy.1.res.oracle b/tests/value/oracle/initialized_copy.1.res.oracle
index 878a548361d1bc08e0af09fba8a15570ca5a8dce..1677d41e75209c183f1158c9395466d3e5e020b8 100644
--- a/tests/value/oracle/initialized_copy.1.res.oracle
+++ b/tests/value/oracle/initialized_copy.1.res.oracle
@@ -88,7 +88,7 @@
   ==END OF DUMP==
 [eva:alarm] initialized_copy.i:151: Warning: 
   accessing uninitialized left-value. assert \initialized(&a_8);
-[kernel:annot:missing-spec] initialized_copy.i:22: Warning: 
+[kernel:annot:missing-spec] initialized_copy.i:151: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/input.res.oracle b/tests/value/oracle/input.res.oracle
index bbd39cd72e44541bbb912112a80814ffe9d7081f..541d5189697e32fffaa76c7d04371a3348d1d0e3 100644
--- a/tests/value/oracle/input.res.oracle
+++ b/tests/value/oracle/input.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   a ∈ {0}
   b ∈ {0}
-[kernel:annot:missing-spec] input.i:1: Warning: 
+[kernel:annot:missing-spec] input.i:7: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index a233e82216b0c479caf3ad5bc2c193ab1d9eadb3..7ccd5e0302a676eb3ee7293c6683d039208b0eca 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -29,7 +29,7 @@
   st_tab3_int_3.t[0] ∈ {30}
                .t[1] ∈ {31}
                .t[2] ∈ {32}
-[kernel:annot:missing-spec] leaf.i:3: Warning: 
+[kernel:annot:missing-spec] leaf.i:48: Warning: 
   Neither code nor specification for function f_int_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_int_int <- main.
@@ -57,35 +57,35 @@
 [eva] leaf.i:57: Frama_C_show_each_F: {5}
 [eva] leaf.i:59: Frama_C_show_each_G: {{ &g }}
 [eva] leaf.i:60: Frama_C_show_each_F: {5}
-[kernel:annot:missing-spec] leaf.i:14: Warning: 
+[kernel:annot:missing-spec] leaf.i:62: Warning: 
   Neither code nor specification for function f_star_int_cint,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_star_int_cint <- main.
   Called from leaf.i:62.
 [eva] using specification for function f_star_int_cint
 [eva] Done for function f_star_int_cint
-[kernel:annot:missing-spec] leaf.i:17: Warning: 
+[kernel:annot:missing-spec] leaf.i:64: Warning: 
   Neither code nor specification for function f_star_int_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_star_int_int <- main.
   Called from leaf.i:64.
 [eva] using specification for function f_star_int_int
 [eva] Done for function f_star_int_int
-[kernel:annot:missing-spec] leaf.i:19: Warning: 
+[kernel:annot:missing-spec] leaf.i:65: Warning: 
   Neither code nor specification for function f_tab3_int_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_tab3_int_int <- main.
   Called from leaf.i:65.
 [eva] using specification for function f_tab3_int_int
 [eva] Done for function f_tab3_int_int
-[kernel:annot:missing-spec] leaf.i:18: Warning: 
+[kernel:annot:missing-spec] leaf.i:66: Warning: 
   Neither code nor specification for function f_tab_int_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_tab_int_int <- main.
   Called from leaf.i:66.
 [eva] using specification for function f_tab_int_int
 [eva] Done for function f_tab_int_int
-[kernel:annot:missing-spec] leaf.i:38: Warning: 
+[kernel:annot:missing-spec] leaf.i:68: Warning: 
   Neither code nor specification for function f_st_star_cint_st_star_cint,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_st_star_cint_st_star_cint <- main.
@@ -95,7 +95,7 @@
 [eva:garbled-mix:write] leaf.i:68: 
   Assigning imprecise value to st_star_cint_1.
   The imprecision originates from Library function {leaf.i:68}
-[kernel:annot:missing-spec] leaf.i:39: Warning: 
+[kernel:annot:missing-spec] leaf.i:69: Warning: 
   Neither code nor specification for function f_st_star_int_st_star_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_st_star_int_st_star_int <- main.
@@ -105,28 +105,28 @@
 [eva:garbled-mix:write] leaf.i:69: 
   Assigning imprecise value to st_star_int_1.
   The imprecision originates from Library function {leaf.i:69}
-[kernel:annot:missing-spec] leaf.i:40: Warning: 
+[kernel:annot:missing-spec] leaf.i:70: Warning: 
   Neither code nor specification for function f_st_tab3_int_st_tab3_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_st_tab3_int_st_tab3_int <- main.
   Called from leaf.i:70.
 [eva] using specification for function f_st_tab3_int_st_tab3_int
 [eva] Done for function f_st_tab3_int_st_tab3_int
-[kernel:annot:missing-spec] leaf.i:42: Warning: 
+[kernel:annot:missing-spec] leaf.i:72: Warning: 
   Neither code nor specification for function f_star_st_star_cint_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_star_st_star_cint_int <- main.
   Called from leaf.i:72.
 [eva] using specification for function f_star_st_star_cint_int
 [eva] Done for function f_star_st_star_cint_int
-[kernel:annot:missing-spec] leaf.i:43: Warning: 
+[kernel:annot:missing-spec] leaf.i:73: Warning: 
   Neither code nor specification for function f_star_st_star_int_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_star_st_star_int_int <- main.
   Called from leaf.i:73.
 [eva] using specification for function f_star_st_star_int_int
 [eva] Done for function f_star_st_star_int_int
-[kernel:annot:missing-spec] leaf.i:44: Warning: 
+[kernel:annot:missing-spec] leaf.i:74: Warning: 
   Neither code nor specification for function f_star_st_tab3_int_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_star_st_tab3_int_int <- main.
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 640d666d56183fac609c60cfad8abb8e780df2a8..3f486d154c0c0f64d200520942925f611f485b1d 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -8,7 +8,7 @@
   I ∈ {0}
 [eva:alarm] leaf2.i:6: Warning: 
   pointer downcast. assert (unsigned int)(&I) ≤ 2147483647;
-[kernel:annot:missing-spec] leaf2.i:2: Warning: 
+[kernel:annot:missing-spec] leaf2.i:6: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle
index 7adfce4bcc88cb2f795ae464c9131bbe9bc6c05f..9d1932aa482eece15fb1af19cb6a2e1c98beb281 100644
--- a/tests/value/oracle/leaf_spec.0.res.oracle
+++ b/tests/value/oracle/leaf_spec.0.res.oracle
@@ -4,28 +4,28 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] leaf_spec.i:9: Warning: 
+[kernel:annot:missing-spec] leaf_spec.i:19: Warning: 
   Neither code nor specification for function f1,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f1 <- main.
   Called from leaf_spec.i:19.
 [eva] using specification for function f1
 [eva] Done for function f1
-[kernel:annot:missing-spec] leaf_spec.i:11: Warning: 
+[kernel:annot:missing-spec] leaf_spec.i:20: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
   Called from leaf_spec.i:20.
 [eva] using specification for function g
 [eva] Done for function g
-[kernel:annot:missing-spec] leaf_spec.i:13: Warning: 
+[kernel:annot:missing-spec] leaf_spec.i:21: Warning: 
   Neither code nor specification for function h,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function h <- main.
   Called from leaf_spec.i:21.
 [eva] using specification for function h
 [eva] Done for function h
-[kernel:annot:missing-spec] leaf_spec.i:15: Warning: 
+[kernel:annot:missing-spec] leaf_spec.i:22: Warning: 
   Neither code nor specification for function k,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function k <- main.
@@ -34,7 +34,7 @@
 [eva:invalid-assigns] leaf_spec.i:22: 
   Completely invalid destination for assigns clause *l. Ignoring.
 [eva] Done for function k
-[kernel:annot:missing-spec] leaf_spec.i:16: Warning: 
+[kernel:annot:missing-spec] leaf_spec.i:22: Warning: 
   Neither code nor specification for function k0,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function k0 <- main.
diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle
index 91821a7fba1fd39ca073bf9028b810a5e4762a53..f47d633f23ac1ee42e1fc1f98b1918dfbd95d7a4 100644
--- a/tests/value/oracle/leaf_spec.1.res.oracle
+++ b/tests/value/oracle/leaf_spec.1.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] leaf_spec.i:6: Warning: 
+[kernel:annot:missing-spec] leaf_spec.i:27: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main1.
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index adccceb6d27877ea5faee59cc926a814a5e263ba..3a3a113d63804454659655d9caeb4b00194905de 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -76,7 +76,7 @@
   S_1_0_S_q_ss[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
   S_0_1_S_q_ss[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
   S_1_1_S_q_ss[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
-[kernel:annot:missing-spec] library.i:5: Warning: 
+[kernel:annot:missing-spec] library.i:30: Warning: 
   Neither code nor specification for function f_int,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f_int <- main.
@@ -96,7 +96,7 @@
 [eva:alarm] library.i:33: Warning: 
   out of bounds read. assert \valid_read(*(*G));
 [eva:alarm] library.i:33: Warning: out of bounds write. assert \valid(*(*(*G)));
-[kernel:annot:missing-spec] library.i:18: Warning: 
+[kernel:annot:missing-spec] library.i:37: Warning: 
   Neither code nor specification for function gen,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function gen <- main.
diff --git a/tests/value/oracle/local_variables.res.oracle b/tests/value/oracle/local_variables.res.oracle
index 5c1c6d008b5143a5875d87dd5ced5934eb26d1eb..441104cedc724e860e17e463d445524e240a514c 100644
--- a/tests/value/oracle/local_variables.res.oracle
+++ b/tests/value/oracle/local_variables.res.oracle
@@ -13,7 +13,7 @@
   Called from local_variables.i:30.
 [eva] computing for function w <- u <- main.
   Called from local_variables.i:11.
-[kernel:annot:missing-spec] local_variables.i:4: Warning: 
+[kernel:annot:missing-spec] local_variables.i:24: Warning: 
   Neither code nor specification for function unkn,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function unkn <- w <- u <- main.
diff --git a/tests/value/oracle/noreturn.res.oracle b/tests/value/oracle/noreturn.res.oracle
index c9131db13713726af019c2c2a6eaf68db5f73aad..955ecabd5080090c944da30f12759bd3a50a0f61 100644
--- a/tests/value/oracle/noreturn.res.oracle
+++ b/tests/value/oracle/noreturn.res.oracle
@@ -16,14 +16,14 @@
   Called from noreturn.i:28.
 [eva] Recording results for warn_never_ends
 [eva] Done for function warn_never_ends
-[kernel:annot:missing-spec] noreturn.i:1: Warning: 
+[kernel:annot:missing-spec] noreturn.i:29: Warning: 
   Neither code nor specification for function stop,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function stop <- main.
   Called from noreturn.i:29.
 [eva] using specification for function stop
 [eva] Done for function stop
-[kernel:annot:missing-spec] noreturn.i:3: Warning: 
+[kernel:annot:missing-spec] noreturn.i:30: Warning: 
   Neither code nor specification for function haltme,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function haltme <- main.
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index a14d8d6d471f2d77f43d01edd894de4da5348dce..21313b3be754e82c6d4c9570db9f1ae65208e409 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -110,7 +110,7 @@
 [eva] Done for function origin_arithmetic_3
 [eva] computing for function origin_leaf_1 <- main.
   Called from origin.i:97.
-[kernel:annot:missing-spec] origin.i:30: Warning: 
+[kernel:annot:missing-spec] origin.i:38: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- origin_leaf_1 <- main.
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index a6bb3080bd7126ef1ce1c4e5ee0ed473a316487b..2d7eae48a93c4432e4dac6e0f18275b4fdc43432 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -52,7 +52,7 @@
    .t[0] ∈ {{ &y }}
    .t[1] ∈ {0}
   S_gpp[0..1] ∈ [--..--]
-[kernel:annot:missing-spec] origin.i:7: Warning: 
+[kernel:annot:missing-spec] origin.i:124: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- origin.
diff --git a/tests/value/oracle/output_leafs.res.oracle b/tests/value/oracle/output_leafs.res.oracle
index 928c51aa4ca5ab0cdca657fa2f8818aaa4001e29..a2b97d84281ca7503ade5338b8e41e9965588c11 100644
--- a/tests/value/oracle/output_leafs.res.oracle
+++ b/tests/value/oracle/output_leafs.res.oracle
@@ -43,7 +43,7 @@
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
   Called from output_leafs.i:47.
-[kernel:annot:missing-spec] output_leafs.i:36: Warning: 
+[kernel:annot:missing-spec] output_leafs.i:40: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main3 <- main.
diff --git a/tests/value/oracle/postcond_leaf.res.oracle b/tests/value/oracle/postcond_leaf.res.oracle
index d5444651d9968404388ff92d571b577bf431639d..c667f6ecd05deecab8b4a69cdd4a9433b6dd14ac 100644
--- a/tests/value/oracle/postcond_leaf.res.oracle
+++ b/tests/value/oracle/postcond_leaf.res.oracle
@@ -3,7 +3,7 @@
 [eva:initial-state] Values of globals at initialization
   i ∈ [--..--]
   j ∈ [--..--]
-[kernel:annot:missing-spec] postcond_leaf.c:22: Warning: 
+[kernel:annot:missing-spec] postcond_leaf.c:109: Warning: 
   Neither code nor explicit assigns for function f1,
    generating default clauses. See -generated-spec-* options for more info
 [eva] using specification for function f1
diff --git a/tests/value/oracle/postcondition.res.oracle b/tests/value/oracle/postcondition.res.oracle
index d1287f10cc7f44b1a5e897e92a5a7c7ecb9df523..fcfd148f70a8b458c58ae8c8daccdeb8d74be096 100644
--- a/tests/value/oracle/postcondition.res.oracle
+++ b/tests/value/oracle/postcondition.res.oracle
@@ -17,7 +17,7 @@
   Called from postcondition.i:84.
 [eva] postcondition.i:84: function get_index: precondition got status valid.
 [eva] postcondition.i:17: Frama_C_show_each_cmd: {1}
-[kernel:annot:missing-spec] postcondition.i:5: Warning: 
+[kernel:annot:missing-spec] postcondition.i:20: Warning: 
   Neither code nor explicit assigns for function u,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function u <- get_index <- main.
@@ -75,7 +75,7 @@
 [eva] computing for function u <- main.
   Called from postcondition.i:88.
 [eva] Done for function u
-[kernel:annot:missing-spec] postcondition.i:8: Warning: 
+[kernel:annot:missing-spec] postcondition.i:89: Warning: 
   Neither code nor explicit assigns for function cap,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function cap <- main.
diff --git a/tests/value/oracle/precond.res.oracle b/tests/value/oracle/precond.res.oracle
index 450e321eef9a9de3c1211abddc972010236bd63c..c7c6f73dfa1e2cc2ff7c62247190ba84d74f8899 100644
--- a/tests/value/oracle/precond.res.oracle
+++ b/tests/value/oracle/precond.res.oracle
@@ -17,7 +17,7 @@
 [eva] precond.c:32: function f: precondition 'i' got status valid.
 [eva] Recording results for f
 [eva] Done for function f
-[kernel:annot:missing-spec] precond.c:25: Warning: 
+[kernel:annot:missing-spec] precond.c:34: Warning: 
   Neither code nor explicit assigns for function g,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
@@ -27,7 +27,7 @@
 [eva] Done for function g
 [eva] computing for function aux <- main.
   Called from precond.c:36.
-[kernel:annot:missing-spec] precond.c:16: Warning: 
+[kernel:annot:missing-spec] precond.c:21: Warning: 
   Neither code nor explicit assigns for function f2,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function f2 <- aux <- main.
diff --git a/tests/value/oracle/precond2.0.res.oracle b/tests/value/oracle/precond2.0.res.oracle
index c2f33d78730097749ad37db31c749de5a2523471..2d9a1fc75369fceade9e8e1a44cbf918fc2f2935 100644
--- a/tests/value/oracle/precond2.0.res.oracle
+++ b/tests/value/oracle/precond2.0.res.oracle
@@ -19,7 +19,7 @@
   function f: precondition 'i' got status invalid.
 [eva] Recording results for f
 [eva] Done for function f
-[kernel:annot:missing-spec] precond2.c:17: Warning: 
+[kernel:annot:missing-spec] precond2.c:24: Warning: 
   Neither code nor explicit assigns for function g,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/precond2.1.res.oracle b/tests/value/oracle/precond2.1.res.oracle
index 9200a22a04a9873349f0ad16dae49ca79ef983a1..8924205852c56a0c05aa8786e6209be420a706c3 100644
--- a/tests/value/oracle/precond2.1.res.oracle
+++ b/tests/value/oracle/precond2.1.res.oracle
@@ -17,7 +17,7 @@
   function f: precondition 'i' got status invalid.
 [eva] Recording results for f
 [eva] Done for function f
-[kernel:annot:missing-spec] precond2.c:17: Warning: 
+[kernel:annot:missing-spec] precond2.c:24: Warning: 
   Neither code nor explicit assigns for function g,
    generating default clauses. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/resolve.res.oracle b/tests/value/oracle/resolve.res.oracle
index e17390ebcbc2958fdf124494f6e52878910f5925..d39a8926209e0a0824c168db6e5b23f109460d5a 100644
--- a/tests/value/oracle/resolve.res.oracle
+++ b/tests/value/oracle/resolve.res.oracle
@@ -4,7 +4,7 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[kernel:annot:missing-spec] resolve.i:3: Warning: 
+[kernel:annot:missing-spec] resolve.i:12: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
diff --git a/tests/value/oracle/semaphore.res.oracle b/tests/value/oracle/semaphore.res.oracle
index fbe8d53985fe4d5b33edd0c1a43802243305f2e2..12339ab06615a383b8a0d157b84099221cd74e6a 100644
--- a/tests/value/oracle/semaphore.res.oracle
+++ b/tests/value/oracle/semaphore.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   Sa ∈ {0}
   Sb ∈ {0}
-[kernel:annot:missing-spec] semaphore.i:6: Warning: 
+[kernel:annot:missing-spec] semaphore.i:31: Warning: 
   Neither code nor specification for function V,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function V <- g.
@@ -23,7 +23,7 @@
   Called from semaphore.i:31.
 [eva] Done for function V
 [eva] semaphore.i:28: starting to merge loop iterations
-[kernel:annot:missing-spec] semaphore.i:6: Warning: 
+[kernel:annot:missing-spec] semaphore.i:34: Warning: 
   Neither code nor specification for function P,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function P <- g.
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
index 8c0e0d9b03025094ce24f384ac44ca4617ef87d7..17a53f17bdc53a87de17f235c7ae66c7f93e46f1 100644
--- a/tests/value/oracle/strings.res.oracle
+++ b/tests/value/oracle/strings.res.oracle
@@ -40,7 +40,7 @@
   Z ∈ {0}
 [eva] computing for function string_reads <- main.
   Called from strings.i:142.
-[kernel:annot:missing-spec] strings.i:15: Warning: 
+[kernel:annot:missing-spec] strings.i:39: Warning: 
   Neither code nor specification for function u,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function u <- string_reads <- main.
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 0b65451110d25e3ca57c7fbed5ff0928e33cd0ba..65b9fa9ca02d563fb33cab39721eedcf84ad9f11 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -52,14 +52,14 @@
   assertion got status invalid (stopping propagation).
 [eva] Recording results for logic
 [eva] Done for function logic
-[kernel:annot:missing-spec] summary.i:48: Warning: 
+[kernel:annot:missing-spec] summary.i:64: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
   Called from summary.i:64.
 [eva] using specification for function f
 [eva] Done for function f
-[kernel:annot:missing-spec] summary.i:49: Warning: 
+[kernel:annot:missing-spec] summary.i:65: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index c016f68b72a8853f972d3552238d4ddd7e0ad153..78f84b5adc28a23ea09391128d089ce0c39e5da7 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -74,14 +74,14 @@
   assertion got status invalid (stopping propagation).
 [eva] Recording results for logic
 [eva] Done for function logic
-[kernel:annot:missing-spec] summary.i:48: Warning: 
+[kernel:annot:missing-spec] summary.i:64: Warning: 
   Neither code nor specification for function f,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function f <- main.
   Called from summary.i:64.
 [eva] using specification for function f
 [eva] Done for function f
-[kernel:annot:missing-spec] summary.i:49: Warning: 
+[kernel:annot:missing-spec] summary.i:65: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/switch2.res.oracle b/tests/value/oracle/switch2.res.oracle
index 031594491084e4815a1827666ba750ab6503676c..ba43fc436aed196825091b57f2c702586fce25c7 100644
--- a/tests/value/oracle/switch2.res.oracle
+++ b/tests/value/oracle/switch2.res.oracle
@@ -8,7 +8,7 @@
   Called from switch2.i:13.
 [eva] Recording results for f
 [eva] Done for function f
-[kernel:annot:missing-spec] switch2.i:7: Warning: 
+[kernel:annot:missing-spec] switch2.i:13: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index 90b425ae5cb8d3c589344375e8563f217aa685ad..860675533da474100fdec794e7fa88d4b497a4d1 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -14,7 +14,7 @@
   Called from use_spec.i:25.
 [eva] using specification for function f
 [eva] Done for function f
-[kernel:annot:missing-spec] use_spec.i:13: Warning: 
+[kernel:annot:missing-spec] use_spec.i:26: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index fb4b4c41a4fa710b822eb5dc598ed31acb91b0bb..88fa49960f6ea16fb0c275670748ff79cfa95df0 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -14,7 +14,7 @@
   Called from use_spec.i:25.
 [eva] using specification for function f
 [eva] Done for function f
-[kernel:annot:missing-spec] use_spec.i:13: Warning: 
+[kernel:annot:missing-spec] use_spec.i:26: Warning: 
   Neither code nor specification for function g,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function g <- main.
diff --git a/tests/value/oracle/volatile.res.oracle b/tests/value/oracle/volatile.res.oracle
index 5f3ac9c064e23c84d968e1fcac001d3e42260a33..d8d0bd4dec754e5d4993a0ea299b78db456953f4 100644
--- a/tests/value/oracle/volatile.res.oracle
+++ b/tests/value/oracle/volatile.res.oracle
@@ -55,7 +55,7 @@
   signed overflow. assert x_0 + y_0 ≤ 2147483647;
 [eva] Recording results for fn1
 [eva] Done for function fn1
-[kernel:annot:missing-spec] volatile.c:20: Warning: 
+[kernel:annot:missing-spec] volatile.c:40: Warning: 
   Neither code nor specification for function fn2,
    generating default assigns. See -generated-spec-* options for more info
 [eva] computing for function fn2 <- main1 <- main.