diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
index 46379ed00ac854e9956120efd17acd2f8156cabf..c46055dd4a58a205e31956206de4d70292a59bbd 100644
--- a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
+++ b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
@@ -4,18 +4,18 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   nondet ∈ [--..--]
-[eva] computing for function may_not_terminate <- main.
-  Called from n5.i:21.
 [kernel] n5.i:21: Warning: 
   No code nor implicit assigns clause for function may_not_terminate, generating default assigns from the prototype
+[eva] computing for function may_not_terminate <- main.
+  Called from n5.i:21.
 [eva] using specification for function may_not_terminate
 [eva] Done for function may_not_terminate
 [eva] computing for function f <- main.
   Called from n5.i:22.
-[eva] computing for function never_terminates <- f <- main.
-  Called from n5.i:12.
 [kernel] n5.i:12: Warning: 
   No code nor implicit assigns clause for function never_terminates, generating default assigns from the prototype
+[eva] computing for function never_terminates <- f <- main.
+  Called from n5.i:12.
 [eva] using specification for function never_terminates
 [eva] Done for function never_terminates
 [eva] Recording results for f
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index b476eeb4126e85ea99a46c608c380c756defad9b..5647ffdfd1d4c01f4910a6efcdfc05e2ae610bd3 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -10,10 +10,10 @@
 [eva] Done for function main1
 [eva] computing for function main2 <- main.
   Called from csv.c:55.
-[eva] computing for function f <- main2 <- main.
-  Called from csv.c:21.
 [kernel] csv.c:21: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[eva] computing for function f <- main2 <- main.
+  Called from csv.c:21.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] computing for function f <- main2 <- main.
diff --git a/src/plugins/value/engine/compute_functions.ml b/src/plugins/value/engine/compute_functions.ml
index 32ebe6a24ae98bb0848f11475bbd4ea4f2ba3bd0..701376e8202398681776dcd6f7870fa40891b412 100644
--- a/src/plugins/value/engine/compute_functions.ml
+++ b/src/plugins/value/engine/compute_functions.ml
@@ -177,11 +177,6 @@ module Make (Abstract: Abstractions.Eva) = struct
     let global = match call_kinstr with Kglobal -> true | _ -> false in
     let pp = not global && Parameters.ValShowProgress.get () in
     let call_stack = Eva_utils.call_stack () in
-    if pp then
-      Self.feedback
-        "@[computing for function %a.@\nCalled from %a.@]"
-        Value_types.Callstack.pretty_short call_stack
-        Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc call_kinstr);
     let use_spec =
       match recursion with
       | Some { depth } when depth >= Parameters.RecursiveUnroll.get () ->
@@ -194,6 +189,11 @@ module Make (Abstract: Abstractions.Eva) = struct
           then `Spec (Annotations.funspec kf)
           else `Def def
     in
