From 0da8cbebb7c259320c903f57560ccced85dd0e83 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?David=20B=C3=BChler?= <david.buhler@cea.fr>
Date: Mon, 21 Feb 2022 15:02:13 +0100
Subject: [PATCH] [Eva] Changes the order in which two messages are printed at
function calls.
---
.../tests/nonterm/oracle/n5.res.oracle | 8 ++--
.../report/tests/report/oracle/csv.res.oracle | 4 +-
src/plugins/value/engine/compute_functions.ml | 10 ++---
tests/builtins/oracle/imprecise.res.oracle | 8 ++--
tests/builtins/oracle/watch.res.oracle | 4 +-
.../oracle/fct_ptr.res.oracle | 4 +-
tests/float/oracle/alarms.0.res.oracle | 4 +-
tests/float/oracle/alarms.1.res.oracle | 4 +-
tests/float/oracle/alarms.2.res.oracle | 4 +-
.../contract_special_float.1.res.oracle | 4 +-
.../contract_special_float.2.res.oracle | 4 +-
tests/float/oracle/s.res.oracle | 12 ++---
tests/impact/oracle/call.0.res.oracle | 4 +-
tests/impact/oracle/call.1.res.oracle | 4 +-
tests/impact/oracle/call.2.res.oracle | 4 +-
tests/impact/oracle/undef_function.res.oracle | 4 +-
tests/impact/oracle/variadic.res.oracle | 4 +-
tests/journal/oracle/intra.res.oracle | 4 +-
tests/libc/oracle/search_h.res.oracle | 8 ++--
tests/libc/oracle/spawn_h.res.oracle | 32 +++++++-------
tests/pdg/oracle/bts1194.res.oracle | 4 +-
tests/pdg/oracle/no_body.res.oracle | 4 +-
.../pdg/oracle/pb_infinite_loop.2.res.oracle | 4 +-
tests/pdg/oracle/variadic.res.oracle | 4 +-
tests/scope/oracle/bts383.res.oracle | 4 +-
tests/slicing/oracle/bts1768.res.oracle | 4 +-
tests/slicing/oracle/bts709.res.oracle | 4 +-
tests/slicing/oracle/combine.res.oracle | 4 +-
tests/slicing/oracle/filter.res.oracle | 4 +-
tests/slicing/oracle/loops.15.res.oracle | 4 +-
tests/slicing/oracle/loops.16.res.oracle | 4 +-
tests/slicing/oracle/loops.17.res.oracle | 4 +-
tests/slicing/oracle/loops.18.res.oracle | 4 +-
tests/slicing/oracle/min_call.res.oracle | 12 ++---
tests/slicing/oracle/ptr_fct.res.oracle | 4 +-
.../oracle/select_by_annot.0.res.oracle | 4 +-
.../oracle/select_by_annot.1.res.oracle | 4 +-
.../oracle/select_by_annot.10.res.oracle | 4 +-
.../oracle/select_by_annot.11.res.oracle | 4 +-
.../oracle/select_by_annot.12.res.oracle | 4 +-
.../oracle/select_by_annot.13.res.oracle | 4 +-
.../oracle/select_by_annot.14.res.oracle | 4 +-
.../oracle/select_by_annot.2.res.oracle | 4 +-
.../oracle/select_by_annot.3.res.oracle | 4 +-
.../oracle/select_by_annot.4.res.oracle | 4 +-
.../oracle/select_by_annot.5.res.oracle | 4 +-
.../oracle/select_by_annot.6.res.oracle | 4 +-
.../oracle/select_by_annot.7.res.oracle | 4 +-
.../oracle/select_by_annot.8.res.oracle | 4 +-
.../oracle/select_by_annot.9.res.oracle | 4 +-
.../slicing/oracle/select_calls.0.res.oracle | 12 ++---
.../slicing/oracle/select_calls.1.res.oracle | 4 +-
.../slicing/oracle/select_return.0.res.oracle | 12 ++---
.../slicing/oracle/select_return.1.res.oracle | 12 ++---
.../oracle/select_return.10.res.oracle | 12 ++---
.../oracle/select_return.11.res.oracle | 12 ++---
.../oracle/select_return.12.res.oracle | 12 ++---
.../oracle/select_return.13.res.oracle | 12 ++---
.../oracle/select_return.14.res.oracle | 12 ++---
.../oracle/select_return.15.res.oracle | 12 ++---
.../oracle/select_return.16.res.oracle | 12 ++---
.../oracle/select_return.17.res.oracle | 12 ++---
.../oracle/select_return.18.res.oracle | 12 ++---
.../oracle/select_return.19.res.oracle | 12 ++---
.../slicing/oracle/select_return.2.res.oracle | 12 ++---
.../oracle/select_return.20.res.oracle | 12 ++---
.../oracle/select_return.21.res.oracle | 12 ++---
.../slicing/oracle/select_return.3.res.oracle | 12 ++---
.../slicing/oracle/select_return.4.res.oracle | 12 ++---
.../slicing/oracle/select_return.5.res.oracle | 12 ++---
.../slicing/oracle/select_return.6.res.oracle | 12 ++---
.../slicing/oracle/select_return.7.res.oracle | 12 ++---
.../slicing/oracle/select_return.8.res.oracle | 12 ++---
.../slicing/oracle/select_return.9.res.oracle | 12 ++---
.../oracle/select_return_bis.0.res.oracle | 12 ++---
.../oracle/select_return_bis.1.res.oracle | 12 ++---
.../oracle/select_return_bis.10.res.oracle | 12 ++---
.../oracle/select_return_bis.2.res.oracle | 12 ++---
.../oracle/select_return_bis.3.res.oracle | 12 ++---
.../oracle/select_return_bis.4.res.oracle | 12 ++---
.../oracle/select_return_bis.5.res.oracle | 12 ++---
.../oracle/select_return_bis.6.res.oracle | 12 ++---
.../oracle/select_return_bis.7.res.oracle | 12 ++---
.../oracle/select_return_bis.8.res.oracle | 12 ++---
.../oracle/select_return_bis.9.res.oracle | 12 ++---
tests/slicing/oracle/slice_no_body.res.oracle | 4 +-
.../oracle/unravel-flavors.0.res.oracle | 4 +-
.../oracle/unravel-flavors.1.res.oracle | 4 +-
.../oracle/unravel-flavors.2.res.oracle | 4 +-
.../oracle/unravel-flavors.3.res.oracle | 4 +-
.../slicing/oracle/unravel-point.0.res.oracle | 4 +-
.../slicing/oracle/unravel-point.1.res.oracle | 4 +-
.../slicing/oracle/unravel-point.2.res.oracle | 4 +-
.../slicing/oracle/unravel-point.3.res.oracle | 4 +-
.../slicing/oracle/unravel-point.4.res.oracle | 8 ++--
.../oracle/unravel-variance.0.res.oracle | 24 +++++-----
.../oracle/unravel-variance.1.res.oracle | 24 +++++-----
.../oracle/unravel-variance.2.res.oracle | 24 +++++-----
.../oracle/unravel-variance.3.res.oracle | 24 +++++-----
.../oracle/unravel-variance.4.res.oracle | 24 +++++-----
tests/slicing/oracle/variadic.0.res.oracle | 4 +-
tests/slicing/oracle/variadic.1.res.oracle | 4 +-
tests/slicing/oracle/variadic.2.res.oracle | 4 +-
tests/slicing/oracle/variadic.3.res.oracle | 4 +-
tests/slicing/oracle/variadic.4.res.oracle | 4 +-
tests/sparecode/oracle/bts334.0.res.oracle | 4 +-
tests/sparecode/oracle/bts334.1.res.oracle | 4 +-
tests/sparecode/oracle/bts334.2.res.oracle | 4 +-
tests/sparecode/oracle/intra.0.res.oracle | 4 +-
tests/sparecode/oracle/intra.1.res.oracle | 4 +-
tests/sparecode/oracle/top.1.res.oracle | 4 +-
tests/spec/oracle/assigns_void.1.res.oracle | 4 +-
tests/value/oracle/assigns.res.oracle | 16 +++----
tests/value/oracle/assigns_from.res.oracle | 4 +-
tests/value/oracle/automalloc.res.oracle | 8 ++--
tests/value/oracle/behaviors1.res.oracle | 20 ++++-----
tests/value/oracle/bitfield.res.oracle | 4 +-
tests/value/oracle/bts0506.0.res.oracle | 28 ++++++------
tests/value/oracle/bts0506.1.res.oracle | 28 ++++++------
tests/value/oracle/bug0223.0.res.oracle | 8 ++--
tests/value/oracle/bug0223.1.res.oracle | 8 ++--
tests/value/oracle/bug_023.res.oracle | 4 +-
tests/value/oracle/call.res.oracle | 8 ++--
tests/value/oracle/cond.res.oracle | 4 +-
tests/value/oracle/copy_stdin.res.oracle | 4 +-
tests/value/oracle/empty_struct.6.res.oracle | 4 +-
tests/value/oracle/f1.res.oracle | 4 +-
tests/value/oracle/false.res.oracle | 4 +-
tests/value/oracle/from_call.0.res.oracle | 4 +-
tests/value/oracle/from_call.1.res.oracle | 4 +-
tests/value/oracle/ineq.res.oracle | 4 +-
tests/value/oracle/infinite.res.oracle | 4 +-
.../oracle/initialized_copy.0.res.oracle | 4 +-
.../oracle/initialized_copy.1.res.oracle | 4 +-
tests/value/oracle/input.res.oracle | 4 +-
tests/value/oracle/leaf.res.oracle | 44 +++++++++----------
tests/value/oracle/leaf2.res.oracle | 4 +-
tests/value/oracle/leaf_spec.0.res.oracle | 20 ++++-----
tests/value/oracle/leaf_spec.1.res.oracle | 4 +-
tests/value/oracle/library.res.oracle | 8 ++--
tests/value/oracle/local_variables.res.oracle | 4 +-
tests/value/oracle/noreturn.res.oracle | 8 ++--
tests/value/oracle/origin.0.res.oracle | 4 +-
tests/value/oracle/origin.1.res.oracle | 4 +-
tests/value/oracle/output_leafs.res.oracle | 4 +-
tests/value/oracle/pb.res.oracle | 4 +-
tests/value/oracle/postcondition.res.oracle | 8 ++--
tests/value/oracle/precond.res.oracle | 8 ++--
tests/value/oracle/precond2.0.res.oracle | 4 +-
tests/value/oracle/precond2.1.res.oracle | 4 +-
tests/value/oracle/resolve.res.oracle | 4 +-
tests/value/oracle/semaphore.res.oracle | 8 ++--
tests/value/oracle/strings.res.oracle | 4 +-
tests/value/oracle/summary.3.res.oracle | 8 ++--
tests/value/oracle/summary.4.res.oracle | 8 ++--
tests/value/oracle/switch2.res.oracle | 4 +-
tests/value/oracle/undef_fct.res.oracle | 4 +-
tests/value/oracle/use_spec.0.res.oracle | 4 +-
tests/value/oracle/use_spec.1.res.oracle | 4 +-
tests/value/oracle/va_list.0.res.oracle | 4 +-
tests/value/oracle/va_list.1.res.oracle | 4 +-
tests/value/oracle/va_list2.1.res.oracle | 12 ++---
tests/value/oracle/volatile.res.oracle | 4 +-
tests/value/oracle/widen_overflow.res.oracle | 4 +-
tests/value/traces/oracle/test5.res.oracle | 4 +-
165 files changed, 641 insertions(+), 641 deletions(-)
diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
index 46379ed00ac..c46055dd4a5 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 b476eeb4126..5647ffdfd1d 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 32ebe6a24ae..701376e8202 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 b61a66f8678..c5d23a2cbd6 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 d4614af0957..d0a7fe337f5 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 89f9227804b..3b6bf0a4150 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 56452818c48..8e964fd6c67 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 e6c9a72e274..95735134c42 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 41b7b1439a8..6c47a9b44c5 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 fe8edb1fd33..86c08416bbd 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 3224017364e..daefc3e0500 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 6efaa5f3723..4981289b342 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 20364db19a0..10834db797c 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 9f1a28300c6..7388b39fa5c 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 517e087479b..8f91333b858 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 a62609de5f2..59f4b23f32d 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 e36dee6c9a0..b2c68043834 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 1cd15712237..052f7084bea 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 4c13bafba72..d4e37519386 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 b687f61add5..2f4e8e1010d 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 145aeb752d3..1af129e7a33 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 cbceb964eb1..f65d81c52ff 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 630316bb7ff..70e67333d4c 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 4557ce0ab0d..2ff0dc65eba 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 28b7158a7c8..5800bac5891 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 3a40e1f72cf..b9ebf7ff3bd 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 eeb349a839c..8230e738d1b 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 a9894ef7c84..59b371fa229 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 3d965436dc7..f4a04eb5b5e 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 16dd3f30158..eec7e4e722e 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 3fd8813c214..bea08b5034d 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 aa15e9fe124..0537db0b91b 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 04dc49b1ee3..70c363c51df 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 f3607c3ab3b..b13c5f6f59c 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 3d93973ee4d..6b36f47ccf3 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 31ce22ade86..8d7e7082e3c 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 c0f3575f5dc..ae07dade26d 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 c30f26887f6..34f900b14e6 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 5b27209920b..9b3fce6ec83 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 0c6fe54f4cf..762c51f3171 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 8f680bd8056..98dd4ebe7bd 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 69d8673daf1..0a2424c7fb1 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 2447ad2d338..169060a52c2 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 25a50f5cd59..3afd30f22fd 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 8d2642c6fa8..6997ef7e7a8 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 165cc861ab7..324e00126ff 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 fb469fe2139..233dfb495a3 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 540bcb17efb..87bb4419e11 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 31a3e7b2447..e92d795a5c1 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 8140a0c2883..a3c5b6b8368 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 94b3e492732..a684da35d34 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 7a93b917c1a..9d99c35a72c 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 8e3f0312d80..c11f145c965 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 85264a8d545..9c6ec7fbefb 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 dcdfd537935..2e7bb25265f 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 cbd031e0a0c..e1608c0ea0a 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 1359b887541..d05d1bf7538 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 e1b8f746bbe..3e93305f887 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 19c955fa3e8..78eee4e08b7 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 f1324cfe026..2fe88bed783 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 75cb38c7d7f..d12c38a5def 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 60119b1ea8b..9d0c0e93a69 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 a1023b621f8..f2116fc1925 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 3df04b0b9e8..ca61ac7c11d 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 479a7c97c1a..12e4ac0f72b 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 af215381307..112c5f5bfe9 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 be094adf73b..fc7b7263a78 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 1dc96345e15..9812edcd573 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 3a8819580ec..54256a99991 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 da728895098..4f5db2fd09e 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 206f26b5c65..49367975721 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 166d4eb3946..805198cb1ee 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 7a3e2021331..46f7ae57275 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 08c18f52960..cefcbc973eb 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 3f7c4dea692..8ea85881233 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 c3940889b4c..1985843e0c8 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 ea0823f9f32..e32eca9c3af 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 d057238968c..7373b527766 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 da97a2aa60c..92082b533a7 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 1447173a96e..4a345c49e0b 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 d85a5be0f6b..fc53a600ed4 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 fc50b4155ac..a31e484106f 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 0cbccc1d95c..59ffe732a6a 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 578fb7a7f41..956b521ba11 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 c0c04e4202f..7d550fad782 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 ddb4f878d25..a7c932d646a 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 b9bdf5dc091..3bcb555020c 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 2499a87e271..17186c7cd18 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 99c65cccbea..0402f471ca7 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 06320e6214a..fe639f3a189 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 e7cd4149d40..ac85ebce187 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 eacf84e9425..b51385835ff 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 cae8b16117c..2e29586990b 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 762e31c287d..75d9af9abc2 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 3bacc206809..6303ed58ec1 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 1c8e3423519..ce81c2c6e23 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 dc3d6684c28..bccf37024ec 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 26c8a8589de..ae3068ba0ad 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 4b3f186ea75..2664ab39dcc 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 df31e40bcc0..82f8aced737 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 d20a0522f67..6d5dd41248b 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 262fef8cb4b..caccc9ace2f 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 84212502c03..fae36df0bab 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 72db5708548..335a7f4c973 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 72db5708548..335a7f4c973 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 b514401262e..b5d83bb8ac7 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 14a05eb9249..77e6867d86f 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 46154e7440c..2f276f5ff60 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 519649a8fa7..14470158edb 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 15c053d475d..3715b90db0f 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 1d348f16c91..4f6f7329b0c 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 fa59eca7f82..fb9a8b2d5ba 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 fc787492fd0..1bdb53cd806 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 f8e6dc8fe59..0149986d5d7 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 5f9f0324265..1ead5d50a96 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 7971f0399f3..504e982e895 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 c38d611eb27..506aa9ec93d 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 b5cfd130ceb..994c9d1fe3e 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 188a7a4ff1a..18a53ed9fcc 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 bac86646e41..f470f869eec 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 bac86646e41..f470f869eec 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 4170a126f4f..a73637c9d9e 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 c79671e10e0..90128fff00c 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 aac8f1c4fa2..93f3f3d260d 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 318ef12b9de..d1469e3cccb 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 2ef33b093bc..712cbb8faff 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 ea4068132c6..4b59de37098 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 f5540c4e17c..25154cc12ce 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 2b4d8567b16..101005bed38 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 31c4e165ddf..14097263afd 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 22bf10d5982..1f2d06ec970 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 b88f0ef2e1e..6085126abf6 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 2832044a814..3e88f8016fc 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 99d71e0d2f6..10bb9ea2fcb 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 ef6baf62160..29aae661504 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 c99ce35def3..8b695654329 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 700476b6dde..c0946ca0be1 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 8ceb41a435b..3c6f556f1f8 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 5aa26ccfd38..2f12a97cad9 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 b8440bbf0b2..68669bb02a0 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 982e7dbf46d..70764f925a7 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 9feb9c11794..0021e4852e0 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 c310a6f5dd1..a3cd9bb508d 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 0d2507fa530..5ebc7d0dd4d 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 cda9d44678f..9f87300e48c 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 887817b6ca5..52f3bdc4e4c 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 acbf0e9f211..e714c6b9e81 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 d7cae39457b..01008cd0490 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 10ee7cb691c..bdee5be00a8 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 4787a711af4..39929885285 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 1e2c42f7cc6..defb6792df4 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 de195078b4d..cf0fba3e324 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 7301164cb25..f6dca26f664 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 dc0ab11b566..5d8c312f33f 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 81eb2443521..5610a4663e5 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 52037497ce5..93846958e7c 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 738e41a5ec2..1266df08b00 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 91cc617b674..e999d6f573c 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 e06b8f50352..509dad58e05 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 109901ba36a..69b64d84e22 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 b2650b533ef..77f3d371928 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 93afb0592bc..8cd4da46460 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 13de58ca7e9..b53a798a5f7 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 7dcb1b7df9e..acaa81473fe 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 c3e94b81b63..65e159b215a 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:
--
GitLab