+    if pp then
+      Self.feedback
+        "@[computing for function %a.@\nCalled from %a.@]"
+        Value_types.Callstack.pretty_short call_stack
+        Cil_datatype.Location.pretty (Cil_datatype.Kinstr.loc call_kinstr);
     let cvalue_state = Abstract.Dom.get_cvalue_or_top state in
     let resulting_states, cacheable = match use_spec with
       | `Spec spec ->
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index b61a66f867893673b1b2dc405b68d0dd3d493381..c5d23a2cbd6870325adf211e6bde1b09c99cfab4 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -129,10 +129,10 @@
 [eva] Done for function cast_address
 [eva] computing for function garbled_mix_null <- main.
   Called from imprecise.c:148.
-[eva] computing for function gm_f1 <- garbled_mix_null <- main.
-  Called from imprecise.c:75.
 [kernel:annot:missing-spec] imprecise.c:75: Warning: 
   Neither code nor specification for function gm_f1, generating default assigns from the prototype
+[eva] computing for function gm_f1 <- garbled_mix_null <- main.
+  Called from imprecise.c:75.
 [eva] using specification for function gm_f1
 [eva] Done for function gm_f1
 [eva] imprecise.c:76: 
@@ -167,10 +167,10 @@
 [eva:alarm] imprecise.c:77: Warning: 
   accessing left-value that contains escaping addresses.
   assert ¬\dangling(p_gm_null);
-[eva] computing for function gm_f2 <- garbled_mix_null <- main.
-  Called from imprecise.c:77.
 [kernel:annot:missing-spec] imprecise.c:77: Warning: 
   Neither code nor specification for function gm_f2, generating default assigns from the prototype
+[eva] computing for function gm_f2 <- garbled_mix_null <- main.
+  Called from imprecise.c:77.
 [eva] using specification for function gm_f2
 [eva] Done for function gm_f2
 [eva] imprecise.c:78: 
diff --git a/tests/builtins/oracle/watch.res.oracle b/tests/builtins/oracle/watch.res.oracle
index d4614af09571f9432fc8944a259c19c8b41d79f7..d0a7fe337f5359bd6bd41e7536d4d1c6d7489935 100644
--- a/tests/builtins/oracle/watch.res.oracle
+++ b/tests/builtins/oracle/watch.res.oracle
@@ -15,10 +15,10 @@
 [eva] watch.c:10: Call to builtin Frama_C_watch_value
 [eva] watch.c:13: Watchpoint: & c [--..--]
 [eva] watch.c:14: Watchpoint: & c [--..--]
-[eva] computing for function u <- main.
-  Called from watch.c:16.
 [kernel:annot:missing-spec] watch.c:16: Warning: 
   Neither code nor specification for function u, generating default assigns from the prototype
+[eva] computing for function u <- main.
+  Called from watch.c:16.
 [eva] using specification for function u
 [eva] Done for function u
 [eva] watch.c:17: Watchpoint: & c [--..--]
diff --git a/tests/constant_propagation/oracle/fct_ptr.res.oracle b/tests/constant_propagation/oracle/fct_ptr.res.oracle
index 89f9227804b66c8807052a458436b2125ba9e4d8..3b6bf0a4150ceb31f0c6c4089e29839eda1dffd4 100644
--- a/tests/constant_propagation/oracle/fct_ptr.res.oracle
+++ b/tests/constant_propagation/oracle/fct_ptr.res.oracle
@@ -7,10 +7,10 @@
   pf ∈ {0}
 [eva] computing for function g <- main.
   Called from fct_ptr.i:15.
-[eva] computing for function f <- g <- main.
-  Called from fct_ptr.i:8.
 [kernel:annot:missing-spec] fct_ptr.i:8: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- g <- main.
+  Called from fct_ptr.i:8.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for g
diff --git a/tests/float/oracle/alarms.0.res.oracle b/tests/float/oracle/alarms.0.res.oracle
index 56452818c480a652a5846f033d785d4c754fe0da..8e964fd6c677d12e8068ca89de3c960044b80c11 100644
--- a/tests/float/oracle/alarms.0.res.oracle
+++ b/tests/float/oracle/alarms.0.res.oracle
@@ -32,10 +32,10 @@
   tmp ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
-[eva] computing for function fd <- main1 <- main.
-  Called from alarms.i:21.
 [kernel:annot:missing-spec] alarms.i:21: Warning: 
   Neither code nor specification for function fd, generating default assigns from the prototype
+[eva] computing for function fd <- main1 <- main.
+  Called from alarms.i:21.
 [eva] using specification for function fd
 [eva] Done for function fd
 [eva:alarm] alarms.i:21: Warning: 
diff --git a/tests/float/oracle/alarms.1.res.oracle b/tests/float/oracle/alarms.1.res.oracle
index e6c9a72e274d561e744c9b83cf14d450cac99886..95735134c42367149c53c4ba8502e4cc652e78e4 100644
--- a/tests/float/oracle/alarms.1.res.oracle
+++ b/tests/float/oracle/alarms.1.res.oracle
@@ -29,10 +29,10 @@
   tmp ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
-[eva] computing for function fd <- main1 <- main.
-  Called from alarms.i:21.
 [kernel:annot:missing-spec] alarms.i:21: Warning: 
   Neither code nor specification for function fd, generating default assigns from the prototype
+[eva] computing for function fd <- main1 <- main.
+  Called from alarms.i:21.
 [eva] using specification for function fd
 [eva] Done for function fd
 [eva:alarm] alarms.i:21: Warning: 
diff --git a/tests/float/oracle/alarms.2.res.oracle b/tests/float/oracle/alarms.2.res.oracle
index 41b7b1439a87c1d8fe89d3e63226cc6a3a8c321e..6c47a9b44c57b387e173f5f380b9e47c2e794498 100644
--- a/tests/float/oracle/alarms.2.res.oracle
+++ b/tests/float/oracle/alarms.2.res.oracle
@@ -26,10 +26,10 @@
   tmp ∈ UNINITIALIZED
   l ∈ [--..--]
   ==END OF DUMP==
-[eva] computing for function fd <- main1 <- main.
-  Called from alarms.i:21.
 [kernel:annot:missing-spec] alarms.i:21: Warning: 
   Neither code nor specification for function fd, generating default assigns from the prototype
+[eva] computing for function fd <- main1 <- main.
+  Called from alarms.i:21.
 [eva] using specification for function fd
 [eva] Done for function fd
 [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 fe8edb1fd33ab883cdfdee3b00b9c7ecfe98c5f0..86c08416bbdaff949193ab85ef743721a2d09340 100644
--- a/tests/float/oracle/contract_special_float.1.res.oracle
+++ b/tests/float/oracle/contract_special_float.1.res.oracle
@@ -16,10 +16,10 @@
 [eva] Done for function fun
 [eva:alarm] contract_special_float.c:93: Warning: 
   NaN double value. assert ¬\is_NaN(v);
-[eva] computing for function fun_no_default <- main.
-  Called from contract_special_float.c:94.
 [kernel] contract_special_float.c:94: Warning: 
   No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[eva] computing for function fun_no_default <- main.
+  Called from contract_special_float.c:94.
 [eva] using specification for function fun_no_default
 [eva:alarm] contract_special_float.c:94: Warning: 
   function fun_no_default: precondition 'not_negative' got status unknown.
diff --git a/tests/float/oracle/contract_special_float.2.res.oracle b/tests/float/oracle/contract_special_float.2.res.oracle
index 3224017364e22a08d51e47a88d6a0cd9417437b8..daefc3e0500b277b95d58763b0a48636faf4978f 100644
--- a/tests/float/oracle/contract_special_float.2.res.oracle
+++ b/tests/float/oracle/contract_special_float.2.res.oracle
@@ -8,10 +8,10 @@
   Called from contract_special_float.c:92.
 [eva] using specification for function fun
 [eva] Done for function fun
-[eva] computing for function fun_no_default <- main.
-  Called from contract_special_float.c:94.
 [kernel] contract_special_float.c:94: Warning: 
   No code nor explicit assigns clause for function fun_no_default, generating default assigns from the specification
+[eva] computing for function fun_no_default <- main.
+  Called from contract_special_float.c:94.
 [eva] using specification for function fun_no_default
 [eva] Done for function fun_no_default
 [eva] computing for function fun_no_disjoint <- main.
diff --git a/tests/float/oracle/s.res.oracle b/tests/float/oracle/s.res.oracle
index 6efaa5f37230b6b9441b3ac90e4f12c471c609ce..4981289b342551b63ac74d396431c9e71950ca1d 100644
--- a/tests/float/oracle/s.res.oracle
+++ b/tests/float/oracle/s.res.oracle
@@ -244,18 +244,18 @@
   G19 ∈ {0}
 [eva] computing for function F4 <- main.
   Called from s.i:260.
-[eva] computing for function F1 <- F4 <- main.
-  Called from s.i:230.
 [kernel:annot:missing-spec] s.i:230: Warning: 
   Neither code nor specification for function F1, generating default assigns from the prototype
+[eva] computing for function F1 <- F4 <- main.
+  Called from s.i:230.
 [eva] using specification for function F1
 [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;
-[eva] computing for function F2 <- F4 <- main.
-  Called from s.i:233.
 [kernel:annot:missing-spec] s.i:233: Warning: 
   Neither code nor specification for function F2, generating default assigns from the prototype
+[eva] computing for function F2 <- F4 <- main.
+  Called from s.i:233.
 [eva] using specification for function F2
 [eva] Done for function F2
 [eva:alarm] s.i:238: Warning: accessing out of bounds index. assert 0 ≤ V5;
@@ -265,10 +265,10 @@
 [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;
-[eva] computing for function F3 <- F4 <- main.
-  Called from s.i:244.
 [kernel:annot:missing-spec] s.i:244: Warning: 
   Neither code nor specification for function F3, generating default assigns from the prototype
+[eva] computing for function F3 <- F4 <- main.
+  Called from s.i:244.
 [eva] using specification for function F3
 [eva] Done for function F3
 [eva:alarm] s.i:245: Warning: accessing out of bounds index. assert 0 ≤ V7;
diff --git a/tests/impact/oracle/call.0.res.oracle b/tests/impact/oracle/call.0.res.oracle
index 20364db19a0bcb57304643cffb859085f6d40fef..10834db797c6b9fd61331ed083dfe5cd8bcd6edd 100644
--- a/tests/impact/oracle/call.0.res.oracle
+++ b/tests/impact/oracle/call.0.res.oracle
@@ -12,10 +12,10 @@
   Called from call.i:16.
 [eva] using specification for function p1
 [eva] Done for function p1
-[eva] computing for function p2 <- test <- main.
-  Called from call.i:16.
 [kernel:annot:missing-spec] call.i:16: Warning: 
   Neither code nor specification for function p2, generating default assigns from the prototype
+[eva] computing for function p2 <- test <- main.
+  Called from call.i:16.
 [eva] using specification for function p2
 [eva] Done for function p2
 [eva] Recording results for test
diff --git a/tests/impact/oracle/call.1.res.oracle b/tests/impact/oracle/call.1.res.oracle
index 9f1a28300c66fcac0559aa738d890905eb7ca679..7388b39fa5c93ed2feb78abc754f6311667da8f7 100644
--- a/tests/impact/oracle/call.1.res.oracle
+++ b/tests/impact/oracle/call.1.res.oracle
@@ -14,10 +14,10 @@
   Called from call.i:16.
 [eva] using specification for function p1
 [eva] Done for function p1
-[eva] computing for function p2 <- test <- call_test <- main2.
-  Called from call.i:16.
 [kernel:annot:missing-spec] call.i:16: Warning: 
   Neither code nor specification for function p2, generating default assigns from the prototype
+[eva] computing for function p2 <- test <- call_test <- main2.
+  Called from call.i:16.
 [eva] using specification for function p2
 [eva] Done for function p2
 [eva] Recording results for test
diff --git a/tests/impact/oracle/call.2.res.oracle b/tests/impact/oracle/call.2.res.oracle
index 517e087479b9f93b1cecb56c69aec47611bc556c..8f91333b85850fc0097eda8efa92321f9859d39a 100644
--- a/tests/impact/oracle/call.2.res.oracle
+++ b/tests/impact/oracle/call.2.res.oracle
@@ -15,10 +15,10 @@
 [eva] using specification for function p3
 [eva] call.i:41: Warning: no \from part for clause 'assigns G;'
 [eva] Done for function p3
-[eva] computing for function p2 <- test3 <- call_test3 <- main3.
-  Called from call.i:45.
 [kernel:annot:missing-spec] call.i:45: Warning: 
   Neither code nor specification for function p2, generating default assigns from the prototype
+[eva] computing for function p2 <- test3 <- call_test3 <- main3.
+  Called from call.i:45.
 [eva] using specification for function p2
 [eva] Done for function p2
 [eva] Recording results for test3
diff --git a/tests/impact/oracle/undef_function.res.oracle b/tests/impact/oracle/undef_function.res.oracle
index a62609de5f28d0975a112d12effa7d1eb17a31e8..59f4b23f32d44712c698d013533a2cc08693aef3 100644
--- a/tests/impact/oracle/undef_function.res.oracle
+++ b/tests/impact/oracle/undef_function.res.oracle
@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   y ∈ {0}
-[eva] computing for function g <- main.
-  Called from undef_function.i:10.
 [kernel:annot:missing-spec] undef_function.i:10: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from undef_function.i:10.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for main
diff --git a/tests/impact/oracle/variadic.res.oracle b/tests/impact/oracle/variadic.res.oracle
index e36dee6c9a0c0ad3ed90ce5f401da521949b7d6a..b2c68043834b6fd0229f28e39869ed0c22cd78a8 100644
--- a/tests/impact/oracle/variadic.res.oracle
+++ b/tests/impact/oracle/variadic.res.oracle
@@ -6,10 +6,10 @@
 [eva:initial-state] Values of globals at initialization
   y ∈ {0}
   z ∈ {0}
-[eva] computing for function f <- main.
-  Called from variadic.i:12.
 [kernel:annot:missing-spec] variadic.i:12: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from variadic.i:12.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/journal/oracle/intra.res.oracle b/tests/journal/oracle/intra.res.oracle
index 1cd1571223722dac18125880403465facf99258e..052f7084beaf919d15fdb51263abd24d850c2459 100644
--- a/tests/journal/oracle/intra.res.oracle
+++ b/tests/journal/oracle/intra.res.oracle
@@ -48,10 +48,10 @@
   Called from intra.i:89.
 [eva] Recording results for assign
 [eva] Done for function assign
-[eva] computing for function stop <- main.
-  Called from intra.i:92.
 [kernel:annot:missing-spec] intra.i:92: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- main.
+  Called from intra.i:92.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for main
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index 4c13bafba7279dc080a6ef0ddf38420223081c44..d4e3751938630cc926bf1afeda75acff53d06fa0 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -35,10 +35,10 @@
 [eva] Done for function strcpy
 [eva:alarm] search_h.c:32: Warning: 
   out of bounds write. assert \valid(&elementptr->count);
-[eva] computing for function tsearch <- main.
-  Called from search_h.c:34.
 [kernel:annot:missing-spec] search_h.c:34: Warning: 
   Neither code nor specification for function tsearch, generating default assigns from the prototype
+[eva] computing for function tsearch <- main.
+  Called from search_h.c:34.
 [eva] using specification for function tsearch
 [eva:invalid-assigns] search_h.c:34: 
   Completely invalid destination for assigns clause *compar. Ignoring.
@@ -54,10 +54,10 @@
 [eva] Done for function exit
 [eva:alarm] search_h.c:40: Warning: 
   out of bounds read. assert \valid_read((struct element **)node);
-[eva] computing for function twalk <- main.
-  Called from search_h.c:46.
 [kernel:annot:missing-spec] search_h.c:46: Warning: 
   Neither code nor specification for function twalk, generating default assigns from the prototype
+[eva] computing for function twalk <- main.
+  Called from search_h.c:46.
 [eva] using specification for function twalk
 [eva:invalid-assigns] search_h.c:46: 
   Completely invalid destination for assigns clause *action. Ignoring.
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index b687f61add5134e4d083b5ebae573336f0840311..2f4e8e1010d683fc6d97ab5a26862ec2f9459ca8 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -11,10 +11,10 @@
 [eva] spawn_h.c:36: 
   Assigning imprecise value to opt.
   The imprecision originates from Library function {spawn_h.c:36}
-[eva] computing for function posix_spawn_file_actions_init <- main.
-  Called from spawn_h.c:43.
 [kernel:annot:missing-spec] spawn_h.c:43: Warning: 
   Neither code nor specification for function posix_spawn_file_actions_init, generating default assigns from the prototype
+[eva] computing for function posix_spawn_file_actions_init <- main.
+  Called from spawn_h.c:43.
 [eva] using specification for function posix_spawn_file_actions_init
 [eva] Done for function posix_spawn_file_actions_init
 [eva] computing for function perror <- main.
@@ -27,10 +27,10 @@
   Called from spawn_h.c:45.
 [eva] using specification for function exit
 [eva] Done for function exit
-[eva] computing for function posix_spawn_file_actions_addclose <- main.
-  Called from spawn_h.c:47.
 [kernel:annot:missing-spec] spawn_h.c:47: Warning: 
   Neither code nor specification for function posix_spawn_file_actions_addclose, generating default assigns from the prototype
+[eva] computing for function posix_spawn_file_actions_addclose <- main.
+  Called from spawn_h.c:47.
 [eva] using specification for function posix_spawn_file_actions_addclose
 [eva] Done for function posix_spawn_file_actions_addclose
 [eva] computing for function perror <- main.
@@ -41,10 +41,10 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:50.
 [eva] Done for function exit
-[eva] computing for function posix_spawnattr_init <- main.
-  Called from spawn_h.c:60.
 [kernel:annot:missing-spec] spawn_h.c:60: Warning: 
   Neither code nor specification for function posix_spawnattr_init, generating default assigns from the prototype
+[eva] computing for function posix_spawnattr_init <- main.
+  Called from spawn_h.c:60.
 [eva] using specification for function posix_spawnattr_init
 [eva] Done for function posix_spawnattr_init
 [eva] computing for function perror <- main.
@@ -55,10 +55,10 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:62.
 [eva] Done for function exit
-[eva] computing for function posix_spawnattr_setflags <- main.
-  Called from spawn_h.c:63.
 [kernel:annot:missing-spec] spawn_h.c:63: Warning: 
   Neither code nor specification for function posix_spawnattr_setflags, generating default assigns from the prototype
+[eva] computing for function posix_spawnattr_setflags <- main.
+  Called from spawn_h.c:63.
 [eva] using specification for function posix_spawnattr_setflags
 [eva] Done for function posix_spawnattr_setflags
 [eva] computing for function perror <- main.
@@ -75,10 +75,10 @@
 [eva] spawn_h.c:67: 
   function sigfillset: precondition 'valid_set' got status valid.
 [eva] Done for function sigfillset
-[eva] computing for function posix_spawnattr_setsigmask <- main.
-  Called from spawn_h.c:68.
 [kernel:annot:missing-spec] spawn_h.c:68: Warning: 
   Neither code nor specification for function posix_spawnattr_setsigmask, generating default assigns from the prototype
+[eva] computing for function posix_spawnattr_setsigmask <- main.
+  Called from spawn_h.c:68.
 [eva] using specification for function posix_spawnattr_setsigmask
 [eva] Done for function posix_spawnattr_setsigmask
 [eva] computing for function perror <- main.
@@ -143,10 +143,10 @@
 [eva] Done for function exit
 [eva:alarm] spawn_h.c:82: Warning: 
   out of bounds read. assert \valid_read(argv + optind);
-[eva] computing for function posix_spawnp <- main.
-  Called from spawn_h.c:82.
 [kernel:annot:missing-spec] spawn_h.c:82: Warning: 
   Neither code nor specification for function posix_spawnp, generating default assigns from the prototype
+[eva] computing for function posix_spawnp <- main.
+  Called from spawn_h.c:82.
 [eva] using specification for function posix_spawnp
 [eva] Done for function posix_spawnp
 [eva] computing for function perror <- main.
@@ -157,10 +157,10 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:85.
 [eva] Done for function exit
-[eva] computing for function posix_spawnattr_destroy <- main.
-  Called from spawn_h.c:90.
 [kernel:annot:missing-spec] spawn_h.c:90: Warning: 
   Neither code nor specification for function posix_spawnattr_destroy, generating default assigns from the prototype
+[eva] computing for function posix_spawnattr_destroy <- main.
+  Called from spawn_h.c:90.
 [eva] using specification for function posix_spawnattr_destroy
 [eva] Done for function posix_spawnattr_destroy
 [eva] computing for function perror <- main.
@@ -171,10 +171,10 @@
 [eva] computing for function exit <- main.
   Called from spawn_h.c:92.
 [eva] Done for function exit
-[eva] computing for function posix_spawn_file_actions_destroy <- main.
-  Called from spawn_h.c:96.
 [kernel:annot:missing-spec] spawn_h.c:96: Warning: 
   Neither code nor specification for function posix_spawn_file_actions_destroy, generating default assigns from the prototype
+[eva] computing for function posix_spawn_file_actions_destroy <- main.
+  Called from spawn_h.c:96.
 [eva] using specification for function posix_spawn_file_actions_destroy
 [eva] Done for function posix_spawn_file_actions_destroy
 [eva] computing for function perror <- main.
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 145aeb752d3a920752391a5eaaa261f9a2e3e284..1af129e7a33f4659fae790fd9894b9c1db5be0d0 100644
--- a/tests/pdg/oracle/bts1194.res.oracle
+++ b/tests/pdg/oracle/bts1194.res.oracle
@@ -213,10 +213,10 @@
   Y ∈ {0}
 [eva] computing for function f_slice_1 <- main.
   Called from bts1194.c:32.
-[eva] computing for function input <- f_slice_1 <- main.
-  Called from bts1194.c:13.
 [kernel:annot:missing-spec] bts1194.c:13: Warning: 
   Neither code nor specification for function input, generating default assigns from the prototype
+[eva] computing for function input <- f_slice_1 <- main.
+  Called from bts1194.c:13.
 [eva] using specification for function input
 [eva] Done for function input
 [eva:alarm] bts1194.c:17: Warning: assertion got status unknown.
diff --git a/tests/pdg/oracle/no_body.res.oracle b/tests/pdg/oracle/no_body.res.oracle
index cbceb964eb12fbaa49587302d2283bfe7f6e3654..f65d81c52ff573d8b4deff6e9968abe6004ea706 100644
--- a/tests/pdg/oracle/no_body.res.oracle
+++ b/tests/pdg/oracle/no_body.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ {0}
-[eva] computing for function f <- main.
-  Called from no_body.c:24.
 [kernel:annot:missing-spec] no_body.c:24: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from no_body.c:24.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] computing for function loop <- main.
diff --git a/tests/pdg/oracle/pb_infinite_loop.2.res.oracle b/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
index 630316bb7ff028f2aa704681ff10def50844de5a..70e67333d4cf25a264fb22ebbd70e1ac5c76a12e 100644
--- a/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
+++ b/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ [--..--]
-[eva] computing for function exit <- test_exit.
-  Called from pb_infinite_loop.c:48.
 [kernel:annot:missing-spec] pb_infinite_loop.c:48: Warning: 
   Neither code nor specification for function exit, generating default assigns from the prototype
+[eva] computing for function exit <- test_exit.
+  Called from pb_infinite_loop.c:48.
 [eva] using specification for function exit
 [eva] Done for function exit
 [eva] Recording results for test_exit
diff --git a/tests/pdg/oracle/variadic.res.oracle b/tests/pdg/oracle/variadic.res.oracle
index 4557ce0ab0dd6b19ee856acfaf566f2d8344cab4..2ff0dc65eba330eaff972dff1d8bfb863dad12df 100644
--- a/tests/pdg/oracle/variadic.res.oracle
+++ b/tests/pdg/oracle/variadic.res.oracle
@@ -6,10 +6,10 @@
   
 [eva] computing for function f1 <- main.
   Called from variadic.c:37.
-[eva] computing for function lib_f <- f1 <- main.
-  Called from variadic.c:23.
 [kernel:annot:missing-spec] variadic.c:23: Warning: 
   Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] computing for function lib_f <- f1 <- main.
+  Called from variadic.c:23.
 [eva] using specification for function lib_f
 [eva] Done for function lib_f
 [eva] Recording results for f1
diff --git a/tests/scope/oracle/bts383.res.oracle b/tests/scope/oracle/bts383.res.oracle
index 28b7158a7c81c8e3cfcb75761b2623a177c214a5..5800bac5891a9bec7ec03be35240d922082f7cca 100644
--- a/tests/scope/oracle/bts383.res.oracle
+++ b/tests/scope/oracle/bts383.res.oracle
@@ -38,10 +38,10 @@
   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);
-[eva] computing for function out_char <- out_string <- main.
-  Called from bts383.c:36.
 [kernel:annot:missing-spec] bts383.c:36: Warning: 
   Neither code nor specification for function out_char, generating default assigns from the prototype
+[eva] computing for function out_char <- out_string <- main.
+  Called from bts383.c:36.
 [eva] using specification for function out_char
 [eva] Done for function out_char
 [eva] bts383.c:35: starting to merge loop iterations
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 3a40e1f72cfdd0497f04c3a4a40fd43a0047bc6c..b9ebf7ff3bdbeb98fb1c7e6b59e1ba898e36792f 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -10,10 +10,10 @@
   step ∈ {0}
 [eva] computing for function lecture <- main.
   Called from bts1768.i:45.
-[eva] computing for function choisir <- lecture <- main.
-  Called from bts1768.i:18.
 [kernel] bts1768.i:18: Warning: 
   No code nor implicit assigns clause for function choisir, generating default assigns from the prototype
+[eva] computing for function choisir <- lecture <- main.
+  Called from bts1768.i:18.
 [eva] using specification for function choisir
 [eva] Done for function choisir
 [eva] Recording results for lecture
diff --git a/tests/slicing/oracle/bts709.res.oracle b/tests/slicing/oracle/bts709.res.oracle
index eeb349a839c18ef29ec2b3fce4e7dca38cc12998..8230e738d1b9a9e282706d7e5e2bde3e68d37a03 100644
--- a/tests/slicing/oracle/bts709.res.oracle
+++ b/tests/slicing/oracle/bts709.res.oracle
@@ -9,10 +9,10 @@
   var2 IN {0}
 [eva] computing for function inputsOf_testcase_func <- main.
   Called from bts709.c:47.
-[eva] computing for function nondet_int <- inputsOf_testcase_func <- main.
-  Called from bts709.c:55.
 [kernel:annot:missing-spec] bts709.c:55: Warning: 
   Neither code nor specification for function nondet_int, generating default assigns from the prototype
+[eva] computing for function nondet_int <- inputsOf_testcase_func <- main.
+  Called from bts709.c:55.
 [eva] using specification for function nondet_int
 [eva] Done for function nondet_int
 [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 a9894ef7c846fce6d6a1069847511b0912c64183..59b371fa22936b89432dee3c3dd180b20291895f 100644
--- a/tests/slicing/oracle/combine.res.oracle
+++ b/tests/slicing/oracle/combine.res.oracle
@@ -121,10 +121,10 @@ int main(int x)
   
 [eva] computing for function f <- main.
   Called from combine.i:24.
-[eva] computing for function g <- f <- main.
-  Called from combine.i:17.
 [kernel:annot:missing-spec] combine.i:17: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- f <- main.
+  Called from combine.i:17.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/filter.res.oracle b/tests/slicing/oracle/filter.res.oracle
index 3d965436dc7a3a1ee3df68d55401c0c142a4c6b3..f4a04eb5b5eb35e339107a6837a5007ba5c4a40e 100644
--- a/tests/slicing/oracle/filter.res.oracle
+++ b/tests/slicing/oracle/filter.res.oracle
@@ -11,10 +11,10 @@
 [eva] Done for function bts806
 [eva] computing for function unspec <- main.
   Called from filter.i:43.
-[eva] computing for function f <- unspec <- main.
-  Called from filter.i:36.
 [kernel:annot:missing-spec] filter.i:36: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- unspec <- main.
+  Called from filter.i:36.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for unspec
diff --git a/tests/slicing/oracle/loops.15.res.oracle b/tests/slicing/oracle/loops.15.res.oracle
index 16dd3f30158a46fd9c7adbdb72fd0b6762691220..eec7e4e722e0f6d94f986ee16dd341399f5aa0de 100644
--- a/tests/slicing/oracle/loops.15.res.oracle
+++ b/tests/slicing/oracle/loops.15.res.oracle
@@ -11,10 +11,10 @@
   Z ∈ [--..--]
 [eva] loops.i:68: assertion got status valid.
 [eva] loops.i:66: starting to merge loop iterations
-[eva] computing for function stop <- stop_f1.
-  Called from loops.i:70.
 [kernel:annot:missing-spec] loops.i:70: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- stop_f1.
+  Called from loops.i:70.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for stop_f1
diff --git a/tests/slicing/oracle/loops.16.res.oracle b/tests/slicing/oracle/loops.16.res.oracle
index 3fd8813c21437c89615b4e571cae3dc0621375e8..bea08b5034d7a62fa70d6672bc961b9844d392e4 100644
--- a/tests/slicing/oracle/loops.16.res.oracle
+++ b/tests/slicing/oracle/loops.16.res.oracle
@@ -11,10 +11,10 @@
   Z ∈ [--..--]
 [eva] loops.i:68: assertion got status valid.
 [eva] loops.i:66: starting to merge loop iterations
-[eva] computing for function stop <- stop_f1.
-  Called from loops.i:70.
 [kernel:annot:missing-spec] loops.i:70: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- stop_f1.
+  Called from loops.i:70.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for stop_f1
diff --git a/tests/slicing/oracle/loops.17.res.oracle b/tests/slicing/oracle/loops.17.res.oracle
index aa15e9fe124a5770fe1936ed9c8ef0f200e1c07d..0537db0b91b439f6d941bd35953f79ae36c7ac50 100644
--- a/tests/slicing/oracle/loops.17.res.oracle
+++ b/tests/slicing/oracle/loops.17.res.oracle
@@ -11,10 +11,10 @@
   Z ∈ [--..--]
 [eva:alarm] loops.i:82: Warning: signed overflow. assert c + 10 ≤ 2147483647;
 [eva:alarm] loops.i:88: Warning: assertion got status unknown.
-[eva] computing for function stop <- stop_f2.
-  Called from loops.i:89.
 [kernel:annot:missing-spec] loops.i:89: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- stop_f2.
+  Called from loops.i:89.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for stop_f2
diff --git a/tests/slicing/oracle/loops.18.res.oracle b/tests/slicing/oracle/loops.18.res.oracle
index 04dc49b1ee3eb3b6b7eb0101612a851b90c3afea..70c363c51dfa1f85af6e0ac42d201e7a7fb24902 100644
--- a/tests/slicing/oracle/loops.18.res.oracle
+++ b/tests/slicing/oracle/loops.18.res.oracle
@@ -11,10 +11,10 @@
   Z ∈ [--..--]
 [eva:alarm] loops.i:82: Warning: signed overflow. assert c + 10 ≤ 2147483647;
 [eva:alarm] loops.i:88: Warning: assertion got status unknown.
-[eva] computing for function stop <- stop_f2.
-  Called from loops.i:89.
 [kernel:annot:missing-spec] loops.i:89: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- stop_f2.
+  Called from loops.i:89.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for stop_f2
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index f3607c3ab3b4940722b6795cd9097a58361a414b..b13c5f6f59cd8e63d0a775d0a152267be24013e2 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -10,16 +10,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -56,10 +56,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/ptr_fct.res.oracle b/tests/slicing/oracle/ptr_fct.res.oracle
index 3d93973ee4d712091d3a3481daadce5f39f5140c..6b36f47ccf37855a27b08a2cf1d3a1938ded6f75 100644
--- a/tests/slicing/oracle/ptr_fct.res.oracle
+++ b/tests/slicing/oracle/ptr_fct.res.oracle
@@ -8,10 +8,10 @@
   ptf ∈ {0}
 [eva] computing for function g <- h.
   Called from ptr_fct.i:23.
-[eva] computing for function f2 <- g <- h.
-  Called from ptr_fct.i:17.
 [kernel:annot:missing-spec] ptr_fct.i:17: Warning: 
   Neither code nor specification for function f2, generating default assigns from the prototype
+[eva] computing for function f2 <- g <- h.
+  Called from ptr_fct.i:17.
 [eva] using specification for function f2
 [eva] Done for function f2
 [eva] computing for function f1 <- 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 31ce22ade863eab258bb37862d1de367a96ec7f3..8d7e7082e3c68493a11f27374b28923f8223180b 100644
--- a/tests/slicing/oracle/select_by_annot.0.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.0.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index c0f3575f5dc322dc8ddc849af89fecdd2f29787c..ae07dade26d480fce1d7cf3ee17ffda866ceea2f 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index c30f26887f6c5c0f036094807aed8fdbd49a114e..34f900b14e6424248c3a94c0518b5ce35c7d215f 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.11.res.oracle b/tests/slicing/oracle/select_by_annot.11.res.oracle
index 5b27209920b895c89f8c23bb3135d9795246fff3..9b3fce6ec83a8544876c066e958976b8a785c42e 100644
--- a/tests/slicing/oracle/select_by_annot.11.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.11.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index 0c6fe54f4cf7193a2ad7426653f3d44ee3dd95f9..762c51f3171fad5510ae4f93098fcb85a30ae48b 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.13.res.oracle b/tests/slicing/oracle/select_by_annot.13.res.oracle
index 8f680bd8056d3f27317815d56659cba58465bbcd..98dd4ebe7bdc9857052b79c9db5c412734bf9593 100644
--- a/tests/slicing/oracle/select_by_annot.13.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.13.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index 69d8673daf166031a605627daf7ea23bf6e550b7..0a2424c7fb144a6ee4b07f112186d748e5cc4735 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.2.res.oracle b/tests/slicing/oracle/select_by_annot.2.res.oracle
index 2447ad2d3380583eb6259cbc192eb559dc8606f5..169060a52c2f9bf8462882d4d3ebbaad08b07050 100644
--- a/tests/slicing/oracle/select_by_annot.2.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.2.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index 25a50f5cd59edd247f74833690d9f3bbb92a43b2..3afd30f22fd2fc6c6eaf7547a8db88211208d942 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 8d2642c6fa807da28c38c401e1b4c12ba49dbf92..6997ef7e7a89dc508c40abde0826544c0163a20b 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index 165cc861ab72f82a834e850c7a4f33b9433b2fe0..324e00126ff00f1c013cfab833844601bddd6871 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index fb469fe2139a5a8b7b8bdc417b29db69356e5965..233dfb495a340d13e22b8bd006b1cd71aa50b730 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index 540bcb17efb6a9e698444e3b15ea6bb2c7dbf3e4..87bb4419e117e5cf001669267484e66ee112728c 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index 31a3e7b24478f1607ad9dd209a798ced369857cd..e92d795a5c11d703abcb62c7229b145306f29c63 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index 8140a0c2883108a82fbc579a14c6cd12742f03fd..a3c5b6b83688036eadee760d98c6de3e4a24e8ed 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -18,10 +18,10 @@
   signed overflow. assert S.a + a ≤ 2147483647;
 [eva] Recording results for modifS
 [eva] Done for function modifS
-[eva] computing for function new_int <- main.
-  Called from select_by_annot.i:140.
 [kernel:annot:missing-spec] select_by_annot.i:140: Warning: 
   Neither code nor specification for function new_int, generating default assigns from the prototype
+[eva] computing for function new_int <- main.
+  Called from select_by_annot.i:140.
 [eva] using specification for function new_int
 [eva] Done for function new_int
 [eva] computing for function f1 <- main.
diff --git a/tests/slicing/oracle/select_calls.0.res.oracle b/tests/slicing/oracle/select_calls.0.res.oracle
index 94b3e49273274813cf5e473e27472d797f7ec762..a684da35d348c819ce341aba38bfb7e132ee2b74 100644
--- a/tests/slicing/oracle/select_calls.0.res.oracle
+++ b/tests/slicing/oracle/select_calls.0.res.oracle
@@ -6,19 +6,19 @@
 [eva:initial-state] Values of globals at initialization
   c ∈ [--..--]
   d ∈ [--..--]
-[eva] computing for function send <- f.
-  Called from select_calls.i:22.
 [kernel:annot:missing-spec] select_calls.i:22: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f.
+  Called from select_calls.i:22.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] computing for function send <- f.
   Called from select_calls.i:23.
 [eva] Done for function send
-[eva] computing for function crypt <- f.
-  Called from select_calls.i:24.
 [kernel:annot:missing-spec] select_calls.i:24: Warning: 
   Neither code nor specification for function crypt, generating default assigns from the prototype
+[eva] computing for function crypt <- f.
+  Called from select_calls.i:24.
 [eva] using specification for function crypt
 [eva] Done for function crypt
 [eva] computing for function send <- f.
@@ -27,10 +27,10 @@
 [eva] computing for function send <- f.
   Called from select_calls.i:28.
 [eva] Done for function send
-[eva] computing for function uncrypt <- f.
-  Called from select_calls.i:30.
 [kernel:annot:missing-spec] select_calls.i:30: Warning: 
   Neither code nor specification for function uncrypt, generating default assigns from the prototype
+[eva] computing for function uncrypt <- f.
+  Called from select_calls.i:30.
 [eva] using specification for function uncrypt
 [eva] Done for function uncrypt
 [eva] computing for function send <- f.
diff --git a/tests/slicing/oracle/select_calls.1.res.oracle b/tests/slicing/oracle/select_calls.1.res.oracle
index 7a93b917c1ac311b745dc0f3d6b433818f1268ee..9d99c35a72c437ac31e3e1e1388c277c296e64e7 100644
--- a/tests/slicing/oracle/select_calls.1.res.oracle
+++ b/tests/slicing/oracle/select_calls.1.res.oracle
@@ -6,10 +6,10 @@
 [eva:initial-state] Values of globals at initialization
   c ∈ [--..--]
   d ∈ [--..--]
-[eva] computing for function nothing <- g.
-  Called from select_calls.i:42.
 [kernel:annot:missing-spec] select_calls.i:42: Warning: 
   Neither code nor specification for function nothing, generating default assigns from the prototype
+[eva] computing for function nothing <- g.
+  Called from select_calls.i:42.
 [eva] using specification for function nothing
 [eva] Done for function nothing
 [eva] Recording results for g
diff --git a/tests/slicing/oracle/select_return.0.res.oracle b/tests/slicing/oracle/select_return.0.res.oracle
index 8e3f0312d8029824207255aef5444406e99e9b50..c11f145c96547f4c50ce6114b7d7cc30bc17c10d 100644
--- a/tests/slicing/oracle/select_return.0.res.oracle
+++ b/tests/slicing/oracle/select_return.0.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.1.res.oracle b/tests/slicing/oracle/select_return.1.res.oracle
index 85264a8d545404c7d6e0a1f26ffe35ffabd0b1bf..9c6ec7fbefb3098d928fe89409980bda00eccc58 100644
--- a/tests/slicing/oracle/select_return.1.res.oracle
+++ b/tests/slicing/oracle/select_return.1.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.10.res.oracle b/tests/slicing/oracle/select_return.10.res.oracle
index dcdfd537935503464f352abdb8a50f0ac9c2c826..2e7bb25265f9543976a6f12f6bee99da0be882a0 100644
--- a/tests/slicing/oracle/select_return.10.res.oracle
+++ b/tests/slicing/oracle/select_return.10.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.11.res.oracle b/tests/slicing/oracle/select_return.11.res.oracle
index cbd031e0a0c408883af1bff8a4116dc0b05bac31..e1608c0ea0a8deec6ac5f60af4786efd92ab3a2c 100644
--- a/tests/slicing/oracle/select_return.11.res.oracle
+++ b/tests/slicing/oracle/select_return.11.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.12.res.oracle b/tests/slicing/oracle/select_return.12.res.oracle
index 1359b8875417bbe9e020d1f1fe7f6f885d7f4c04..d05d1bf75388534ac46553c2749f615ef0358a4c 100644
--- a/tests/slicing/oracle/select_return.12.res.oracle
+++ b/tests/slicing/oracle/select_return.12.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.13.res.oracle b/tests/slicing/oracle/select_return.13.res.oracle
index e1b8f746bbeb4fb79a80ee506af233834d2a44cc..3e93305f88758089dfd68cddb5c2dad84b61fe75 100644
--- a/tests/slicing/oracle/select_return.13.res.oracle
+++ b/tests/slicing/oracle/select_return.13.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.14.res.oracle b/tests/slicing/oracle/select_return.14.res.oracle
index 19c955fa3e88eb6ff2894f6542b3f726bfa28629..78eee4e08b70f6742b2ea85c701c427cc1d91cd7 100644
--- a/tests/slicing/oracle/select_return.14.res.oracle
+++ b/tests/slicing/oracle/select_return.14.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.15.res.oracle b/tests/slicing/oracle/select_return.15.res.oracle
index f1324cfe026e73d64021f6e3a28b1570eb12921f..2fe88bed783cb40305be67f1bedfb8ec7a5e650a 100644
--- a/tests/slicing/oracle/select_return.15.res.oracle
+++ b/tests/slicing/oracle/select_return.15.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.16.res.oracle b/tests/slicing/oracle/select_return.16.res.oracle
index 75cb38c7d7f7f327e2ecc75735bfa425702bba73..d12c38a5def65774d149656ca9a641fd955d1ac1 100644
--- a/tests/slicing/oracle/select_return.16.res.oracle
+++ b/tests/slicing/oracle/select_return.16.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.17.res.oracle b/tests/slicing/oracle/select_return.17.res.oracle
index 60119b1ea8b86a0c01dcbfda9e987d21a4912761..9d0c0e93a698cce3c2eaa9e0a3b7c8691f5eea1f 100644
--- a/tests/slicing/oracle/select_return.17.res.oracle
+++ b/tests/slicing/oracle/select_return.17.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.18.res.oracle b/tests/slicing/oracle/select_return.18.res.oracle
index a1023b621f83c5888ca889df20c9f242cbd7255a..f2116fc192526cf851f636d405e617254d18e374 100644
--- a/tests/slicing/oracle/select_return.18.res.oracle
+++ b/tests/slicing/oracle/select_return.18.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.19.res.oracle b/tests/slicing/oracle/select_return.19.res.oracle
index 3df04b0b9e8cad44e7424b9df84f2f3c8d688818..ca61ac7c11d4e94706315ebb24a4dcae4b37a32e 100644
--- a/tests/slicing/oracle/select_return.19.res.oracle
+++ b/tests/slicing/oracle/select_return.19.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.2.res.oracle b/tests/slicing/oracle/select_return.2.res.oracle
index 479a7c97c1a8645423e66d9ddb09483ac4fac8a7..12e4ac0f72be9bb0c328c7b5ffe8e7ee8fc92f6c 100644
--- a/tests/slicing/oracle/select_return.2.res.oracle
+++ b/tests/slicing/oracle/select_return.2.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.20.res.oracle b/tests/slicing/oracle/select_return.20.res.oracle
index af21538130724556d55802fade61f07027acb07a..112c5f5bfe9daaae6f4a0c6d340a8bed4f4f1ca1 100644
--- a/tests/slicing/oracle/select_return.20.res.oracle
+++ b/tests/slicing/oracle/select_return.20.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.21.res.oracle b/tests/slicing/oracle/select_return.21.res.oracle
index be094adf73b8f896253f2a9b03190c4e5e6fff3b..fc7b7263a782cac7b7a43e2648a76856c9a41910 100644
--- a/tests/slicing/oracle/select_return.21.res.oracle
+++ b/tests/slicing/oracle/select_return.21.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.3.res.oracle b/tests/slicing/oracle/select_return.3.res.oracle
index 1dc96345e15dc2a4b95869aef28dce9455cb77be..9812edcd573de0eb8a5dcce0fdf3242713794af0 100644
--- a/tests/slicing/oracle/select_return.3.res.oracle
+++ b/tests/slicing/oracle/select_return.3.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.4.res.oracle b/tests/slicing/oracle/select_return.4.res.oracle
index 3a8819580ec3c90411f89b31c0e4d8a207b258dd..54256a9999125e620220427a33c4e2925f0ef150 100644
--- a/tests/slicing/oracle/select_return.4.res.oracle
+++ b/tests/slicing/oracle/select_return.4.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.5.res.oracle b/tests/slicing/oracle/select_return.5.res.oracle
index da7288950985eff6f33ddb9c1455acaf5ef0aab8..4f5db2fd09eca3dfe8a0201723d86780d23d5257 100644
--- a/tests/slicing/oracle/select_return.5.res.oracle
+++ b/tests/slicing/oracle/select_return.5.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.6.res.oracle b/tests/slicing/oracle/select_return.6.res.oracle
index 206f26b5c652b7295eb1071f2c6108f28306001f..49367975721c747f4f69145fc1a06a93dda92f74 100644
--- a/tests/slicing/oracle/select_return.6.res.oracle
+++ b/tests/slicing/oracle/select_return.6.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.7.res.oracle b/tests/slicing/oracle/select_return.7.res.oracle
index 166d4eb39460d432449c3b437f89a4b216f9a358..805198cb1ee88eca06a4ebe6ce714073ec356dca 100644
--- a/tests/slicing/oracle/select_return.7.res.oracle
+++ b/tests/slicing/oracle/select_return.7.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.8.res.oracle b/tests/slicing/oracle/select_return.8.res.oracle
index 7a3e2021331fc0a0b41d606ebb7adc1584e6378f..46f7ae572759a6c7d306a249cb2184777a73eabd 100644
--- a/tests/slicing/oracle/select_return.8.res.oracle
+++ b/tests/slicing/oracle/select_return.8.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return.9.res.oracle b/tests/slicing/oracle/select_return.9.res.oracle
index 08c18f52960abe07bedb53b5d8cf57e75d5c4302..cefcbc973ebe0865baa8dfcc2a1834618960f06d 100644
--- a/tests/slicing/oracle/select_return.9.res.oracle
+++ b/tests/slicing/oracle/select_return.9.res.oracle
@@ -11,16 +11,16 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return.i:44.
-[eva] computing for function get <- k <- g.
-  Called from select_return.i:35.
 [kernel:annot:missing-spec] select_return.i:35: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return.i:35.
 [eva] using specification for function get
 [eva] Done for function get
-[eva] computing for function send_bis <- k <- g.
-  Called from select_return.i:39.
 [kernel:annot:missing-spec] select_return.i:39: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k <- g.
+  Called from select_return.i:39.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k
@@ -57,10 +57,10 @@
 [eva] Done for function send_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return.i:53.
 [kernel:annot:missing-spec] select_return.i:53: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return.i:53.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.0.res.oracle b/tests/slicing/oracle/select_return_bis.0.res.oracle
index 3f7c4dea6927a05468a0f96dd08061e4171f998c..8ea8588123349807331da21444ad76db30e4a29d 100644
--- a/tests/slicing/oracle/select_return_bis.0.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.0.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.1.res.oracle b/tests/slicing/oracle/select_return_bis.1.res.oracle
index c3940889b4c4eb2a2c3ecfd986c86c5d75eda8ec..1985843e0c856671e582c9b8b4a053bc292fede0 100644
--- a/tests/slicing/oracle/select_return_bis.1.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.1.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.10.res.oracle b/tests/slicing/oracle/select_return_bis.10.res.oracle
index ea0823f9f32639ec35318dd1e686da5c697d22d1..e32eca9c3afcf0fba7d02dc1aa2be8f452f43b57 100644
--- a/tests/slicing/oracle/select_return_bis.10.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.10.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.2.res.oracle b/tests/slicing/oracle/select_return_bis.2.res.oracle
index d057238968c7951d74fceffe308cc2e5d37da6ed..7373b5277664370907b74738fc337fff836d4237 100644
--- a/tests/slicing/oracle/select_return_bis.2.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.2.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.3.res.oracle b/tests/slicing/oracle/select_return_bis.3.res.oracle
index da97a2aa60c105fb8d421a78abec6bb6064441b8..92082b533a77c7a257928f2a408552424230dbb6 100644
--- a/tests/slicing/oracle/select_return_bis.3.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.3.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.4.res.oracle b/tests/slicing/oracle/select_return_bis.4.res.oracle
index 1447173a96e30c85ea12d0d1be2fa44262f9b7d3..4a345c49e0b0fc9e47497c43bf4142b1038462ae 100644
--- a/tests/slicing/oracle/select_return_bis.4.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.4.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.5.res.oracle b/tests/slicing/oracle/select_return_bis.5.res.oracle
index d85a5be0f6b9c0bebf1728a5dfce808a8986be66..fc53a600ed4dc48067618fe1005b7498cbaf1300 100644
--- a/tests/slicing/oracle/select_return_bis.5.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.5.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.6.res.oracle b/tests/slicing/oracle/select_return_bis.6.res.oracle
index fc50b4155ac11681c74a0440f9b8f6dbba2fb428..a31e484106f52830ef839784d4e6aae2eaff223c 100644
--- a/tests/slicing/oracle/select_return_bis.6.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.6.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.7.res.oracle b/tests/slicing/oracle/select_return_bis.7.res.oracle
index 0cbccc1d95c6dc0210546787ce22961315395c98..59ffe732a6ad243c161c54e6f25438d85d449fa9 100644
--- a/tests/slicing/oracle/select_return_bis.7.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.7.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.8.res.oracle b/tests/slicing/oracle/select_return_bis.8.res.oracle
index 578fb7a7f41e9c184a85893aba3a84d3643ce44a..956b521ba11c369ef2ab05c5a5902722fb7d6fb6 100644
--- a/tests/slicing/oracle/select_return_bis.8.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.8.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/select_return_bis.9.res.oracle b/tests/slicing/oracle/select_return_bis.9.res.oracle
index c0c04e4202fef80c95ceeccb2d9d3aeaafdd0cb1..7d550fad782ab271bbcf82ea51f7114013fa0f2d 100644
--- a/tests/slicing/oracle/select_return_bis.9.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.9.res.oracle
@@ -11,18 +11,18 @@
   I ∈ [--..--]
 [eva] computing for function k <- g.
   Called from select_return_bis.i:35.
-[eva] computing for function get <- k <- g.
-  Called from select_return_bis.i:28.
 [kernel:annot:missing-spec] select_return_bis.i:28: Warning: 
   Neither code nor specification for function get, generating default assigns from the prototype
+[eva] computing for function get <- k <- g.
+  Called from select_return_bis.i:28.
 [eva] using specification for function get
 [eva] Done for function get
 [eva] computing for function k_bis <- k <- g.
   Called from select_return_bis.i:30.
-[eva] computing for function send_bis <- k_bis <- k <- g.
-  Called from select_return_bis.i:24.
 [kernel:annot:missing-spec] select_return_bis.i:24: Warning: 
   Neither code nor specification for function send_bis, generating default assigns from the prototype
+[eva] computing for function send_bis <- k_bis <- k <- g.
+  Called from select_return_bis.i:24.
 [eva] using specification for function send_bis
 [eva] Done for function send_bis
 [eva] Recording results for k_bis
@@ -61,10 +61,10 @@
 [eva] select_return_bis.i:30: Reusing old results for call to k_bis
 [eva] Recording results for k
 [eva] Done for function k
-[eva] computing for function send <- f <- g.
-  Called from select_return_bis.i:44.
 [kernel:annot:missing-spec] select_return_bis.i:44: Warning: 
   Neither code nor specification for function send, generating default assigns from the prototype
+[eva] computing for function send <- f <- g.
+  Called from select_return_bis.i:44.
 [eva] using specification for function send
 [eva] Done for function send
 [eva] Recording results for f
diff --git a/tests/slicing/oracle/slice_no_body.res.oracle b/tests/slicing/oracle/slice_no_body.res.oracle
index ddb4f878d25fd38dae70874ab3737a90d4ed490b..a7c932d646a3ed5a0a9411307ea45983aff513f1 100644
--- a/tests/slicing/oracle/slice_no_body.res.oracle
+++ b/tests/slicing/oracle/slice_no_body.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ [--..--]
-[eva] computing for function f <- h.
-  Called from slice_no_body.i:21.
 [kernel:annot:missing-spec] slice_no_body.i:21: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- h.
+  Called from slice_no_body.i:21.
 [eva] using specification for function f
 [eva] Done for function f
 [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 b9bdf5dc091f20376705e2042a1f036b167d23dd..3bcb555020cb6c3231d12de2808185c7a9838b11 100644
--- a/tests/slicing/oracle/unravel-flavors.0.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.0.res.oracle
@@ -61,10 +61,10 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-flavors.i:19.
 [kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-flavors.i:19.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-flavors.1.res.oracle b/tests/slicing/oracle/unravel-flavors.1.res.oracle
index 2499a87e271696fec5e39fe9b448984293157bdd..17186c7cd187ee83e11fe23a7562422a87eeab3d 100644
--- a/tests/slicing/oracle/unravel-flavors.1.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.1.res.oracle
@@ -61,10 +61,10 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-flavors.i:19.
 [kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-flavors.i:19.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-flavors.2.res.oracle b/tests/slicing/oracle/unravel-flavors.2.res.oracle
index 99c65cccbeaa018f23f297e5a989f47e2e59b777..0402f471ca708f0205f1e2ef4a1de623691d5b6c 100644
--- a/tests/slicing/oracle/unravel-flavors.2.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.2.res.oracle
@@ -61,10 +61,10 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-flavors.i:19.
 [kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-flavors.i:19.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-flavors.3.res.oracle b/tests/slicing/oracle/unravel-flavors.3.res.oracle
index 06320e6214a02e9f8c3339e0e9d2b20704d336b1..fe639f3a189614c3fa11656ada21f454c1cb0967 100644
--- a/tests/slicing/oracle/unravel-flavors.3.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.3.res.oracle
@@ -61,10 +61,10 @@
   signed overflow. assert yellow + green ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-flavors.i:60.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-flavors.i:19.
 [kernel:annot:missing-spec] unravel-flavors.i:19: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-flavors.i:19.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-point.0.res.oracle b/tests/slicing/oracle/unravel-point.0.res.oracle
index e7cd4149d40dffc78b9c51f33a629696a8c3a103..ac85ebce1875c26d1452683f3c4f8d89ffcb9afb 100644
--- a/tests/slicing/oracle/unravel-point.0.res.oracle
+++ b/tests/slicing/oracle/unravel-point.0.res.oracle
@@ -36,10 +36,10 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-point.i:36.
 [kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-point.i:36.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-point.1.res.oracle b/tests/slicing/oracle/unravel-point.1.res.oracle
index eacf84e9425cc9038a2c48e1a080a2fdf6677c96..b51385835fffcd8731380223ea577b4fcaf2a094 100644
--- a/tests/slicing/oracle/unravel-point.1.res.oracle
+++ b/tests/slicing/oracle/unravel-point.1.res.oracle
@@ -36,10 +36,10 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-point.i:36.
 [kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-point.i:36.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-point.2.res.oracle b/tests/slicing/oracle/unravel-point.2.res.oracle
index cae8b16117c7b4728aad7a8cad03ced5b2205832..2e29586990b327a64dd22184c3b459f3357622fe 100644
--- a/tests/slicing/oracle/unravel-point.2.res.oracle
+++ b/tests/slicing/oracle/unravel-point.2.res.oracle
@@ -36,10 +36,10 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-point.i:36.
 [kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-point.i:36.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-point.3.res.oracle b/tests/slicing/oracle/unravel-point.3.res.oracle
index 762e31c287dbe235d1c4ec7fed1bca56c636182b..75d9af9abc2f2af899622bd58dcfa3dd543ae226 100644
--- a/tests/slicing/oracle/unravel-point.3.res.oracle
+++ b/tests/slicing/oracle/unravel-point.3.res.oracle
@@ -36,10 +36,10 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-point.i:36.
 [kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-point.i:36.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
diff --git a/tests/slicing/oracle/unravel-point.4.res.oracle b/tests/slicing/oracle/unravel-point.4.res.oracle
index 3bacc2068096deeb3130c792e45f46d70849b19e..6303ed58ec186d15f4a4d6ab64e9061a6692b2af 100644
--- a/tests/slicing/oracle/unravel-point.4.res.oracle
+++ b/tests/slicing/oracle/unravel-point.4.res.oracle
@@ -36,10 +36,10 @@
   signed overflow. assert *y + *x ≤ 2147483647;
 [eva] computing for function send1 <- main.
   Called from unravel-point.i:75.
-[eva] computing for function printf <- send1 <- main.
-  Called from unravel-point.i:36.
 [kernel:annot:missing-spec] unravel-point.i:36: Warning: 
   Neither code nor specification for function printf, generating default assigns from the prototype
+[eva] computing for function printf <- send1 <- main.
+  Called from unravel-point.i:36.
 [eva] using specification for function printf
 [eva] Done for function printf
 [eva] Recording results for send1
@@ -139,10 +139,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function scanf <- main.
-  Called from unravel-point.i:59.
 [kernel:annot:missing-spec] unravel-point.i:59: Warning: 
   Neither code nor specification for function scanf, generating default assigns from the prototype
+[eva] computing for function scanf <- main.
+  Called from unravel-point.i:59.
 [eva] using specification for function scanf
 [eva] Done for function scanf
 [eva:alarm] unravel-point.i:60: Warning: 
diff --git a/tests/slicing/oracle/unravel-variance.0.res.oracle b/tests/slicing/oracle/unravel-variance.0.res.oracle
index 1c8e34235197346f72f1a569ce80fc062fc11642..ce81c2c6e23826179c5c6549698a5d4e50933f9b 100644
--- a/tests/slicing/oracle/unravel-variance.0.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.0.res.oracle
@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function scanf <- main.
-  Called from unravel-variance.i:31.
 [kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf, generating default assigns from the prototype
+[eva] computing for function scanf <- main.
+  Called from unravel-variance.i:31.
 [eva] using specification for function scanf
 [eva] Done for function scanf
 [eva:alarm] unravel-variance.i:32: Warning: 
@@ -122,10 +122,10 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[eva] computing for function printf1 <- main.
-  Called from unravel-variance.i:52.
 [kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1, generating default assigns from the prototype
+[eva] computing for function printf1 <- main.
+  Called from unravel-variance.i:52.
 [eva] using specification for function printf1
 [eva] Done for function printf1
 [eva:alarm] unravel-variance.i:53: Warning: 
@@ -134,10 +134,10 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[eva] computing for function printf2 <- main.
-  Called from unravel-variance.i:53.
 [kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2, generating default assigns from the prototype
+[eva] computing for function printf2 <- main.
+  Called from unravel-variance.i:53.
 [eva] using specification for function printf2
 [eva] Done for function printf2
 [eva:alarm] unravel-variance.i:54: Warning: 
@@ -146,10 +146,10 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[eva] computing for function printf3 <- main.
-  Called from unravel-variance.i:54.
 [kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3, generating default assigns from the prototype
+[eva] computing for function printf3 <- main.
+  Called from unravel-variance.i:54.
 [eva] using specification for function printf3
 [eva] Done for function printf3
 [eva:alarm] unravel-variance.i:55: Warning: 
@@ -158,10 +158,10 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[eva] computing for function printf4 <- main.
-  Called from unravel-variance.i:55.
 [kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4, generating default assigns from the prototype
+[eva] computing for function printf4 <- main.
+  Called from unravel-variance.i:55.
 [eva] using specification for function printf4
 [eva] Done for function printf4
 [eva:alarm] unravel-variance.i:56: Warning: 
@@ -170,10 +170,10 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[eva] computing for function printf5 <- main.
-  Called from unravel-variance.i:56.
 [kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5, generating default assigns from the prototype
+[eva] computing for function printf5 <- main.
+  Called from unravel-variance.i:56.
 [eva] using specification for function printf5
 [eva] Done for function printf5
 [eva] Recording results for main
diff --git a/tests/slicing/oracle/unravel-variance.1.res.oracle b/tests/slicing/oracle/unravel-variance.1.res.oracle
index dc3d6684c28ce34fe7cc00e67d7f4cd799a18957..bccf37024ec5c6c98c0e662e8132bfef551b400f 100644
--- a/tests/slicing/oracle/unravel-variance.1.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.1.res.oracle
@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function scanf <- main.
-  Called from unravel-variance.i:31.
 [kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf, generating default assigns from the prototype
+[eva] computing for function scanf <- main.
+  Called from unravel-variance.i:31.
 [eva] using specification for function scanf
 [eva] Done for function scanf
 [eva:alarm] unravel-variance.i:32: Warning: 
@@ -122,10 +122,10 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[eva] computing for function printf1 <- main.
-  Called from unravel-variance.i:52.
 [kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1, generating default assigns from the prototype
+[eva] computing for function printf1 <- main.
+  Called from unravel-variance.i:52.
 [eva] using specification for function printf1
 [eva] Done for function printf1
 [eva:alarm] unravel-variance.i:53: Warning: 
@@ -134,10 +134,10 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[eva] computing for function printf2 <- main.
-  Called from unravel-variance.i:53.
 [kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2, generating default assigns from the prototype
+[eva] computing for function printf2 <- main.
+  Called from unravel-variance.i:53.
 [eva] using specification for function printf2
 [eva] Done for function printf2
 [eva:alarm] unravel-variance.i:54: Warning: 
@@ -146,10 +146,10 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[eva] computing for function printf3 <- main.
-  Called from unravel-variance.i:54.
 [kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3, generating default assigns from the prototype
+[eva] computing for function printf3 <- main.
+  Called from unravel-variance.i:54.
 [eva] using specification for function printf3
 [eva] Done for function printf3
 [eva:alarm] unravel-variance.i:55: Warning: 
@@ -158,10 +158,10 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[eva] computing for function printf4 <- main.
-  Called from unravel-variance.i:55.
 [kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4, generating default assigns from the prototype
+[eva] computing for function printf4 <- main.
+  Called from unravel-variance.i:55.
 [eva] using specification for function printf4
 [eva] Done for function printf4
 [eva:alarm] unravel-variance.i:56: Warning: 
@@ -170,10 +170,10 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[eva] computing for function printf5 <- main.
-  Called from unravel-variance.i:56.
 [kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5, generating default assigns from the prototype
+[eva] computing for function printf5 <- main.
+  Called from unravel-variance.i:56.
 [eva] using specification for function printf5
 [eva] Done for function printf5
 [eva] Recording results for main
diff --git a/tests/slicing/oracle/unravel-variance.2.res.oracle b/tests/slicing/oracle/unravel-variance.2.res.oracle
index 26c8a8589de6636f9d9be36d24a787717ecfbc59..ae3068ba0adbefe5d89ad12876b135c664d0df2f 100644
--- a/tests/slicing/oracle/unravel-variance.2.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.2.res.oracle
@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function scanf <- main.
-  Called from unravel-variance.i:31.
 [kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf, generating default assigns from the prototype
+[eva] computing for function scanf <- main.
+  Called from unravel-variance.i:31.
 [eva] using specification for function scanf
 [eva] Done for function scanf
 [eva:alarm] unravel-variance.i:32: Warning: 
@@ -122,10 +122,10 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[eva] computing for function printf1 <- main.
-  Called from unravel-variance.i:52.
 [kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1, generating default assigns from the prototype
+[eva] computing for function printf1 <- main.
+  Called from unravel-variance.i:52.
 [eva] using specification for function printf1
 [eva] Done for function printf1
 [eva:alarm] unravel-variance.i:53: Warning: 
@@ -134,10 +134,10 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[eva] computing for function printf2 <- main.
-  Called from unravel-variance.i:53.
 [kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2, generating default assigns from the prototype
+[eva] computing for function printf2 <- main.
+  Called from unravel-variance.i:53.
 [eva] using specification for function printf2
 [eva] Done for function printf2
 [eva:alarm] unravel-variance.i:54: Warning: 
@@ -146,10 +146,10 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[eva] computing for function printf3 <- main.
-  Called from unravel-variance.i:54.
 [kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3, generating default assigns from the prototype
+[eva] computing for function printf3 <- main.
+  Called from unravel-variance.i:54.
 [eva] using specification for function printf3
 [eva] Done for function printf3
 [eva:alarm] unravel-variance.i:55: Warning: 
@@ -158,10 +158,10 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[eva] computing for function printf4 <- main.
-  Called from unravel-variance.i:55.
 [kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4, generating default assigns from the prototype
+[eva] computing for function printf4 <- main.
+  Called from unravel-variance.i:55.
 [eva] using specification for function printf4
 [eva] Done for function printf4
 [eva:alarm] unravel-variance.i:56: Warning: 
@@ -170,10 +170,10 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[eva] computing for function printf5 <- main.
-  Called from unravel-variance.i:56.
 [kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5, generating default assigns from the prototype
+[eva] computing for function printf5 <- main.
+  Called from unravel-variance.i:56.
 [eva] using specification for function printf5
 [eva] Done for function printf5
 [eva] Recording results for main
diff --git a/tests/slicing/oracle/unravel-variance.3.res.oracle b/tests/slicing/oracle/unravel-variance.3.res.oracle
index 4b3f186ea752e779cb84de981e9330c7ab16c4ef..2664ab39dcca01a8670d4684ab2a06e4aa112266 100644
--- a/tests/slicing/oracle/unravel-variance.3.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.3.res.oracle
@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function scanf <- main.
-  Called from unravel-variance.i:31.
 [kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf, generating default assigns from the prototype
+[eva] computing for function scanf <- main.
+  Called from unravel-variance.i:31.
 [eva] using specification for function scanf
 [eva] Done for function scanf
 [eva:alarm] unravel-variance.i:32: Warning: 
@@ -122,10 +122,10 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[eva] computing for function printf1 <- main.
-  Called from unravel-variance.i:52.
 [kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1, generating default assigns from the prototype
+[eva] computing for function printf1 <- main.
+  Called from unravel-variance.i:52.
 [eva] using specification for function printf1
 [eva] Done for function printf1
 [eva:alarm] unravel-variance.i:53: Warning: 
@@ -134,10 +134,10 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[eva] computing for function printf2 <- main.
-  Called from unravel-variance.i:53.
 [kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2, generating default assigns from the prototype
+[eva] computing for function printf2 <- main.
+  Called from unravel-variance.i:53.
 [eva] using specification for function printf2
 [eva] Done for function printf2
 [eva:alarm] unravel-variance.i:54: Warning: 
@@ -146,10 +146,10 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[eva] computing for function printf3 <- main.
-  Called from unravel-variance.i:54.
 [kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3, generating default assigns from the prototype
+[eva] computing for function printf3 <- main.
+  Called from unravel-variance.i:54.
 [eva] using specification for function printf3
 [eva] Done for function printf3
 [eva:alarm] unravel-variance.i:55: Warning: 
@@ -158,10 +158,10 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[eva] computing for function printf4 <- main.
-  Called from unravel-variance.i:55.
 [kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4, generating default assigns from the prototype
+[eva] computing for function printf4 <- main.
+  Called from unravel-variance.i:55.
 [eva] using specification for function printf4
 [eva] Done for function printf4
 [eva:alarm] unravel-variance.i:56: Warning: 
@@ -170,10 +170,10 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[eva] computing for function printf5 <- main.
-  Called from unravel-variance.i:56.
 [kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5, generating default assigns from the prototype
+[eva] computing for function printf5 <- main.
+  Called from unravel-variance.i:56.
 [eva] using specification for function printf5
 [eva] Done for function printf5
 [eva] Recording results for main
diff --git a/tests/slicing/oracle/unravel-variance.4.res.oracle b/tests/slicing/oracle/unravel-variance.4.res.oracle
index df31e40bcc05c85b466e8971860f9ba3698a2b6d..82f8aced73733f8aeccb0c5b8bbb6147357b7f2c 100644
--- a/tests/slicing/oracle/unravel-variance.4.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.4.res.oracle
@@ -5,10 +5,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function scanf <- main.
-  Called from unravel-variance.i:31.
 [kernel:annot:missing-spec] unravel-variance.i:31: Warning: 
   Neither code nor specification for function scanf, generating default assigns from the prototype
+[eva] computing for function scanf <- main.
+  Called from unravel-variance.i:31.
 [eva] using specification for function scanf
 [eva] Done for function scanf
 [eva:alarm] unravel-variance.i:32: Warning: 
@@ -122,10 +122,10 @@
 [eva:alarm] unravel-variance.i:52: Warning: 
   overflow in conversion from floating-point to integer.
   assert var2 < 2147483648;
-[eva] computing for function printf1 <- main.
-  Called from unravel-variance.i:52.
 [kernel:annot:missing-spec] unravel-variance.i:52: Warning: 
   Neither code nor specification for function printf1, generating default assigns from the prototype
+[eva] computing for function printf1 <- main.
+  Called from unravel-variance.i:52.
 [eva] using specification for function printf1
 [eva] Done for function printf1
 [eva:alarm] unravel-variance.i:53: Warning: 
@@ -134,10 +134,10 @@
 [eva:alarm] unravel-variance.i:53: Warning: 
   overflow in conversion from floating-point to integer.
   assert var3 < 2147483648;
-[eva] computing for function printf2 <- main.
-  Called from unravel-variance.i:53.
 [kernel:annot:missing-spec] unravel-variance.i:53: Warning: 
   Neither code nor specification for function printf2, generating default assigns from the prototype
+[eva] computing for function printf2 <- main.
+  Called from unravel-variance.i:53.
 [eva] using specification for function printf2
 [eva] Done for function printf2
 [eva:alarm] unravel-variance.i:54: Warning: 
@@ -146,10 +146,10 @@
 [eva:alarm] unravel-variance.i:54: Warning: 
   overflow in conversion from floating-point to integer.
   assert var4 < 2147483648;
-[eva] computing for function printf3 <- main.
-  Called from unravel-variance.i:54.
 [kernel:annot:missing-spec] unravel-variance.i:54: Warning: 
   Neither code nor specification for function printf3, generating default assigns from the prototype
+[eva] computing for function printf3 <- main.
+  Called from unravel-variance.i:54.
 [eva] using specification for function printf3
 [eva] Done for function printf3
 [eva:alarm] unravel-variance.i:55: Warning: 
@@ -158,10 +158,10 @@
 [eva:alarm] unravel-variance.i:55: Warning: 
   overflow in conversion from floating-point to integer.
   assert var5 < 2147483648;
-[eva] computing for function printf4 <- main.
-  Called from unravel-variance.i:55.
 [kernel:annot:missing-spec] unravel-variance.i:55: Warning: 
   Neither code nor specification for function printf4, generating default assigns from the prototype
+[eva] computing for function printf4 <- main.
+  Called from unravel-variance.i:55.
 [eva] using specification for function printf4
 [eva] Done for function printf4
 [eva:alarm] unravel-variance.i:56: Warning: 
@@ -170,10 +170,10 @@
 [eva:alarm] unravel-variance.i:56: Warning: 
   overflow in conversion from floating-point to integer.
   assert var1 < 2147483648;
-[eva] computing for function printf5 <- main.
-  Called from unravel-variance.i:56.
 [kernel:annot:missing-spec] unravel-variance.i:56: Warning: 
   Neither code nor specification for function printf5, generating default assigns from the prototype
+[eva] computing for function printf5 <- main.
+  Called from unravel-variance.i:56.
 [eva] using specification for function printf5
 [eva] Done for function printf5
 [eva] Recording results for main
diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle
index d20a0522f6731e4af50c9f68039d8b7e92b73173..6d5dd41248b88c5806c51f48e48a27da9a68563c 100644
--- a/tests/slicing/oracle/variadic.0.res.oracle
+++ b/tests/slicing/oracle/variadic.0.res.oracle
@@ -8,10 +8,10 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[eva] computing for function lib_f <- f1 <- main.
-  Called from tests/pdg/variadic.c:23.
 [kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] computing for function lib_f <- f1 <- main.
+  Called from tests/pdg/variadic.c:23.
 [eva] using specification for function lib_f
 [eva] Done for function lib_f
 [eva] Recording results for f1
diff --git a/tests/slicing/oracle/variadic.1.res.oracle b/tests/slicing/oracle/variadic.1.res.oracle
index 262fef8cb4b2cae2bcc0badd9938d0d54e6b5030..caccc9ace2f1209f70922e257a64c7dc11bc39b1 100644
--- a/tests/slicing/oracle/variadic.1.res.oracle
+++ b/tests/slicing/oracle/variadic.1.res.oracle
@@ -8,10 +8,10 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[eva] computing for function lib_f <- f1 <- main.
-  Called from tests/pdg/variadic.c:23.
 [kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] computing for function lib_f <- f1 <- main.
+  Called from tests/pdg/variadic.c:23.
 [eva] using specification for function lib_f
 [eva] Done for function lib_f
 [eva] Recording results for f1
diff --git a/tests/slicing/oracle/variadic.2.res.oracle b/tests/slicing/oracle/variadic.2.res.oracle
index 84212502c0317c64bee00c339a3c38acec3bc55a..fae36df0bab812afb90e041377ab3c21422c5079 100644
--- a/tests/slicing/oracle/variadic.2.res.oracle
+++ b/tests/slicing/oracle/variadic.2.res.oracle
@@ -8,10 +8,10 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[eva] computing for function lib_f <- f1 <- main.
-  Called from tests/pdg/variadic.c:23.
 [kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] computing for function lib_f <- f1 <- main.
+  Called from tests/pdg/variadic.c:23.
 [eva] using specification for function lib_f
 [eva] Done for function lib_f
 [eva] Recording results for f1
diff --git a/tests/slicing/oracle/variadic.3.res.oracle b/tests/slicing/oracle/variadic.3.res.oracle
index 72db5708548e320f6d5aa039ec9c80861fbe6132..335a7f4c9736f14e2d65caa9c36fc125ded46262 100644
--- a/tests/slicing/oracle/variadic.3.res.oracle
+++ b/tests/slicing/oracle/variadic.3.res.oracle
@@ -8,10 +8,10 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[eva] computing for function lib_f <- f1 <- main.
-  Called from tests/pdg/variadic.c:23.
 [kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] computing for function lib_f <- f1 <- main.
+  Called from tests/pdg/variadic.c:23.
 [eva] using specification for function lib_f
 [eva] Done for function lib_f
 [eva] Recording results for f1
diff --git a/tests/slicing/oracle/variadic.4.res.oracle b/tests/slicing/oracle/variadic.4.res.oracle
index 72db5708548e320f6d5aa039ec9c80861fbe6132..335a7f4c9736f14e2d65caa9c36fc125ded46262 100644
--- a/tests/slicing/oracle/variadic.4.res.oracle
+++ b/tests/slicing/oracle/variadic.4.res.oracle
@@ -8,10 +8,10 @@
   
 [eva] computing for function f1 <- main.
   Called from tests/pdg/variadic.c:37.
-[eva] computing for function lib_f <- f1 <- main.
-  Called from tests/pdg/variadic.c:23.
 [kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning: 
   Neither code nor specification for function lib_f, generating default assigns from the prototype
+[eva] computing for function lib_f <- f1 <- main.
+  Called from tests/pdg/variadic.c:23.
 [eva] using specification for function lib_f
 [eva] Done for function lib_f
 [eva] Recording results for f1
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index b514401262ed3be20fa52868c0d3e5fba91a910e..b5d83bb8ac73533c87e09bfe5e6f2580b7ddec63 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -12,10 +12,10 @@
   s1 ∈ {0}
   si[0..1] ∈ {0}
   so[0..1] ∈ {0}
-[eva] computing for function init <- main_init.
-  Called from bts334.i:66.
 [kernel] bts334.i:66: Warning: 
   No code nor explicit assigns clause for function init, generating default assigns from the specification
+[eva] computing for function init <- main_init.
+  Called from bts334.i:66.
 [eva] using specification for function init
 [eva] bts334.i:61: Warning: 
   no 'assigns \result \from ...' clause specified for function init
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 14a05eb9249e23f0cb01f74180123ac88740d85f..77e6867d86f7469c165f58830a95983a72c8330b 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -12,10 +12,10 @@
   s1 ∈ {0}
   si[0..1] ∈ {0}
   so[0..1] ∈ {0}
-[eva] computing for function init <- main_init.
-  Called from bts334.i:66.
 [kernel] bts334.i:66: Warning: 
   No code nor explicit assigns clause for function init, generating default assigns from the specification
+[eva] computing for function init <- main_init.
+  Called from bts334.i:66.
 [eva] using specification for function init
 [eva] bts334.i:61: Warning: 
   no 'assigns \result \from ...' clause specified for function init
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index 46154e7440ca51b5e742d0548aad9600d1ff5c1a..2f276f5ff609c6532b77d47ce878fe364e49a637 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -11,10 +11,10 @@
   s1 ∈ {0}
   si[0..1] ∈ {0}
   so[0..1] ∈ {0}
-[eva] computing for function init <- main_init.
-  Called from bts334.i:66.
 [kernel] bts334.i:66: Warning: 
   No code nor explicit assigns clause for function init, generating default assigns from the specification
+[eva] computing for function init <- main_init.
+  Called from bts334.i:66.
 [eva] using specification for function init
 [eva] bts334.i:61: Warning: 
   no 'assigns \result \from ...' clause specified for function init
diff --git a/tests/sparecode/oracle/intra.0.res.oracle b/tests/sparecode/oracle/intra.0.res.oracle
index 519649a8fa7de78c626161d6eac01aa5db2a7070..14470158edb9c522b23ca615c210dc09c4ce4179 100644
--- a/tests/sparecode/oracle/intra.0.res.oracle
+++ b/tests/sparecode/oracle/intra.0.res.oracle
@@ -49,10 +49,10 @@
   Called from intra.i:88.
 [eva] Recording results for assign
 [eva] Done for function assign
-[eva] computing for function stop <- main.
-  Called from intra.i:91.
 [kernel:annot:missing-spec] intra.i:91: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- main.
+  Called from intra.i:91.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for main
diff --git a/tests/sparecode/oracle/intra.1.res.oracle b/tests/sparecode/oracle/intra.1.res.oracle
index 15c053d475d926a938530b72798d70253b050218..3715b90db0f8366641498b59675fc0f0b95f6a29 100644
--- a/tests/sparecode/oracle/intra.1.res.oracle
+++ b/tests/sparecode/oracle/intra.1.res.oracle
@@ -48,10 +48,10 @@
   Called from intra.i:88.
 [eva] Recording results for assign
 [eva] Done for function assign
-[eva] computing for function stop <- main.
-  Called from intra.i:91.
 [kernel:annot:missing-spec] intra.i:91: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- main.
+  Called from intra.i:91.
 [eva] using specification for function stop
 [eva] Done for function stop
 [eva] Recording results for main
diff --git a/tests/sparecode/oracle/top.1.res.oracle b/tests/sparecode/oracle/top.1.res.oracle
index 1d348f16c914d0926d755228321df4bc5bb06970..4f6f7329b0c8ab48220792237e262e3c14ab4a1d 100644
--- a/tests/sparecode/oracle/top.1.res.oracle
+++ b/tests/sparecode/oracle/top.1.res.oracle
@@ -16,10 +16,10 @@
 [eva] Done for function main_top
 [eva] computing for function not_used_in_main_top <- main_call_top.
   Called from top.i:27.
-[eva] computing for function print <- not_used_in_main_top <- main_call_top.
-  Called from top.i:10.
 [kernel:annot:missing-spec] top.i:10: Warning: 
   Neither code nor specification for function print, generating default assigns from the prototype
+[eva] computing for function print <- not_used_in_main_top <- main_call_top.
+  Called from top.i:10.
 [eva] using specification for function print
 [eva] Done for function print
 [eva] Recording results for not_used_in_main_top
diff --git a/tests/spec/oracle/assigns_void.1.res.oracle b/tests/spec/oracle/assigns_void.1.res.oracle
index fa59eca7f82e704ec2f3575b27813a3345af91d3..fb9a8b2d5baf925d7c65b0220e3dc581cc224341 100644
--- a/tests/spec/oracle/assigns_void.1.res.oracle
+++ b/tests/spec/oracle/assigns_void.1.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- g.
-  Called from assigns_void.c:11.
 [kernel:annot:missing-spec] assigns_void.c:11: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- g.
+  Called from assigns_void.c:11.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for g
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index fc787492fd03594f6fd0695eb22d300a00846d47..1bdb53cd80638ca67a3459df8cda1068e0b917d8 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -102,22 +102,22 @@
 [eva] using specification for function ff3
 [eva] assigns.i:68: Warning: no \from part for clause 'assigns y1, y3;'
 [eva] Done for function ff3
-[eva] computing for function ff4 <- main2 <- main.
-  Called from assigns.i:79.
 [kernel:annot:missing-spec] assigns.i:79: Warning: 
   Neither code nor specification for function ff4, generating default assigns from the prototype
+[eva] computing for function ff4 <- main2 <- main.
+  Called from assigns.i:79.
 [eva] using specification for function ff4
 [eva] Done for function ff4
-[eva] computing for function ff5 <- main2 <- main.
-  Called from assigns.i:80.
 [kernel:annot:missing-spec] assigns.i:80: Warning: 
   Neither code nor specification for function ff5, generating default assigns from the prototype
+[eva] computing for function ff5 <- main2 <- main.
+  Called from assigns.i:80.
 [eva] using specification for function ff5
 [eva] Done for function ff5
-[eva] computing for function ff2 <- main2 <- main.
-  Called from assigns.i:82.
 [kernel:annot:missing-spec] assigns.i:82: Warning: 
   Neither code nor specification for function ff2, generating default assigns from the prototype
+[eva] computing for function ff2 <- main2 <- main.
+  Called from assigns.i:82.
 [eva] using specification for function ff2
 [eva] Done for function ff2
 [eva] computing for function ff2_bis <- main2 <- main.
@@ -130,10 +130,10 @@
   pointer comparison. assert \pointer_comparable((void *)p, (void *)(&x));
 [eva] Recording results for main2
 [eva] Done for function main2
-[eva] computing for function main3 <- main.
-  Called from assigns.i:112.
 [kernel:annot:missing-spec] assigns.i:112: Warning: 
   Neither code nor specification for function main3, generating default assigns from the prototype
+[eva] computing for function main3 <- main.
+  Called from assigns.i:112.
 [eva] using specification for function main3
 [eva] Done for function main3
 [eva] computing for function main4 <- main.
diff --git a/tests/value/oracle/assigns_from.res.oracle b/tests/value/oracle/assigns_from.res.oracle
index f8e6dc8fe59c3acfd7bc4d6557869917bf83f6cc..0149986d5d772be27b59719f380ba7ccead5db0d 100644
--- a/tests/value/oracle/assigns_from.res.oracle
+++ b/tests/value/oracle/assigns_from.res.oracle
@@ -186,10 +186,10 @@
 [eva] Done for function main9
 [eva] computing for function main10 <- main.
   Called from assigns_from.i:244.
-[eva] computing for function c <- main10 <- main.
-  Called from assigns_from.i:152.
 [kernel:annot:missing-spec] assigns_from.i:152: Warning: 
   Neither code nor specification for function c, generating default assigns from the prototype
+[eva] computing for function c <- main10 <- main.
+  Called from assigns_from.i:152.
 [eva] using specification for function c
 [eva] Done for function c
 [eva] assigns_from.i:152: starting to merge loop iterations
diff --git a/tests/value/oracle/automalloc.res.oracle b/tests/value/oracle/automalloc.res.oracle
index 5f9f032426501548404c5a1baf17b3e9851b9cea..1ead5d50a962fa7fc3d5efdaf50f763f9c8363dd 100644
--- a/tests/value/oracle/automalloc.res.oracle
+++ b/tests/value/oracle/automalloc.res.oracle
@@ -4,16 +4,16 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function malloc <- main.
-  Called from automalloc.i:14.
 [kernel:annot:missing-spec] automalloc.i:14: Warning: 
   Neither code nor specification for function malloc, generating default assigns from the prototype
+[eva] computing for function malloc <- main.
+  Called from automalloc.i:14.
 [eva] using specification for function malloc
 [eva] Done for function malloc
-[eva] computing for function realloc <- main.
-  Called from automalloc.i:15.
 [kernel:annot:missing-spec] automalloc.i:15: Warning: 
   Neither code nor specification for function realloc, generating default assigns from the prototype
+[eva] computing for function realloc <- main.
+  Called from automalloc.i:15.
 [eva] using specification for function realloc
 [eva] Done for function realloc
 [eva:alarm] automalloc.i:17: Warning: 
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 7971f0399f312076281f01f09242f442f0027828..504e982e8951bf6f1ea5d40e294f447aa340583d 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -337,10 +337,10 @@
 [eva] Done for function test_assigns2
 [eva] computing for function test_small1 <- main.
   Called from behaviors1.i:649.
-[eva] computing for function f3 <- test_small1 <- main.
-  Called from behaviors1.i:506.
 [kernel] behaviors1.i:506: Warning: 
   No code nor implicit assigns clause for function f3, generating default assigns from the prototype
+[eva] computing for function f3 <- test_small1 <- main.
+  Called from behaviors1.i:506.
 [eva] using specification for function f3
 [eva:alarm] behaviors1.i:506: Warning: 
   function f3: precondition got status unknown.
@@ -351,10 +351,10 @@
 [eva] Done for function test_small1
 [eva] computing for function test_small2 <- main.
   Called from behaviors1.i:650.
-[eva] computing for function f4 <- test_small2 <- main.
-  Called from behaviors1.i:521.
 [kernel] behaviors1.i:521: Warning: 
   No code nor implicit assigns clause for function f4, generating default assigns from the prototype
+[eva] computing for function f4 <- test_small2 <- main.
+  Called from behaviors1.i:521.
 [eva] using specification for function f4
 [eva:alarm] behaviors1.i:521: Warning: 
   function f4: precondition got status unknown.
@@ -369,30 +369,30 @@
 [eva] Done for function test_small2
 [eva] computing for function test_small3 <- main.
   Called from behaviors1.i:651.
-[eva] computing for function f5 <- test_small3 <- main.
-  Called from behaviors1.i:534.
 [kernel] behaviors1.i:534: Warning: 
   No code nor implicit assigns clause for function f5, generating default assigns from the prototype
+[eva] computing for function f5 <- test_small3 <- main.
+  Called from behaviors1.i:534.
 [eva] using specification for function f5
 [eva] Done for function f5
 [eva] Recording results for test_small3
 [eva] Done for function test_small3
 [eva] computing for function test_small4 <- main.
   Called from behaviors1.i:652.
-[eva] computing for function f6 <- test_small4 <- main.
-  Called from behaviors1.i:548.
 [kernel] behaviors1.i:548: Warning: 
   No code nor implicit assigns clause for function f6, generating default assigns from the prototype
+[eva] computing for function f6 <- test_small4 <- main.
+  Called from behaviors1.i:548.
 [eva] using specification for function f6
 [eva] Done for function f6
 [eva] Recording results for test_small4
 [eva] Done for function test_small4
 [eva] computing for function test_small5 <- main.
   Called from behaviors1.i:653.
-[eva] computing for function f7 <- test_small5 <- main.
-  Called from behaviors1.i:561.
 [kernel] behaviors1.i:561: Warning: 
   No code nor implicit assigns clause for function f7, generating default assigns from the prototype
+[eva] computing for function f7 <- test_small5 <- main.
+  Called from behaviors1.i:561.
 [eva] using specification for function f7
 [eva:alarm] behaviors1.i:561: Warning: 
   function f7: precondition got status unknown.
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index c38d611eb27b9e53749960ed74fecb30398cad52..506aa9ec93d5aee5a0993e625296d443a4ae893b 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -99,10 +99,10 @@
   locals {v} escaping the scope of main_old through h
 [eva] computing for function imprecise_bts_1671 <- main.
   Called from bitfield.i:165.
-[eva] computing for function leaf <- imprecise_bts_1671 <- main.
-  Called from bitfield.i:70.
 [kernel:annot:missing-spec] bitfield.i:70: Warning: 
   Neither code nor specification for function leaf, generating default assigns from the prototype
+[eva] computing for function leaf <- imprecise_bts_1671 <- main.
+  Called from bitfield.i:70.
 [eva] using specification for function leaf
 [eva] Done for function leaf
 [eva] bitfield.i:71: 
diff --git a/tests/value/oracle/bts0506.0.res.oracle b/tests/value/oracle/bts0506.0.res.oracle
index b5cfd130cebfdc88fd3e6e5a90532d3798ede1ad..994c9d1fe3eb2e210b00fcbf107dd8bf76a14f61 100644
--- a/tests/value/oracle/bts0506.0.res.oracle
+++ b/tests/value/oracle/bts0506.0.res.oracle
@@ -10,10 +10,10 @@
 [eva] Done for function f
 [eva] computing for function main2 <- main.
   Called from bts0506.i:49.
-[eva] computing for function f1 <- main2 <- main.
-  Called from bts0506.i:15.
 [kernel:annot:missing-spec] bts0506.i:15: Warning: 
   Neither code nor specification for function f1, generating default assigns from the prototype
+[eva] computing for function f1 <- main2 <- main.
+  Called from bts0506.i:15.
 [eva] using specification for function f1
 [eva] Done for function f1
 [eva] computing for function f1 <- main2 <- main.
@@ -25,10 +25,10 @@
 [eva] computing for function f1 <- main2 <- main.
   Called from bts0506.i:18.
 [eva] Done for function f1
-[eva] computing for function f2 <- main2 <- main.
-  Called from bts0506.i:20.
 [kernel:annot:missing-spec] bts0506.i:20: Warning: 
   Neither code nor specification for function f2, generating default assigns from the prototype
+[eva] computing for function f2 <- main2 <- main.
+  Called from bts0506.i:20.
 [eva] using specification for function f2
 [eva] Done for function f2
 [eva] computing for function f2 <- main2 <- main.
@@ -37,19 +37,19 @@
 [eva] computing for function f2 <- main2 <- main.
   Called from bts0506.i:22.
 [eva] Done for function f2
-[eva] computing for function f3 <- main2 <- main.
-  Called from bts0506.i:24.
 [kernel:annot:missing-spec] bts0506.i:24: Warning: 
   Neither code nor specification for function f3, generating default assigns from the prototype
+[eva] computing for function f3 <- main2 <- main.
+  Called from bts0506.i:24.
 [eva] using specification for function f3
 [eva] Done for function f3
 [eva] computing for function f3 <- main2 <- main.
   Called from bts0506.i:25.
 [eva] Done for function f3
-[eva] computing for function f4 <- main2 <- main.
-  Called from bts0506.i:27.
 [kernel:annot:missing-spec] bts0506.i:27: Warning: 
   Neither code nor specification for function f4, generating default assigns from the prototype
+[eva] computing for function f4 <- main2 <- main.
+  Called from bts0506.i:27.
 [eva] using specification for function f4
 [eva] Done for function f4
 [eva:alarm] bts0506.i:27: Warning: 
@@ -61,10 +61,10 @@
 [eva:alarm] bts0506.i:28: Warning: 
   non-finite float value. assert \is_finite(tmp_9);
                           (tmp_9 from f4())
-[eva] computing for function f5 <- main2 <- main.
-  Called from bts0506.i:30.
 [kernel:annot:missing-spec] bts0506.i:30: Warning: 
   Neither code nor specification for function f5, generating default assigns from the prototype
+[eva] computing for function f5 <- main2 <- main.
+  Called from bts0506.i:30.
 [eva] using specification for function f5
 [eva] Done for function f5
 [eva:alarm] bts0506.i:30: Warning: 
@@ -79,10 +79,10 @@
 [eva:alarm] bts0506.i:31: Warning: 
   non-finite double value. assert \is_finite(tmp_11);
                            (tmp_11 from f5())
-[eva] computing for function f6 <- main2 <- main.
-  Called from bts0506.i:33.
 [kernel:annot:missing-spec] bts0506.i:33: Warning: 
   Neither code nor specification for function f6, generating default assigns from the prototype
+[eva] computing for function f6 <- main2 <- main.
+  Called from bts0506.i:33.
 [eva] using specification for function f6
 [eva] Done for function f6
 [eva] computing for function f6 <- main2 <- main.
@@ -91,10 +91,10 @@
 [eva] computing for function f6 <- main2 <- main.
   Called from bts0506.i:35.
 [eva] Done for function f6
-[eva] computing for function f7 <- main2 <- main.
-  Called from bts0506.i:37.
 [kernel:annot:missing-spec] bts0506.i:37: Warning: 
   Neither code nor specification for function f7, generating default assigns from the prototype
+[eva] computing for function f7 <- main2 <- main.
+  Called from bts0506.i:37.
 [eva] using specification for function f7
 [eva] Done for function f7
 [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 188a7a4ff1ad6b4f70cff3036b2edc84b354bd11..18a53ed9fcc536e72cb20026533a90659b788e4b 100644
--- a/tests/value/oracle/bts0506.1.res.oracle
+++ b/tests/value/oracle/bts0506.1.res.oracle
@@ -10,10 +10,10 @@
 [eva] Done for function f
 [eva] computing for function main2 <- main.
   Called from bts0506.i:49.
-[eva] computing for function f1 <- main2 <- main.
-  Called from bts0506.i:15.
 [kernel:annot:missing-spec] bts0506.i:15: Warning: 
   Neither code nor specification for function f1, generating default assigns from the prototype
+[eva] computing for function f1 <- main2 <- main.
+  Called from bts0506.i:15.
 [eva] using specification for function f1
 [eva] Done for function f1
 [eva] computing for function f1 <- main2 <- main.
@@ -25,10 +25,10 @@
 [eva] computing for function f1 <- main2 <- main.
   Called from bts0506.i:18.
 [eva] Done for function f1
-[eva] computing for function f2 <- main2 <- main.
-  Called from bts0506.i:20.
 [kernel:annot:missing-spec] bts0506.i:20: Warning: 
   Neither code nor specification for function f2, generating default assigns from the prototype
+[eva] computing for function f2 <- main2 <- main.
+  Called from bts0506.i:20.
 [eva] using specification for function f2
 [eva] Done for function f2
 [eva] computing for function f2 <- main2 <- main.
@@ -37,19 +37,19 @@
 [eva] computing for function f2 <- main2 <- main.
   Called from bts0506.i:22.
 [eva] Done for function f2
-[eva] computing for function f3 <- main2 <- main.
-  Called from bts0506.i:24.
 [kernel:annot:missing-spec] bts0506.i:24: Warning: 
   Neither code nor specification for function f3, generating default assigns from the prototype
+[eva] computing for function f3 <- main2 <- main.
+  Called from bts0506.i:24.
 [eva] using specification for function f3
 [eva] Done for function f3
 [eva] computing for function f3 <- main2 <- main.
   Called from bts0506.i:25.
 [eva] Done for function f3
-[eva] computing for function f4 <- main2 <- main.
-  Called from bts0506.i:27.
 [kernel:annot:missing-spec] bts0506.i:27: Warning: 
   Neither code nor specification for function f4, generating default assigns from the prototype
+[eva] computing for function f4 <- main2 <- main.
+  Called from bts0506.i:27.
 [eva] using specification for function f4
 [eva] Done for function f4
 [eva] computing for function f4 <- main2 <- main.
@@ -58,10 +58,10 @@
 [eva:alarm] bts0506.i:28: Warning: 
   non-finite float value. assert \is_finite(tmp_9);
                           (tmp_9 from f4())
-[eva] computing for function f5 <- main2 <- main.
-  Called from bts0506.i:30.
 [kernel:annot:missing-spec] bts0506.i:30: Warning: 
   Neither code nor specification for function f5, generating default assigns from the prototype
+[eva] computing for function f5 <- main2 <- main.
+  Called from bts0506.i:30.
 [eva] using specification for function f5
 [eva] Done for function f5
 [eva:alarm] bts0506.i:30: Warning: 
@@ -73,10 +73,10 @@
 [eva] computing for function f5 <- main2 <- main.
   Called from bts0506.i:31.
 [eva] Done for function f5
-[eva] computing for function f6 <- main2 <- main.
-  Called from bts0506.i:33.
 [kernel:annot:missing-spec] bts0506.i:33: Warning: 
   Neither code nor specification for function f6, generating default assigns from the prototype
+[eva] computing for function f6 <- main2 <- main.
+  Called from bts0506.i:33.
 [eva] using specification for function f6
 [eva] Done for function f6
 [eva] computing for function f6 <- main2 <- main.
@@ -85,10 +85,10 @@
 [eva] computing for function f6 <- main2 <- main.
   Called from bts0506.i:35.
 [eva] Done for function f6
-[eva] computing for function f7 <- main2 <- main.
-  Called from bts0506.i:37.
 [kernel:annot:missing-spec] bts0506.i:37: Warning: 
   Neither code nor specification for function f7, generating default assigns from the prototype
+[eva] computing for function f7 <- main2 <- main.
+  Called from bts0506.i:37.
 [eva] using specification for function f7
 [eva] Done for function f7
 [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 bac86646e418b0526aff9c3c4e184dda31cb45f5..f470f869eec6200f49cb7ef0940e6982ff080a86 100644
--- a/tests/value/oracle/bug0223.0.res.oracle
+++ b/tests/value/oracle/bug0223.0.res.oracle
@@ -7,10 +7,10 @@
   ch2 ∈ {{ NULL ; &S_ch2[0] }}
   S_ch1[0..1] ∈ [--..--]
   S_ch2[0..1] ∈ [--..--]
-[eva] computing for function F <- main.
-  Called from bug0223.i:33.
 [kernel:annot:missing-spec] bug0223.i:33: Warning: 
   Neither code nor specification for function F, generating default assigns from the prototype
+[eva] computing for function F <- main.
+  Called from bug0223.i:33.
 [eva] using specification for function F
 [eva] Done for function F
 [eva] computing for function F <- main.
@@ -18,10 +18,10 @@
 [eva] Done for function F
 [eva] computing for function h2 <- main.
   Called from bug0223.i:35.
-[eva] computing for function my_strcnmp <- h2 <- main.
-  Called from bug0223.i:16.
 [kernel:annot:missing-spec] bug0223.i:16: Warning: 
   Neither code nor specification for function my_strcnmp, generating default assigns from the prototype
+[eva] computing for function my_strcnmp <- h2 <- main.
+  Called from bug0223.i:16.
 [eva] using specification for function my_strcnmp
 [eva] Done for function my_strcnmp
 [eva] Recording results for h2
diff --git a/tests/value/oracle/bug0223.1.res.oracle b/tests/value/oracle/bug0223.1.res.oracle
index bac86646e418b0526aff9c3c4e184dda31cb45f5..f470f869eec6200f49cb7ef0940e6982ff080a86 100644
--- a/tests/value/oracle/bug0223.1.res.oracle
+++ b/tests/value/oracle/bug0223.1.res.oracle
@@ -7,10 +7,10 @@
   ch2 ∈ {{ NULL ; &S_ch2[0] }}
   S_ch1[0..1] ∈ [--..--]
   S_ch2[0..1] ∈ [--..--]
-[eva] computing for function F <- main.
-  Called from bug0223.i:33.
 [kernel:annot:missing-spec] bug0223.i:33: Warning: 
   Neither code nor specification for function F, generating default assigns from the prototype
+[eva] computing for function F <- main.
+  Called from bug0223.i:33.
 [eva] using specification for function F
 [eva] Done for function F
 [eva] computing for function F <- main.
@@ -18,10 +18,10 @@
 [eva] Done for function F
 [eva] computing for function h2 <- main.
   Called from bug0223.i:35.
-[eva] computing for function my_strcnmp <- h2 <- main.
-  Called from bug0223.i:16.
 [kernel:annot:missing-spec] bug0223.i:16: Warning: 
   Neither code nor specification for function my_strcnmp, generating default assigns from the prototype
+[eva] computing for function my_strcnmp <- h2 <- main.
+  Called from bug0223.i:16.
 [eva] using specification for function my_strcnmp
 [eva] Done for function my_strcnmp
 [eva] Recording results for h2
diff --git a/tests/value/oracle/bug_023.res.oracle b/tests/value/oracle/bug_023.res.oracle
index 4170a126f4f784887c14b7e6afe81d850c345d88..a73637c9d9e3cbccb926f02d4c749d7f3499f05d 100644
--- a/tests/value/oracle/bug_023.res.oracle
+++ b/tests/value/oracle/bug_023.res.oracle
@@ -5,10 +5,10 @@
 [eva:initial-state] Values of globals at initialization
   i ∈ {0}
   x ∈ {0}
-[eva] computing for function f <- main.
-  Called from bug_023.i:8.
 [kernel:annot:missing-spec] bug_023.i:8: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from bug_023.i:8.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/value/oracle/call.res.oracle b/tests/value/oracle/call.res.oracle
index c79671e10e0b786cb0d37ab49747a34f1aee4283..90128fff00c1c50370d2d1ca961152171c50b12d 100644
--- a/tests/value/oracle/call.res.oracle
+++ b/tests/value/oracle/call.res.oracle
@@ -11,17 +11,17 @@
 [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;
-[eva] computing for function leaf_fun_int <- main.
-  Called from call.i:19.
 [kernel:annot:missing-spec] call.i:19: Warning: 
   Neither code nor specification for function leaf_fun_int, generating default assigns from the prototype
+[eva] computing for function leaf_fun_int <- main.
+  Called from call.i:19.
 [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);
-[eva] computing for function leaf_fun_charp <- main.
-  Called from call.i:20.
 [kernel:annot:missing-spec] call.i:20: Warning: 
   Neither code nor specification for function leaf_fun_charp, generating default assigns from the prototype
+[eva] computing for function leaf_fun_charp <- main.
+  Called from call.i:20.
 [eva] using specification for function leaf_fun_charp
 [eva] Done for function leaf_fun_charp
 [eva] call.i:23: starting to merge loop iterations
diff --git a/tests/value/oracle/cond.res.oracle b/tests/value/oracle/cond.res.oracle
index aac8f1c4fa2916879b692a85a75a278e75d918c6..93f3f3d260d87ee3e1f656addc8ba23f990b4974 100644
--- a/tests/value/oracle/cond.res.oracle
+++ b/tests/value/oracle/cond.res.oracle
@@ -39,10 +39,10 @@
   Called from cond.i:20.
 [eva] Recording results for f
 [eva] Done for function f
-[eva] computing for function unknf <- main.
-  Called from cond.i:34.
 [kernel:annot:missing-spec] cond.i:34: Warning: 
   Neither code nor specification for function unknf, generating default assigns from the prototype
+[eva] computing for function unknf <- main.
+  Called from cond.i:34.
 [eva] using specification for function unknf
 [eva] Done for function unknf
 [eva] cond.i:37: Frama_C_show_each_2: {0; 1; 2; 4; 5; 6; 7; 8}
diff --git a/tests/value/oracle/copy_stdin.res.oracle b/tests/value/oracle/copy_stdin.res.oracle
index 318ef12b9de6296c6abd0e296a831f6cda7694f3..d1469e3cccbb423a7b74825f15817b2750aa0ed0 100644
--- a/tests/value/oracle/copy_stdin.res.oracle
+++ b/tests/value/oracle/copy_stdin.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function leaf <- main.
-  Called from copy_stdin.i:4.
 [kernel:annot:missing-spec] copy_stdin.i:4: Warning: 
   Neither code nor specification for function leaf, generating default assigns from the prototype
+[eva] computing for function leaf <- main.
+  Called from copy_stdin.i:4.
 [eva] using specification for function leaf
 [eva] Done for function leaf
 [eva] Recording results for main
diff --git a/tests/value/oracle/empty_struct.6.res.oracle b/tests/value/oracle/empty_struct.6.res.oracle
index 2ef33b093bc9869ac82bdee2fd7f6146603fd8ca..712cbb8faff17c3aa431582feba6a0218a3969e1 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -12,10 +12,10 @@
 [eva] empty_struct.c:99: 
   Assigning imprecise value to r.
   The imprecision originates from Library function {empty_struct.c:99}
-[eva] computing for function g <- main4.
-  Called from empty_struct.c:100.
 [kernel:annot:missing-spec] empty_struct.c:100: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main4.
+  Called from empty_struct.c:100.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for main4
diff --git a/tests/value/oracle/f1.res.oracle b/tests/value/oracle/f1.res.oracle
index ea4068132c6e65355819af6b38ab7b1736130154..4b59de37098e33a310f277984b32aedd97862d2b 100644
--- a/tests/value/oracle/f1.res.oracle
+++ b/tests/value/oracle/f1.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- main.
-  Called from f1.i:5.
 [kernel:annot:missing-spec] f1.i:5: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from f1.i:5.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/value/oracle/false.res.oracle b/tests/value/oracle/false.res.oracle
index f5540c4e17cb477acc784760bfed84ce693e62e3..25154cc12ce0807639e59e140f7c7c6ea75ede34 100644
--- a/tests/value/oracle/false.res.oracle
+++ b/tests/value/oracle/false.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- main.
-  Called from false.i:18.
 [kernel] false.i:18: Warning: 
   No code nor implicit assigns clause for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from false.i:18.
 [eva] using specification for function f
 [eva:alarm] false.i:18: Warning: 
   function f: precondition i ≡ 1 got status invalid.
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index 2b4d8567b161b16ef2fdbb297b2a194715f46524..101005bed38dbefde5ee3959f528076e5d542172 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -44,10 +44,10 @@
   f_previous ∈ {{ &a }}
 [eva] computing for function f <- main.
   Called from from_call.i:81.
-[eva] computing for function h <- f <- main.
-  Called from from_call.i:20.
 [kernel:annot:missing-spec] from_call.i:20: Warning: 
   Neither code nor specification for function h, generating default assigns from the prototype
+[eva] computing for function h <- f <- main.
+  Called from from_call.i:20.
 [eva] using specification for function h
 [eva] Done for function h
 [eva] computing for function g <- f <- main.
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index 31c4e165ddfb02b9a87a9df61c7bd56ccbb21204..14097263afd44b7dd97bc7fa346a82925f1cd965 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -44,10 +44,10 @@
   f_previous ∈ {{ &a }}
 [eva] computing for function f <- main.
   Called from from_call.i:81.
-[eva] computing for function h <- f <- main.
-  Called from from_call.i:20.
 [kernel:annot:missing-spec] from_call.i:20: Warning: 
   Neither code nor specification for function h, generating default assigns from the prototype
+[eva] computing for function h <- f <- main.
+  Called from from_call.i:20.
 [eva] using specification for function h
 [eva] Done for function h
 [eva] computing for function g <- f <- main.
diff --git a/tests/value/oracle/ineq.res.oracle b/tests/value/oracle/ineq.res.oracle
index 22bf10d5982fbdaa347aa917108842155dd32e95..1f2d06ec970966e8c9191b178679e09853ea0157 100644
--- a/tests/value/oracle/ineq.res.oracle
+++ b/tests/value/oracle/ineq.res.oracle
@@ -12,10 +12,10 @@
   l ∈ {1}
   m ∈ {-1}
   n ∈ {-1}
-[eva] computing for function any_int <- main.
-  Called from ineq.c:6.
 [kernel:annot:missing-spec] ineq.c:6: Warning: 
   Neither code nor specification for function any_int, generating default assigns from the prototype
+[eva] computing for function any_int <- main.
+  Called from ineq.c:6.
 [eva] using specification for function any_int
 [eva] Done for function any_int
 [eva] Recording results for main
diff --git a/tests/value/oracle/infinite.res.oracle b/tests/value/oracle/infinite.res.oracle
index b88f0ef2e1ea05d252ed69d4f782c3d8ce4b1064..6085126abf62aef997cf6c4eb6d51861f89d4132 100644
--- a/tests/value/oracle/infinite.res.oracle
+++ b/tests/value/oracle/infinite.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   G ∈ {0}
-[eva] computing for function pause <- main.
-  Called from infinite.i:9.
 [kernel:annot:missing-spec] infinite.i:9: Warning: 
   Neither code nor specification for function pause, generating default assigns from the prototype
+[eva] computing for function pause <- main.
+  Called from infinite.i:9.
 [eva] using specification for function pause
 [eva] Done for function pause
 [eva] Recording results for main
diff --git a/tests/value/oracle/initialized_copy.0.res.oracle b/tests/value/oracle/initialized_copy.0.res.oracle
index 2832044a8141fa97c57ff81dd7daacaf40e97824..3e88f8016fc50e077dae6fbae61b9269784a3f97 100644
--- a/tests/value/oracle/initialized_copy.0.res.oracle
+++ b/tests/value/oracle/initialized_copy.0.res.oracle
@@ -96,10 +96,10 @@
   ==END OF DUMP==
 [eva:alarm] initialized_copy.i:151: Warning: 
   accessing uninitialized left-value. assert \initialized(&a_8);
-[eva] computing for function g <- main.
-  Called from initialized_copy.i:151.
 [kernel:annot:missing-spec] initialized_copy.i:151: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from initialized_copy.i:151.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] initialized_copy.i:152: 
diff --git a/tests/value/oracle/initialized_copy.1.res.oracle b/tests/value/oracle/initialized_copy.1.res.oracle
index 99d71e0d2f64e832857ff211df6e48551bba6423..10bb9ea2fcbae4dbd27d879054e00ed62283e9f6 100644
--- a/tests/value/oracle/initialized_copy.1.res.oracle
+++ b/tests/value/oracle/initialized_copy.1.res.oracle
@@ -88,10 +88,10 @@
   ==END OF DUMP==
 [eva:alarm] initialized_copy.i:151: Warning: 
   accessing uninitialized left-value. assert \initialized(&a_8);
-[eva] computing for function g <- main.
-  Called from initialized_copy.i:151.
 [kernel:annot:missing-spec] initialized_copy.i:151: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from initialized_copy.i:151.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] initialized_copy.i:152: 
diff --git a/tests/value/oracle/input.res.oracle b/tests/value/oracle/input.res.oracle
index ef6baf6216064ae1555e1e9a5207bf1f57f89b1c..29aae6615047adc061f32d720dd6fab271b04664 100644
--- a/tests/value/oracle/input.res.oracle
+++ b/tests/value/oracle/input.res.oracle
@@ -5,10 +5,10 @@
 [eva:initial-state] Values of globals at initialization
   a ∈ {0}
   b ∈ {0}
-[eva] computing for function f <- main.
-  Called from input.i:7.
 [kernel:annot:missing-spec] input.i:7: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from input.i:7.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index c99ce35def381874c3f25fa88cd8bc43d186a362..8b69565432950381de0d38b51c4826962f9849c6 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -29,10 +29,10 @@
   st_tab3_int_3.t[0] ∈ {30}
                .t[1] ∈ {31}
                .t[2] ∈ {32}
-[eva] computing for function f_int_int <- main.
-  Called from leaf.i:48.
 [kernel:annot:missing-spec] leaf.i:48: Warning: 
   Neither code nor specification for function f_int_int, generating default assigns from the prototype
+[eva] computing for function f_int_int <- main.
+  Called from leaf.i:48.
 [eva] using specification for function f_int_int
 [eva] Done for function f_int_int
 [eva] computing for function f_int_star_int <- main.
@@ -56,70 +56,70 @@
 [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}
-[eva] computing for function f_star_int_cint <- main.
-  Called from leaf.i:62.
 [kernel:annot:missing-spec] leaf.i:62: Warning: 
   Neither code nor specification for function f_star_int_cint, generating default assigns from the prototype
+[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
-[eva] computing for function f_star_int_int <- main.
-  Called from leaf.i:64.
 [kernel:annot:missing-spec] leaf.i:64: Warning: 
   Neither code nor specification for function f_star_int_int, generating default assigns from the prototype
+[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
-[eva] computing for function f_tab3_int_int <- main.
-  Called from leaf.i:65.
 [kernel:annot:missing-spec] leaf.i:65: Warning: 
   Neither code nor specification for function f_tab3_int_int, generating default assigns from the prototype
+[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
-[eva] computing for function f_tab_int_int <- main.
-  Called from leaf.i:66.
 [kernel:annot:missing-spec] leaf.i:66: Warning: 
   Neither code nor specification for function f_tab_int_int, generating default assigns from the prototype
+[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
-[eva] computing for function f_st_star_cint_st_star_cint <- main.
-  Called from leaf.i:68.
 [kernel:annot:missing-spec] leaf.i:68: Warning: 
   Neither code nor specification for function f_st_star_cint_st_star_cint, generating default assigns from the prototype
+[eva] computing for function f_st_star_cint_st_star_cint <- main.
+  Called from leaf.i:68.
 [eva] using specification for function f_st_star_cint_st_star_cint
 [eva] Done for function f_st_star_cint_st_star_cint
 [eva] leaf.i:68: 
   Assigning imprecise value to st_star_cint_1.
   The imprecision originates from Library function {leaf.i:68}
-[eva] computing for function f_st_star_int_st_star_int <- main.
-  Called from leaf.i:69.
 [kernel:annot:missing-spec] leaf.i:69: Warning: 
   Neither code nor specification for function f_st_star_int_st_star_int, generating default assigns from the prototype
+[eva] computing for function f_st_star_int_st_star_int <- main.
+  Called from leaf.i:69.
 [eva] using specification for function f_st_star_int_st_star_int
 [eva] Done for function f_st_star_int_st_star_int
 [eva] leaf.i:69: 
   Assigning imprecise value to st_star_int_1.
   The imprecision originates from Library function {leaf.i:69}
-[eva] computing for function f_st_tab3_int_st_tab3_int <- main.
-  Called from leaf.i:70.
 [kernel:annot:missing-spec] leaf.i:70: Warning: 
   Neither code nor specification for function f_st_tab3_int_st_tab3_int, generating default assigns from the prototype
+[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
-[eva] computing for function f_star_st_star_cint_int <- main.
-  Called from leaf.i:72.
 [kernel:annot:missing-spec] leaf.i:72: Warning: 
   Neither code nor specification for function f_star_st_star_cint_int, generating default assigns from the prototype
+[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
-[eva] computing for function f_star_st_star_int_int <- main.
-  Called from leaf.i:73.
 [kernel:annot:missing-spec] leaf.i:73: Warning: 
   Neither code nor specification for function f_star_st_star_int_int, generating default assigns from the prototype
+[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
-[eva] computing for function f_star_st_tab3_int_int <- main.
-  Called from leaf.i:74.
 [kernel:annot:missing-spec] leaf.i:74: Warning: 
   Neither code nor specification for function f_star_st_tab3_int_int, generating default assigns from the prototype
+[eva] computing for function f_star_st_tab3_int_int <- main.
+  Called from leaf.i:74.
 [eva] using specification for function f_star_st_tab3_int_int
 [eva] Done for function f_star_st_tab3_int_int
 [eva] Recording results for main
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 700476b6dde016a513c9bd35ad8cdba32886b8d6..c0946ca0be171fcc2ce2631d04d38a95357c9f55 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -8,10 +8,10 @@
   I ∈ {0}
 [eva:alarm] leaf2.i:6: Warning: 
   pointer downcast. assert (unsigned int)(&I) ≤ 2147483647;
-[eva] computing for function f <- main.
-  Called from leaf2.i:6.
 [kernel:annot:missing-spec] leaf2.i:6: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from leaf2.i:6.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] leaf2.i:6: 
diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle
index 8ceb41a435b7f6745fa1733edbcd7591b3799fac..3c6f556f1f8738ace5eb781d3063f038492700b5 100644
--- a/tests/value/oracle/leaf_spec.0.res.oracle
+++ b/tests/value/oracle/leaf_spec.0.res.oracle
@@ -4,36 +4,36 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f1 <- main.
-  Called from leaf_spec.i:19.
 [kernel:annot:missing-spec] leaf_spec.i:19: Warning: 
   Neither code nor specification for function f1, generating default assigns from the prototype
+[eva] computing for function f1 <- main.
+  Called from leaf_spec.i:19.
 [eva] using specification for function f1
 [eva] Done for function f1
-[eva] computing for function g <- main.
-  Called from leaf_spec.i:20.
 [kernel:annot:missing-spec] leaf_spec.i:20: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from leaf_spec.i:20.
 [eva] using specification for function g
 [eva] Done for function g
-[eva] computing for function h <- main.
-  Called from leaf_spec.i:21.
 [kernel:annot:missing-spec] leaf_spec.i:21: Warning: 
   Neither code nor specification for function h, generating default assigns from the prototype
+[eva] computing for function h <- main.
+  Called from leaf_spec.i:21.
 [eva] using specification for function h
 [eva] Done for function h
-[eva] computing for function k <- main.
-  Called from leaf_spec.i:22.
 [kernel:annot:missing-spec] leaf_spec.i:22: Warning: 
   Neither code nor specification for function k, generating default assigns from the prototype
+[eva] computing for function k <- main.
+  Called from leaf_spec.i:22.
 [eva] using specification for function k
 [eva:invalid-assigns] leaf_spec.i:22: 
   Completely invalid destination for assigns clause *l. Ignoring.
 [eva] Done for function k
-[eva] computing for function k0 <- main.
-  Called from leaf_spec.i:22.
 [kernel:annot:missing-spec] leaf_spec.i:22: Warning: 
   Neither code nor specification for function k0, generating default assigns from the prototype
+[eva] computing for function k0 <- main.
+  Called from leaf_spec.i:22.
 [eva] using specification for function k0
 [eva] Done for function k0
 [eva] Recording results for main
diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle
index 5aa26ccfd381223405ebafa19b30e595c7a7550b..2f12a97cad9e6699bd162c2f4df0e4d8395797ec 100644
--- a/tests/value/oracle/leaf_spec.1.res.oracle
+++ b/tests/value/oracle/leaf_spec.1.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- main1.
-  Called from leaf_spec.i:27.
 [kernel:annot:missing-spec] leaf_spec.i:27: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main1.
+  Called from leaf_spec.i:27.
 [eva] using specification for function f
 [eva:invalid-assigns] leaf_spec.i:27: 
   Completely invalid destination for assigns clause *x. Ignoring.
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index b8440bbf0b2cde6861086571dfce3f9f404ceedd..68669bb02a03d27ccbb06da61305e77d7b80a5f4 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -76,10 +76,10 @@
   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
-[eva] computing for function f_int <- main.
-  Called from library.i:30.
 [kernel:annot:missing-spec] library.i:30: Warning: 
   Neither code nor specification for function f_int, generating default assigns from the prototype
+[eva] computing for function f_int <- main.
+  Called from library.i:30.
 [eva] using specification for function f_int
 [eva] Done for function f_int
 [eva] computing for function f_star_int <- main.
@@ -95,10 +95,10 @@
 [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)));
-[eva] computing for function gen <- main.
-  Called from library.i:37.
 [kernel:annot:missing-spec] library.i:37: Warning: 
   Neither code nor specification for function gen, generating default assigns from the prototype
+[eva] computing for function gen <- main.
+  Called from library.i:37.
 [eva] using specification for function gen
 [eva] Done for function gen
 [eva:alarm] library.i:38: Warning: 
diff --git a/tests/value/oracle/local_variables.res.oracle b/tests/value/oracle/local_variables.res.oracle
index 982e7dbf46d78a5b9e5cd06ee6c04d4d0cf2a9ea..70764f925a71633ba2b0c359032138f30b424db5 100644
--- a/tests/value/oracle/local_variables.res.oracle
+++ b/tests/value/oracle/local_variables.res.oracle
@@ -13,10 +13,10 @@
   Called from local_variables.i:30.
 [eva] computing for function w <- u <- main.
   Called from local_variables.i:11.
-[eva] computing for function unkn <- w <- u <- main.
-  Called from local_variables.i:24.
 [kernel:annot:missing-spec] local_variables.i:24: Warning: 
   Neither code nor specification for function unkn, generating default assigns from the prototype
+[eva] computing for function unkn <- w <- u <- main.
+  Called from local_variables.i:24.
 [eva] using specification for function unkn
 [eva] Done for function unkn
 [eva] Recording results for w
diff --git a/tests/value/oracle/noreturn.res.oracle b/tests/value/oracle/noreturn.res.oracle
index 9feb9c11794d0c339d25ef1d7a0e007ee4e9952f..0021e4852e0e59b24f5556c723b88e2561e37a68 100644
--- a/tests/value/oracle/noreturn.res.oracle
+++ b/tests/value/oracle/noreturn.res.oracle
@@ -16,16 +16,16 @@
   Called from noreturn.i:28.
 [eva] Recording results for warn_never_ends
 [eva] Done for function warn_never_ends
-[eva] computing for function stop <- main.
-  Called from noreturn.i:29.
 [kernel:annot:missing-spec] noreturn.i:29: Warning: 
   Neither code nor specification for function stop, generating default assigns from the prototype
+[eva] computing for function stop <- main.
+  Called from noreturn.i:29.
 [eva] using specification for function stop
 [eva] Done for function stop
-[eva] computing for function haltme <- main.
-  Called from noreturn.i:30.
 [kernel:annot:missing-spec] noreturn.i:30: Warning: 
   Neither code nor specification for function haltme, generating default assigns from the prototype
+[eva] computing for function haltme <- main.
+  Called from noreturn.i:30.
 [eva] using specification for function haltme
 [eva] Done for function haltme
 [eva] computing for function never_ends <- main.
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index c310a6f5dd1fc6efa1e504fc30999195c0c4530f..a3cd9bb508d89c09a7ae8d37b6976c9410649457 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -110,10 +110,10 @@
 [eva] Done for function origin_arithmetic_3
 [eva] computing for function origin_leaf_1 <- main.
   Called from origin.i:97.
-[eva] computing for function g <- origin_leaf_1 <- main.
-  Called from origin.i:38.
 [kernel:annot:missing-spec] origin.i:38: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- origin_leaf_1 <- main.
+  Called from origin.i:38.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for origin_leaf_1
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index 0d2507fa5304be33ba086bac01b86a6b51662c6a..5ebc7d0dd4d15d7042776213e8d32beacb13d69e 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -52,10 +52,10 @@
    .t[0] ∈ {{ &y }}
    .t[1] ∈ {0}
   S_gpp[0..1] ∈ [--..--]
-[eva] computing for function f <- origin.
-  Called from origin.i:124.
 [kernel:annot:missing-spec] origin.i:124: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- origin.
+  Called from origin.i:124.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] origin.i:126: 
diff --git a/tests/value/oracle/output_leafs.res.oracle b/tests/value/oracle/output_leafs.res.oracle
index cda9d44678f1f73b8e299d152f62c575b59389a2..9f87300e48cebc7c507a5071b2b519a83248486c 100644
--- a/tests/value/oracle/output_leafs.res.oracle
+++ b/tests/value/oracle/output_leafs.res.oracle
@@ -43,10 +43,10 @@
 [eva] Done for function main2
 [eva] computing for function main3 <- main.
   Called from output_leafs.i:47.
-[eva] computing for function f <- main3 <- main.
-  Called from output_leafs.i:40.
 [kernel:annot:missing-spec] output_leafs.i:40: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main3 <- main.
+  Called from output_leafs.i:40.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main3
diff --git a/tests/value/oracle/pb.res.oracle b/tests/value/oracle/pb.res.oracle
index 887817b6ca59cbb20c33216dc68a84b81375f62d..52f3bdc4e4c319f819e5968a7d2b790cf1c7fa26 100644
--- a/tests/value/oracle/pb.res.oracle
+++ b/tests/value/oracle/pb.res.oracle
@@ -6,10 +6,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- main.
-  Called from pb.i:2.
 [kernel:annot:missing-spec] pb.i:2: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from pb.i:2.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/value/oracle/postcondition.res.oracle b/tests/value/oracle/postcondition.res.oracle
index acbf0e9f21176c1010490011f8d6e9c66c3b5496..e714c6b9e81a3e1687803b51ffca85555e2d1ef8 100644
--- a/tests/value/oracle/postcondition.res.oracle
+++ b/tests/value/oracle/postcondition.res.oracle
@@ -17,10 +17,10 @@
   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}
-[eva] computing for function u <- get_index <- main.
-  Called from postcondition.i:20.
 [kernel] postcondition.i:20: Warning: 
   No code nor implicit assigns clause for function u, generating default assigns from the prototype
+[eva] computing for function u <- get_index <- main.
+  Called from postcondition.i:20.
 [eva] using specification for function u
 [eva] Done for function u
 [eva] postcondition.i:18: starting to merge loop iterations
@@ -74,10 +74,10 @@
 [eva] computing for function u <- main.
   Called from postcondition.i:88.
 [eva] Done for function u
-[eva] computing for function cap <- main.
-  Called from postcondition.i:89.
 [kernel] postcondition.i:89: Warning: 
   No code nor implicit assigns clause for function cap, generating default assigns from the prototype
+[eva] computing for function cap <- main.
+  Called from postcondition.i:89.
 [eva] using specification for function cap
 [eva] Done for function cap
 [eva] computing for function u <- main.
diff --git a/tests/value/oracle/precond.res.oracle b/tests/value/oracle/precond.res.oracle
index d7cae39457b89da747d7bcb336d8ad742c310c61..01008cd04905b7032567375d16efff639f56a92a 100644
--- a/tests/value/oracle/precond.res.oracle
+++ b/tests/value/oracle/precond.res.oracle
@@ -17,19 +17,19 @@
 [eva] precond.c:32: function f: precondition 'i' got status valid.
 [eva] Recording results for f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from precond.c:34.
 [kernel] precond.c:34: Warning: 
   No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from precond.c:34.
 [eva] using specification for function g
 [eva:alarm] precond.c:34: Warning: function g: precondition got status unknown.
 [eva] Done for function g
 [eva] computing for function aux <- main.
   Called from precond.c:36.
-[eva] computing for function f2 <- aux <- main.
-  Called from precond.c:21.
 [kernel] precond.c:21: Warning: 
   No code nor implicit assigns clause for function f2, generating default assigns from the prototype
+[eva] computing for function f2 <- aux <- main.
+  Called from precond.c:21.
 [eva] using specification for function f2
 [eva] precond.c:21: function f2: precondition got status valid.
 [eva] Done for function f2
diff --git a/tests/value/oracle/precond2.0.res.oracle b/tests/value/oracle/precond2.0.res.oracle
index 10ee7cb691c71c333a96e0b869b71de6781c3e6c..bdee5be00a85220edd6ceda78281a48e0c6970d1 100644
--- a/tests/value/oracle/precond2.0.res.oracle
+++ b/tests/value/oracle/precond2.0.res.oracle
@@ -19,10 +19,10 @@
   function f: precondition 'i' got status invalid.
 [eva] Recording results for f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from precond2.c:24.
 [kernel] precond2.c:24: Warning: 
   No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from precond2.c:24.
 [eva] using specification for function g
 [eva] precond2.c:24: function g: precondition got status valid.
 [eva] Done for function g
diff --git a/tests/value/oracle/precond2.1.res.oracle b/tests/value/oracle/precond2.1.res.oracle
index 4787a711af49ec5c93398aa4513386bbb9d207e3..39929885285698e3c2746bd5c6e002c64c3dbfb1 100644
--- a/tests/value/oracle/precond2.1.res.oracle
+++ b/tests/value/oracle/precond2.1.res.oracle
@@ -17,10 +17,10 @@
   function f: precondition 'i' got status invalid.
 [eva] Recording results for f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from precond2.c:24.
 [kernel] precond2.c:24: Warning: 
   No code nor implicit assigns clause for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from precond2.c:24.
 [eva] using specification for function g
 [eva] precond2.c:24: function g: precondition got status valid.
 [eva] Done for function g
diff --git a/tests/value/oracle/resolve.res.oracle b/tests/value/oracle/resolve.res.oracle
index 1e2c42f7cc62a8c8b872a4c619c6e54d4dd16954..defb6792df4472409e9108e75305196444788196 100644
--- a/tests/value/oracle/resolve.res.oracle
+++ b/tests/value/oracle/resolve.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- main.
-  Called from resolve.i:12.
 [kernel:annot:missing-spec] resolve.i:12: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from resolve.i:12.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/value/oracle/semaphore.res.oracle b/tests/value/oracle/semaphore.res.oracle
index de195078b4da65e6526db33fd251edd0e6012669..cf0fba3e324ab5400ec7fc116d77d940581e3e77 100644
--- a/tests/value/oracle/semaphore.res.oracle
+++ b/tests/value/oracle/semaphore.res.oracle
@@ -5,10 +5,10 @@
 [eva:initial-state] Values of globals at initialization
   Sa ∈ {0}
   Sb ∈ {0}
-[eva] computing for function V <- g.
-  Called from semaphore.i:31.
 [kernel:annot:missing-spec] semaphore.i:31: Warning: 
   Neither code nor specification for function V, generating default assigns from the prototype
+[eva] computing for function V <- g.
+  Called from semaphore.i:31.
 [eva] using specification for function V
 [eva] Done for function V
 [eva] semaphore.i:29: starting to merge loop iterations
@@ -22,10 +22,10 @@
   Called from semaphore.i:31.
 [eva] Done for function V
 [eva] semaphore.i:28: starting to merge loop iterations
-[eva] computing for function P <- g.
-  Called from semaphore.i:34.
 [kernel:annot:missing-spec] semaphore.i:34: Warning: 
   Neither code nor specification for function P, generating default assigns from the prototype
+[eva] computing for function P <- g.
+  Called from semaphore.i:34.
 [eva] using specification for function P
 [eva] Done for function P
 [eva] computing for function P <- g.
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
index 7301164cb25036d22ed3e9da6cac60f15e358038..f6dca26f664107f8afc93860a8b2b367eee8d150 100644
--- a/tests/value/oracle/strings.res.oracle
+++ b/tests/value/oracle/strings.res.oracle
@@ -40,10 +40,10 @@
   Z ∈ {0}
 [eva] computing for function string_reads <- main.
   Called from strings.i:142.
-[eva] computing for function u <- string_reads <- main.
-  Called from strings.i:39.
 [kernel:annot:missing-spec] strings.i:39: Warning: 
   Neither code nor specification for function u, generating default assigns from the prototype
+[eva] computing for function u <- string_reads <- main.
+  Called from strings.i:39.
 [eva] using specification for function u
 [eva] Done for function u
 [eva:alarm] strings.i:39: Warning: 
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index dc0ab11b5660f5d184bc56375b5d3586dc795f57..5d8c312f33f90a61c9ac6f269a9b4d9561fe6739 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -52,16 +52,16 @@
   assertion got status invalid (stopping propagation).
 [eva] Recording results for logic
 [eva] Done for function logic
-[eva] computing for function f <- main.
-  Called from summary.i:64.
 [kernel:annot:missing-spec] summary.i:64: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from summary.i:64.
 [eva] using specification for function f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from summary.i:65.
 [kernel:annot:missing-spec] summary.i:65: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from summary.i:65.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for main
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index 81eb244352197d5f99e3c7f35bb16ba46ccbe574..5610a4663e51979179219c0c9d4a542bfb287c58 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -74,16 +74,16 @@
   assertion got status invalid (stopping propagation).
 [eva] Recording results for logic
 [eva] Done for function logic
-[eva] computing for function f <- main.
-  Called from summary.i:64.
 [kernel:annot:missing-spec] summary.i:64: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from summary.i:64.
 [eva] using specification for function f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from summary.i:65.
 [kernel:annot:missing-spec] summary.i:65: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from summary.i:65.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for main
diff --git a/tests/value/oracle/switch2.res.oracle b/tests/value/oracle/switch2.res.oracle
index 52037497ce51b4a7c161947bb78d1275461c30ff..93846958e7c6b1df55c67213acc6c7e2ce6f53fd 100644
--- a/tests/value/oracle/switch2.res.oracle
+++ b/tests/value/oracle/switch2.res.oracle
@@ -8,10 +8,10 @@
   Called from switch2.i:13.
 [eva] Recording results for f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from switch2.i:13.
 [kernel:annot:missing-spec] switch2.i:13: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from switch2.i:13.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] Recording results for main
diff --git a/tests/value/oracle/undef_fct.res.oracle b/tests/value/oracle/undef_fct.res.oracle
index 738e41a5ec2f5fda6a25510ee6fb66db84390151..1266df08b00565dbcde9742413e4d85f934dc556 100644
--- a/tests/value/oracle/undef_fct.res.oracle
+++ b/tests/value/oracle/undef_fct.res.oracle
@@ -6,10 +6,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function f <- main.
-  Called from undef_fct.i:3.
 [kernel:annot:missing-spec] undef_fct.i:3: Warning: 
   Neither code nor specification for function f, generating default assigns from the prototype
+[eva] computing for function f <- main.
+  Called from undef_fct.i:3.
 [eva] using specification for function f
 [eva] Done for function f
 [eva] Recording results for main
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index 91cc617b674eea1bd545678e4bae3bf1cb127695..e999d6f573cb0e0d9b5e643c52a2139be92e0c8b 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -16,10 +16,10 @@
   Called from use_spec.i:25.
 [eva] using specification for function f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from use_spec.i:26.
 [kernel:annot:missing-spec] use_spec.i:26: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from use_spec.i:26.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] computing for function h <- main.
diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index e06b8f503520e0a62d75ffb1b67abb3278ced7ed..509dad58e05892aeec5263d1b953f5d9db54bb68 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -16,10 +16,10 @@
   Called from use_spec.i:25.
 [eva] using specification for function f
 [eva] Done for function f
-[eva] computing for function g <- main.
-  Called from use_spec.i:26.
 [kernel:annot:missing-spec] use_spec.i:26: Warning: 
   Neither code nor specification for function g, generating default assigns from the prototype
+[eva] computing for function g <- main.
+  Called from use_spec.i:26.
 [eva] using specification for function g
 [eva] Done for function g
 [eva] computing for function h <- main.
diff --git a/tests/value/oracle/va_list.0.res.oracle b/tests/value/oracle/va_list.0.res.oracle
index 109901ba36a77c3204732e985e1ce444a69e5407..69b64d84e22aeec36515fb428b3431b527868fca 100644
--- a/tests/value/oracle/va_list.0.res.oracle
+++ b/tests/value/oracle/va_list.0.res.oracle
@@ -8,10 +8,10 @@
   creating variable S_0_S___va_params with imprecise size (type void)
 [eva:initial-state] 
   creating variable S_1_S___va_params with imprecise size (type void)
-[eva] computing for function __builtin_next_arg <- main.
-  Called from va_list.c:14.
 [kernel:annot:missing-spec] va_list.c:14: Warning: 
   Neither code nor specification for function __builtin_next_arg, generating default assigns from the prototype
+[eva] computing for function __builtin_next_arg <- main.
+  Called from va_list.c:14.
 [eva] using specification for function __builtin_next_arg
 [eva] Done for function __builtin_next_arg
 [eva] Recording results for main
diff --git a/tests/value/oracle/va_list.1.res.oracle b/tests/value/oracle/va_list.1.res.oracle
index b2650b533eff03b5ffbbb1d7985c695cfa6f51d1..77f3d371928e7bf65952e8a4bd0b46f99fbaee27 100644
--- a/tests/value/oracle/va_list.1.res.oracle
+++ b/tests/value/oracle/va_list.1.res.oracle
@@ -4,10 +4,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function __builtin_next_arg <- main.
-  Called from va_list.c:14.
 [kernel:annot:missing-spec] va_list.c:14: Warning: 
   Neither code nor specification for function __builtin_next_arg, generating default assigns from the prototype
+[eva] computing for function __builtin_next_arg <- main.
+  Called from va_list.c:14.
 [eva] using specification for function __builtin_next_arg
 [eva] va_list.c:14: User Error: 
   functions returning variadic arguments must be stubbed
diff --git a/tests/value/oracle/va_list2.1.res.oracle b/tests/value/oracle/va_list2.1.res.oracle
index 93afb0592bc75eb294262723678d451390130efe..8cd4da46460a0cb794978cdc83381675772311a0 100644
--- a/tests/value/oracle/va_list2.1.res.oracle
+++ b/tests/value/oracle/va_list2.1.res.oracle
@@ -4,17 +4,17 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function __builtin_va_start <- main.
-  Called from va_list2.c:11.
 [kernel:annot:missing-spec] va_list2.c:11: Warning: 
   Neither code nor specification for function __builtin_va_start, generating default assigns from the prototype
+[eva] computing for function __builtin_va_start <- main.
+  Called from va_list2.c:11.
 [eva] using specification for function __builtin_va_start
 [eva] Done for function __builtin_va_start
 [eva:alarm] va_list2.c:12: Warning: out of bounds read. assert \valid_read(fmt);
-[eva] computing for function __builtin_va_arg <- main.
-  Called from va_list2.c:15.
 [kernel:annot:missing-spec] va_list2.c:15: Warning: 
   Neither code nor specification for function __builtin_va_arg, generating default assigns from the prototype
+[eva] computing for function __builtin_va_arg <- main.
+  Called from va_list2.c:15.
 [eva] using specification for function __builtin_va_arg
 [eva] Done for function __builtin_va_arg
 [eva:alarm] va_list2.c:15: Warning: 
@@ -45,10 +45,10 @@
 [eva] Done for function __builtin_va_arg
 [eva] va_list2.c:21: 
   Frama_C_show_each_f: [-3.40282346639e+38 .. 3.40282346639e+38]
-[eva] computing for function __builtin_va_end <- main.
-  Called from va_list2.c:28.
 [kernel:annot:missing-spec] va_list2.c:28: Warning: 
   Neither code nor specification for function __builtin_va_end, generating default assigns from the prototype
+[eva] computing for function __builtin_va_end <- main.
+  Called from va_list2.c:28.
 [eva] using specification for function __builtin_va_end
 [eva] Done for function __builtin_va_end
 [eva] Recording results for main
diff --git a/tests/value/oracle/volatile.res.oracle b/tests/value/oracle/volatile.res.oracle
index 13de58ca7e95266d0f9b1b51c7b0e8f034edf31e..b53a798a5f7c73bcf06d26caccadc1451211679d 100644
--- a/tests/value/oracle/volatile.res.oracle
+++ b/tests/value/oracle/volatile.res.oracle
@@ -55,10 +55,10 @@
   signed overflow. assert x_0 + y_0 ≤ 2147483647;
 [eva] Recording results for fn1
 [eva] Done for function fn1
-[eva] computing for function fn2 <- main1 <- main.
-  Called from volatile.c:40.
 [kernel:annot:missing-spec] volatile.c:40: Warning: 
   Neither code nor specification for function fn2, generating default assigns from the prototype
+[eva] computing for function fn2 <- main1 <- main.
+  Called from volatile.c:40.
 [eva] using specification for function fn2
 [eva] Done for function fn2
 [eva] volatile.c:41: Frama_C_show_each_d: [-2147483648..2147483647]
diff --git a/tests/value/oracle/widen_overflow.res.oracle b/tests/value/oracle/widen_overflow.res.oracle
index 7dcb1b7df9e8dcd13231c31fc447b8b15a339b81..acaa81473fe37d047ff6fe8a31cebccec426c28d 100644
--- a/tests/value/oracle/widen_overflow.res.oracle
+++ b/tests/value/oracle/widen_overflow.res.oracle
@@ -7,10 +7,10 @@
 [eva:initial-state] Values of globals at initialization
   
 [eva] widen_overflow.i:6: Frama_C_show_each: {4}
-[eva] computing for function u <- main.
-  Called from widen_overflow.i:9.
 [kernel:annot:missing-spec] widen_overflow.i:9: Warning: 
   Neither code nor specification for function u, generating default assigns from the prototype
+[eva] computing for function u <- main.
+  Called from widen_overflow.i:9.
 [eva] using specification for function u
 [eva] Done for function u
 [eva] widen_overflow.i:9: starting to merge loop iterations
diff --git a/tests/value/traces/oracle/test5.res.oracle b/tests/value/traces/oracle/test5.res.oracle
index c3e94b81b6317e06c8284fddac7fb8784b329e78..65e159b215ac3cdbfd7881b377f7c6fac1cd2d06 100644
--- a/tests/value/traces/oracle/test5.res.oracle
+++ b/tests/value/traces/oracle/test5.res.oracle
@@ -7,10 +7,10 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva] computing for function my_switch <- main.
-  Called from test5.i:21.
 [kernel:annot:missing-spec] test5.i:21: Warning: 
   Neither code nor specification for function my_switch, generating default assigns from the prototype
+[eva] computing for function my_switch <- main.
+  Called from test5.i:21.
 [eva] using specification for function my_switch
 [eva] Done for function my_switch
 [eva:alarm] test5.i:21: Warning: