From 03c48550003b827fe85b6f44354b557c8c1609dc Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 29 Jan 2024 18:31:40 +0100
Subject: [PATCH] [Eva] use callsite for populate_funspec locations
---
.../oracle/parallel_threads.res.oracle | 2 +-
.../oracle/threads_debug.res.oracle | 2 +-
.../memory/oracle/hidden_malloc.res.oracle | 2 +-
.../temporal/oracle/t_fun_lib.res.oracle | 2 +-
src/plugins/eva/engine/function_calls.ml | 15 ++++++++-----
.../tests/nonterm/oracle/n5.res.oracle | 4 ++--
.../report/tests/report/oracle/csv.res.oracle | 2 +-
.../oracle/empty-vpar-with-ghost.res.oracle | 2 +-
.../declared/oracle/empty-vpar.res.oracle | 2 +-
.../oracle/function-ptr-with-ghost.res.oracle | 2 +-
.../tests/declared/oracle/label.res.oracle | 2 +-
.../tests/declared/oracle/multi.res.oracle | 4 ++--
.../oracle/no-va-with-ghost.res.oracle | 2 +-
.../tests/declared/oracle/no-va.res.oracle | 2 +-
.../oracle/rvalues-with-ghost.res.oracle | 2 +-
.../tests/declared/oracle/rvalues.res.oracle | 2 +-
.../oracle/simple-with-ghost.res.oracle | 2 +-
.../tests/declared/oracle/simple.res.oracle | 2 +-
.../tests/declared/oracle/struct.res.oracle | 2 +-
.../typedefed_function-with-ghost.res.oracle | 2 +-
.../oracle/typedefed_function.res.oracle | 2 +-
.../tests/known/oracle/exec.res.oracle | 2 +-
.../tests/known/oracle/fcntl.res.oracle | 4 ++--
.../tests/known/oracle/open.res.oracle | 2 +-
.../tests/known/oracle/open_wrong.res.oracle | 2 +-
.../tests/known/oracle/openat.res.oracle | 2 +-
.../tests/known/oracle/printf.res.oracle | 2 +-
.../oracle/printf_wrong_arity.res.oracle | 2 +-
.../oracle/printf_wrong_types.res.oracle | 2 +-
tests/builtins/oracle/imprecise.res.oracle | 2 +-
.../oracle/fct_ptr.res.oracle | 2 +-
tests/fc_script/make-wrapper.t/run.t | 2 +-
tests/float/oracle/alarms.0.res.oracle | 2 +-
tests/float/oracle/alarms.1.res.oracle | 2 +-
tests/float/oracle/alarms.2.res.oracle | 2 +-
.../contract_special_float.1.res.oracle | 2 +-
.../contract_special_float.2.res.oracle | 2 +-
tests/float/oracle/s.res.oracle | 6 ++---
tests/impact/oracle/call.0.res.oracle | 2 +-
tests/impact/oracle/call.1.res.oracle | 2 +-
tests/impact/oracle/call.2.res.oracle | 2 +-
tests/impact/oracle/undef_function.res.oracle | 2 +-
tests/impact/oracle/variadic.res.oracle | 2 +-
tests/libc/oracle/search_h.res.oracle | 4 ++--
tests/libc/oracle/spawn_h.res.oracle | 16 +++++++-------
tests/pdg/oracle/bts1194.res.oracle | 2 +-
tests/pdg/oracle/no_body.res.oracle | 2 +-
.../pdg/oracle/pb_infinite_loop.2.res.oracle | 2 +-
tests/pdg/oracle/variadic.res.oracle | 2 +-
tests/scope/oracle/bts383.res.oracle | 2 +-
tests/slicing/oracle/bts1768.res.oracle | 2 +-
tests/slicing/oracle/bts709.res.oracle | 2 +-
tests/slicing/oracle/combine.res.oracle | 2 +-
tests/slicing/oracle/filter.res.oracle | 2 +-
tests/slicing/oracle/loops.15.res.oracle | 2 +-
tests/slicing/oracle/loops.16.res.oracle | 2 +-
tests/slicing/oracle/loops.17.res.oracle | 2 +-
tests/slicing/oracle/loops.18.res.oracle | 2 +-
tests/slicing/oracle/min_call.res.oracle | 6 ++---
tests/slicing/oracle/ptr_fct.res.oracle | 2 +-
.../oracle/select_by_annot.0.res.oracle | 2 +-
.../oracle/select_by_annot.1.res.oracle | 2 +-
.../oracle/select_by_annot.10.res.oracle | 2 +-
.../oracle/select_by_annot.11.res.oracle | 2 +-
.../oracle/select_by_annot.12.res.oracle | 2 +-
.../oracle/select_by_annot.13.res.oracle | 2 +-
.../oracle/select_by_annot.14.res.oracle | 2 +-
.../oracle/select_by_annot.2.res.oracle | 2 +-
.../oracle/select_by_annot.3.res.oracle | 2 +-
.../oracle/select_by_annot.4.res.oracle | 2 +-
.../oracle/select_by_annot.5.res.oracle | 2 +-
.../oracle/select_by_annot.6.res.oracle | 2 +-
.../oracle/select_by_annot.7.res.oracle | 2 +-
.../oracle/select_by_annot.8.res.oracle | 2 +-
.../oracle/select_by_annot.9.res.oracle | 2 +-
.../slicing/oracle/select_calls.0.res.oracle | 6 ++---
.../slicing/oracle/select_calls.1.res.oracle | 2 +-
.../slicing/oracle/select_return.0.res.oracle | 6 ++---
.../slicing/oracle/select_return.1.res.oracle | 6 ++---
.../oracle/select_return.10.res.oracle | 6 ++---
.../oracle/select_return.11.res.oracle | 6 ++---
.../oracle/select_return.12.res.oracle | 6 ++---
.../oracle/select_return.13.res.oracle | 6 ++---
.../oracle/select_return.14.res.oracle | 6 ++---
.../oracle/select_return.15.res.oracle | 6 ++---
.../oracle/select_return.16.res.oracle | 6 ++---
.../oracle/select_return.17.res.oracle | 6 ++---
.../oracle/select_return.18.res.oracle | 6 ++---
.../oracle/select_return.19.res.oracle | 6 ++---
.../slicing/oracle/select_return.2.res.oracle | 6 ++---
.../oracle/select_return.20.res.oracle | 6 ++---
.../oracle/select_return.21.res.oracle | 6 ++---
.../slicing/oracle/select_return.3.res.oracle | 6 ++---
.../slicing/oracle/select_return.4.res.oracle | 6 ++---
.../slicing/oracle/select_return.5.res.oracle | 6 ++---
.../slicing/oracle/select_return.6.res.oracle | 6 ++---
.../slicing/oracle/select_return.7.res.oracle | 6 ++---
.../slicing/oracle/select_return.8.res.oracle | 6 ++---
.../slicing/oracle/select_return.9.res.oracle | 6 ++---
.../oracle/select_return_bis.0.res.oracle | 6 ++---
.../oracle/select_return_bis.1.res.oracle | 6 ++---
.../oracle/select_return_bis.10.res.oracle | 6 ++---
.../oracle/select_return_bis.2.res.oracle | 6 ++---
.../oracle/select_return_bis.3.res.oracle | 6 ++---
.../oracle/select_return_bis.4.res.oracle | 6 ++---
.../oracle/select_return_bis.5.res.oracle | 6 ++---
.../oracle/select_return_bis.6.res.oracle | 6 ++---
.../oracle/select_return_bis.7.res.oracle | 6 ++---
.../oracle/select_return_bis.8.res.oracle | 6 ++---
.../oracle/select_return_bis.9.res.oracle | 6 ++---
tests/slicing/oracle/slice_no_body.res.oracle | 2 +-
.../oracle/unravel-flavors.0.res.oracle | 2 +-
.../oracle/unravel-flavors.1.res.oracle | 2 +-
.../oracle/unravel-flavors.2.res.oracle | 2 +-
.../oracle/unravel-flavors.3.res.oracle | 2 +-
.../slicing/oracle/unravel-point.0.res.oracle | 2 +-
.../slicing/oracle/unravel-point.1.res.oracle | 2 +-
.../slicing/oracle/unravel-point.2.res.oracle | 2 +-
.../slicing/oracle/unravel-point.3.res.oracle | 2 +-
.../slicing/oracle/unravel-point.4.res.oracle | 4 ++--
.../oracle/unravel-variance.0.res.oracle | 12 +++++-----
.../oracle/unravel-variance.1.res.oracle | 12 +++++-----
.../oracle/unravel-variance.2.res.oracle | 12 +++++-----
.../oracle/unravel-variance.3.res.oracle | 12 +++++-----
.../oracle/unravel-variance.4.res.oracle | 12 +++++-----
tests/slicing/oracle/variadic.0.res.oracle | 2 +-
tests/slicing/oracle/variadic.1.res.oracle | 2 +-
tests/slicing/oracle/variadic.2.res.oracle | 2 +-
tests/slicing/oracle/variadic.3.res.oracle | 2 +-
tests/slicing/oracle/variadic.4.res.oracle | 2 +-
tests/sparecode/oracle/bts334.0.res.oracle | 2 +-
tests/sparecode/oracle/bts334.1.res.oracle | 2 +-
tests/sparecode/oracle/bts334.2.res.oracle | 2 +-
tests/sparecode/oracle/intra.0.res.oracle | 2 +-
tests/sparecode/oracle/intra.1.res.oracle | 2 +-
tests/sparecode/oracle/top.1.res.oracle | 2 +-
tests/spec/oracle/assigns_void.1.res.oracle | 2 +-
.../oracle/default_assigns_bts0966.res.oracle | 2 +-
tests/value/oracle/assigns.res.oracle | 8 +++----
tests/value/oracle/assigns_from.res.oracle | 2 +-
tests/value/oracle/automalloc.res.oracle | 4 ++--
tests/value/oracle/behaviors1.res.oracle | 10 ++++-----
tests/value/oracle/bitfield.res.oracle | 2 +-
tests/value/oracle/bts0506.0.res.oracle | 14 ++++++------
tests/value/oracle/bts0506.1.res.oracle | 14 ++++++------
tests/value/oracle/bug0223.0.res.oracle | 4 ++--
tests/value/oracle/bug0223.1.res.oracle | 4 ++--
tests/value/oracle/bug_023.res.oracle | 2 +-
tests/value/oracle/call.res.oracle | 4 ++--
tests/value/oracle/copy_stdin.res.oracle | 2 +-
tests/value/oracle/empty_struct.6.res.oracle | 2 +-
tests/value/oracle/f1.res.oracle | 2 +-
tests/value/oracle/false.res.oracle | 2 +-
tests/value/oracle/from_call.0.res.oracle | 2 +-
tests/value/oracle/from_call.1.res.oracle | 2 +-
tests/value/oracle/ineq.res.oracle | 2 +-
tests/value/oracle/infinite.res.oracle | 2 +-
.../oracle/initialized_copy.0.res.oracle | 2 +-
.../oracle/initialized_copy.1.res.oracle | 2 +-
tests/value/oracle/input.res.oracle | 2 +-
tests/value/oracle/leaf.res.oracle | 22 +++++++++----------
tests/value/oracle/leaf2.res.oracle | 2 +-
tests/value/oracle/leaf_spec.0.res.oracle | 10 ++++-----
tests/value/oracle/leaf_spec.1.res.oracle | 2 +-
tests/value/oracle/library.res.oracle | 4 ++--
tests/value/oracle/local_variables.res.oracle | 2 +-
tests/value/oracle/noreturn.res.oracle | 4 ++--
tests/value/oracle/origin.0.res.oracle | 2 +-
tests/value/oracle/origin.1.res.oracle | 2 +-
tests/value/oracle/output_leafs.res.oracle | 2 +-
tests/value/oracle/postcond_leaf.res.oracle | 2 +-
tests/value/oracle/postcondition.res.oracle | 4 ++--
tests/value/oracle/precond.res.oracle | 4 ++--
tests/value/oracle/precond2.0.res.oracle | 2 +-
tests/value/oracle/precond2.1.res.oracle | 2 +-
tests/value/oracle/resolve.res.oracle | 2 +-
tests/value/oracle/semaphore.res.oracle | 4 ++--
tests/value/oracle/strings.res.oracle | 2 +-
tests/value/oracle/summary.3.res.oracle | 4 ++--
tests/value/oracle/summary.4.res.oracle | 4 ++--
tests/value/oracle/switch2.res.oracle | 2 +-
tests/value/oracle/use_spec.0.res.oracle | 2 +-
tests/value/oracle/use_spec.1.res.oracle | 2 +-
tests/value/oracle/volatile.res.oracle | 2 +-
184 files changed, 346 insertions(+), 341 deletions(-)
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
index 4a5816b86a6..67745c5779d 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/parallel_threads.res.oracle
@@ -158,7 +158,7 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: Warning:
+[kernel:annot:missing-spec] parallel_threads.c:121: Warning:
Neither code nor specification for function pthread_mutex_trylock,
generating default assigns. See -generated-spec-* options for more info
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning:
diff --git a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
index 4a5816b86a6..67745c5779d 100644
--- a/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
+++ b/src/plugins/e-acsl/tests/concurrency/oracle/threads_debug.res.oracle
@@ -158,7 +158,7 @@
function __e_acsl_assert, behavior blocking: precondition got status unknown.
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:226: Warning:
function __e_acsl_assert, behavior blocking: precondition got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: Warning:
+[kernel:annot:missing-spec] parallel_threads.c:121: Warning:
Neither code nor specification for function pthread_mutex_trylock,
generating default assigns. See -generated-spec-* options for more info
[eva:alarm] FRAMAC_SHARE/libc/pthread.h:313: Warning:
diff --git a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
index a7964a71784..aa890a27d2e 100644
--- a/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
+++ b/src/plugins/e-acsl/tests/memory/oracle/hidden_malloc.res.oracle
@@ -1,5 +1,5 @@
[e-acsl] beginning translation.
[e-acsl] translation done in project "e-acsl".
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+[kernel:annot:missing-spec] hidden_malloc.c:11: Warning:
Neither code nor specification for function realpath,
generating default assigns. See -generated-spec-* options for more info
diff --git a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
index 1583f80fac7..f6c71b561f1 100644
--- a/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
+++ b/src/plugins/e-acsl/tests/temporal/oracle/t_fun_lib.res.oracle
@@ -27,7 +27,7 @@
[eva:alarm] t_fun_lib.c:15: Warning:
function __e_acsl_assert_register_ulong: precondition data->values == \null ||
\valid(data->values) got status unknown.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: Warning:
+[kernel:annot:missing-spec] t_fun_lib.c:19: Warning:
Neither code nor specification for function realpath,
generating default assigns. See -generated-spec-* options for more info
[eva:alarm] t_fun_lib.c:22: Warning:
diff --git a/src/plugins/eva/engine/function_calls.ml b/src/plugins/eva/engine/function_calls.ml
index 24dd64d6ef9..ee88bbdc585 100644
--- a/src/plugins/eva/engine/function_calls.ml
+++ b/src/plugins/eva/engine/function_calls.ml
@@ -154,8 +154,13 @@ let use_spec_instead_of_definition ?(recursion_depth = -1) kf =
(* Returns the function specification of [kf], with generated assigns clauses
if they are missing. *)
-let get_funspec kf =
- Populate_spec.populate_funspec ~do_body:true kf [`Assigns];
+let get_funspec callsite kf =
+ let loc =
+ match callsite with
+ | Kglobal -> None
+ | Kstmt stmt -> Some (Cil_datatype.Stmt.loc stmt)
+ in
+ Populate_spec.populate_funspec ?loc ~do_body:true kf [`Assigns];
Annotations.funspec kf
let analysis_target ~recursion_depth callsite kf =
@@ -166,14 +171,14 @@ let analysis_target ~recursion_depth callsite kf =
if recursion_depth >= Parameters.RecursiveUnroll.get ()
then begin
Recursion.check_spec callsite kf;
- `Spec (get_funspec kf)
+ `Spec (get_funspec callsite kf)
end
else
match kf.fundec with
- | Declaration _ -> `Spec (get_funspec kf)
+ | Declaration _ -> `Spec (get_funspec callsite kf)
| Definition (def, _) ->
if Kernel_function.Set.mem kf (Parameters.UsePrototype.get ())
- then `Spec (get_funspec kf)
+ then `Spec (get_funspec callsite kf)
else `Body (def, save_results def)
let define_analysis_target ?(recursion_depth = -1) callsite kf =
diff --git a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
index 574cd52a006..04e470cae08 100644
--- a/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
+++ b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
nondet ∈ [--..--]
-[kernel:annot:missing-spec] n5.i:9: Warning:
+[kernel:annot:missing-spec] n5.i:21: Warning:
Neither code nor explicit assigns for function may_not_terminate,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function may_not_terminate <- main.
@@ -13,7 +13,7 @@
[eva] Done for function may_not_terminate
[eva] computing for function f <- main.
Called from n5.i:22.
-[kernel:annot:missing-spec] n5.i:5: Warning:
+[kernel:annot:missing-spec] n5.i:12: Warning:
Neither code nor explicit assigns for function never_terminates,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function never_terminates <- f <- main.
diff --git a/src/plugins/report/tests/report/oracle/csv.res.oracle b/src/plugins/report/tests/report/oracle/csv.res.oracle
index 210bc3fcccd..1ad19f92ff2 100644
--- a/src/plugins/report/tests/report/oracle/csv.res.oracle
+++ b/src/plugins/report/tests/report/oracle/csv.res.oracle
@@ -10,7 +10,7 @@
[eva] Done for function main1
[eva] computing for function main2 <- main.
Called from csv.c:55.
-[kernel:annot:missing-spec] csv.c:18: Warning:
+[kernel:annot:missing-spec] csv.c:21: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f <- main2 <- main.
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
index 9a4ba240832..8856945b2de 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar-with-ghost.res.oracle
@@ -2,7 +2,7 @@
[variadic] empty-vpar-with-ghost.i:8:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] empty-vpar-with-ghost.i:5: Warning:
+[kernel:annot:missing-spec] empty-vpar-with-ghost.i:8: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
index 72bb0792e2b..f59a25caa33 100644
--- a/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/empty-vpar.res.oracle
@@ -1,7 +1,7 @@
[variadic] empty-vpar.i:1: Declaration of variadic function f.
[variadic] empty-vpar.i:8: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] empty-vpar.i:5: Warning:
+[kernel:annot:missing-spec] empty-vpar.i:8: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
index c3a46f89849..c47d7de999a 100644
--- a/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/function-ptr-with-ghost.res.oracle
@@ -2,7 +2,7 @@
[variadic] function-ptr-with-ghost.i:2:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] function-ptr-with-ghost.i:4: Warning:
+[kernel:annot:missing-spec] function-ptr-with-ghost.i:2: Warning:
Neither code nor specification for function va_f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function va_f
diff --git a/src/plugins/variadic/tests/declared/oracle/label.res.oracle b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
index b77faefc9d6..bc7ed6281c8 100644
--- a/src/plugins/variadic/tests/declared/oracle/label.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/label.res.oracle
@@ -1,7 +1,7 @@
[variadic] label.i:4: Declaration of variadic function f.
[variadic] label.i:8: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] label.i:4: Warning:
+[kernel:annot:missing-spec] label.i:8: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index 3d7544a2bcc..b2c0657c754 100644
--- a/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
@@ -3,11 +3,11 @@
[variadic] multi.i:9: Generic translation of call to variadic function.
[variadic] multi.i:18: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] multi.i:15: Warning:
+[kernel:annot:missing-spec] multi.i:18: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function g
-[kernel:annot:missing-spec] multi.i:6: Warning:
+[kernel:annot:missing-spec] multi.i:9: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
index 5c1cc2988c4..73007ab0ccb 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va-with-ghost.res.oracle
@@ -1,5 +1,5 @@
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] no-va-with-ghost.i:1: Warning:
+[kernel:annot:missing-spec] no-va-with-ghost.i:4: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
index a9c2ce7a4bf..58717791f35 100644
--- a/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/no-va.res.oracle
@@ -1,5 +1,5 @@
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] no-va.i:1: Warning:
+[kernel:annot:missing-spec] no-va.i:4: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
index a900ef19ea7..5fbb9d01fa7 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues-with-ghost.res.oracle
@@ -2,7 +2,7 @@
[variadic] rvalues-with-ghost.i:5:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] rvalues-with-ghost.i:1: Warning:
+[kernel:annot:missing-spec] rvalues-with-ghost.i:5: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
index 0c9e683b20c..3ffbfe423b8 100644
--- a/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/rvalues.res.oracle
@@ -1,7 +1,7 @@
[variadic] rvalues.i:1: Declaration of variadic function f.
[variadic] rvalues.i:5: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] rvalues.i:1: Warning:
+[kernel:annot:missing-spec] rvalues.i:5: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
index 8025cbd92d5..6e687acfe0e 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple-with-ghost.res.oracle
@@ -2,7 +2,7 @@
[variadic] simple-with-ghost.i:9:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] simple-with-ghost.i:6: Warning:
+[kernel:annot:missing-spec] simple-with-ghost.i:9: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
index 54ea4910750..8725172d792 100644
--- a/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/simple.res.oracle
@@ -1,7 +1,7 @@
[variadic] simple.i:1: Declaration of variadic function f.
[variadic] simple.i:9: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] simple.i:6: Warning:
+[kernel:annot:missing-spec] simple.i:9: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
index bd5b5017ddb..ab60728bd8e 100644
--- a/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/struct.res.oracle
@@ -1,7 +1,7 @@
[variadic] struct.i:5: Declaration of variadic function f.
[variadic] struct.i:10: Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] struct.i:5: Warning:
+[kernel:annot:missing-spec] struct.i:10: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
index b0f695ca4af..a9bee4f8d44 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
@@ -3,7 +3,7 @@
[variadic] typedefed_function-with-ghost.i:5:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] typedefed_function-with-ghost.i:2: Warning:
+[kernel:annot:missing-spec] typedefed_function-with-ghost.i:5: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
index 5d7bccf0c58..2fa079d75a8 100644
--- a/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
+++ b/src/plugins/variadic/tests/declared/oracle/typedefed_function.res.oracle
@@ -2,7 +2,7 @@
[variadic] typedefed_function.i:5:
Generic translation of call to variadic function.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] typedefed_function.i:2: Warning:
+[kernel:annot:missing-spec] typedefed_function.i:5: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function f
diff --git a/src/plugins/variadic/tests/known/oracle/exec.res.oracle b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
index db382b8430b..74ea04f2c8f 100644
--- a/src/plugins/variadic/tests/known/oracle/exec.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/exec.res.oracle
@@ -22,7 +22,7 @@
[eva] using specification for function execve
[eva] using specification for function execv
[eva] using specification for function execvp
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/unistd.h:821: Warning:
+[kernel:annot:missing-spec] exec.c:15: Warning:
Neither code nor specification for function execlp_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function execlp_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
index c5b43790ae0..da138c294e8 100644
--- a/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/fcntl.res.oracle
@@ -37,7 +37,7 @@
[eva] using specification for function __va_fcntl_void
[eva] using specification for function __va_fcntl_int
[eva] using specification for function __va_fcntl_flock
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:129: Warning:
+[kernel:annot:missing-spec] fcntl.c:16: Warning:
Neither code nor specification for function fcntl_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function fcntl_fallback_1
@@ -45,7 +45,7 @@
function __va_fcntl_void: precondition 'cmd_has_void_arg' got status invalid.
[eva:alarm] fcntl.c:24: Warning:
function __va_fcntl_flock: precondition 'cmd_as_flock_arg' got status invalid.
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:129: Warning:
+[kernel:annot:missing-spec] fcntl.c:28: Warning:
Neither code nor specification for function fcntl_fallback_2,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function fcntl_fallback_2
diff --git a/src/plugins/variadic/tests/known/oracle/open.res.oracle b/src/plugins/variadic/tests/known/oracle/open.res.oracle
index 7814251c927..fd420fb5cef 100644
--- a/src/plugins/variadic/tests/known/oracle/open.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open.res.oracle
@@ -21,7 +21,7 @@
[eva] Analyzing a complete application starting at main
[eva] using specification for function __va_open_mode_t
[eva] using specification for function __va_open_void
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:136: Warning:
+[kernel:annot:missing-spec] open.c:9: Warning:
Neither code nor specification for function open_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function open_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
index c45e5c55e42..6550a1739aa 100644
--- a/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/open_wrong.res.oracle
@@ -13,7 +13,7 @@
[variadic] open_wrong.c:13:
Fallback translation of call open to a call to the specialized version open_fallback_1.
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:136: Warning:
+[kernel:annot:missing-spec] open_wrong.c:13: Warning:
Neither code nor specification for function open_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function open_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/openat.res.oracle b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
index f332052289b..b7ac263ec20 100644
--- a/src/plugins/variadic/tests/known/oracle/openat.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/openat.res.oracle
@@ -20,7 +20,7 @@
Fallback translation of call openat to a call to the specialized version openat_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] using specification for function __va_openat_mode_t
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:143: Warning:
+[kernel:annot:missing-spec] openat.c:10: Warning:
Neither code nor specification for function openat_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function openat_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/printf.res.oracle b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
index a6bd5f6a94d..96c9680ea4b 100644
--- a/src/plugins/variadic/tests/known/oracle/printf.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf.res.oracle
@@ -115,7 +115,7 @@
[eva] using specification for function printf_va_24
[eva] using specification for function printf_va_25
[eva] using specification for function printf_va_26
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning:
+[kernel:annot:missing-spec] printf.c:71: Warning:
Neither code nor specification for function printf_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function printf_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
index d89586c5159..4bc1b2c08cd 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_arity.res.oracle
@@ -28,7 +28,7 @@
Fallback translation of call printf to a call to the specialized version printf_va_2_fallback_1.
[eva] Analyzing a complete application starting at main
[eva] using specification for function printf_va_1
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning:
+[kernel:annot:missing-spec] printf_wrong_arity.c:9: Warning:
Neither code nor specification for function printf_va_2_fallback_1,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function printf_va_2_fallback_1
diff --git a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
index 83a51e8e270..24ae14ef3ed 100644
--- a/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
+++ b/src/plugins/variadic/tests/known/oracle/printf_wrong_types.res.oracle
@@ -348,7 +348,7 @@ int main(void)
[eva] Analyzing a complete application starting at main
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: Warning:
+[kernel:annot:missing-spec] printf_wrong_types.c:18: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function printf
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index 5ad0f3b323b..bc169708e5b 100644
--- a/tests/builtins/oracle/imprecise.res.oracle
+++ b/tests/builtins/oracle/imprecise.res.oracle
@@ -129,7 +129,7 @@
[eva] Done for function cast_address
[eva] computing for function garbled_mix_null <- main.
Called from imprecise.c:148.
-[kernel:annot:missing-spec] imprecise.c:72: Warning:
+[kernel:annot:missing-spec] imprecise.c:75: Warning:
Neither code nor specification for function gm_f1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function gm_f1 <- garbled_mix_null <- main.
diff --git a/tests/constant_propagation/oracle/fct_ptr.res.oracle b/tests/constant_propagation/oracle/fct_ptr.res.oracle
index 15dda274f30..a45058cb898 100644
--- a/tests/constant_propagation/oracle/fct_ptr.res.oracle
+++ b/tests/constant_propagation/oracle/fct_ptr.res.oracle
@@ -7,7 +7,7 @@
pf ∈ {0}
[eva] computing for function g <- main.
Called from fct_ptr.i:15.
-[kernel:annot:missing-spec] fct_ptr.i:11: Warning:
+[kernel:annot:missing-spec] fct_ptr.i:8: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- g <- main.
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
index 6e978274306..b64143a7e57 100644
--- a/tests/fc_script/make-wrapper.t/run.t
+++ b/tests/fc_script/make-wrapper.t/run.t
@@ -29,7 +29,7 @@ verbose output for Make.
main
[eva] using specification for function large_name_to_force_line_break_in_stack_msg
[eva] using specification for function specified
- [kernel:annot:missing-spec] make-wrapper.c:14: Warning:
+ [kernel:annot:missing-spec] make-wrapper.c:29: Warning:
Neither code nor specification for function external,
generating default assigns. See -generated-spec-* options for more info
[kernel] User Error: warning annot:missing-spec treated as fatal error.
diff --git a/tests/float/oracle/alarms.0.res.oracle b/tests/float/oracle/alarms.0.res.oracle
index 30155d0cc17..6d32745d1b0 100644
--- a/tests/float/oracle/alarms.0.res.oracle
+++ b/tests/float/oracle/alarms.0.res.oracle
@@ -37,7 +37,7 @@
mvd ∈ UNINITIALIZED
l ∈ [--..--]
==END OF DUMP==
-[kernel:annot:missing-spec] alarms.i:11: Warning:
+[kernel:annot:missing-spec] alarms.i:21: Warning:
Neither code nor specification for function fd,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function fd <- main1 <- main.
diff --git a/tests/float/oracle/alarms.1.res.oracle b/tests/float/oracle/alarms.1.res.oracle
index 69eb74ce4a3..7eb8cbc512c 100644
--- a/tests/float/oracle/alarms.1.res.oracle
+++ b/tests/float/oracle/alarms.1.res.oracle
@@ -34,7 +34,7 @@
mvd ∈ UNINITIALIZED
l ∈ [--..--]
==END OF DUMP==
-[kernel:annot:missing-spec] alarms.i:11: Warning:
+[kernel:annot:missing-spec] alarms.i:21: Warning:
Neither code nor specification for function fd,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function fd <- main1 <- main.
diff --git a/tests/float/oracle/alarms.2.res.oracle b/tests/float/oracle/alarms.2.res.oracle
index c8d7e2c4d4b..111eb599476 100644
--- a/tests/float/oracle/alarms.2.res.oracle
+++ b/tests/float/oracle/alarms.2.res.oracle
@@ -31,7 +31,7 @@
mvd ∈ UNINITIALIZED
l ∈ [--..--]
==END OF DUMP==
-[kernel:annot:missing-spec] alarms.i:11: Warning:
+[kernel:annot:missing-spec] alarms.i:21: Warning:
Neither code nor specification for function fd,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function fd <- main1 <- main.
diff --git a/tests/float/oracle/contract_special_float.1.res.oracle b/tests/float/oracle/contract_special_float.1.res.oracle
index 89383cc7912..4e3111b5d00 100644
--- a/tests/float/oracle/contract_special_float.1.res.oracle
+++ b/tests/float/oracle/contract_special_float.1.res.oracle
@@ -16,7 +16,7 @@
[eva] Done for function fun
[eva:alarm] contract_special_float.c:93: Warning:
NaN double value. assert ¬\is_NaN(v);
-[kernel:annot:missing-spec] contract_special_float.c:48: Warning:
+[kernel:annot:missing-spec] contract_special_float.c:94: Warning:
Neither code nor explicit assigns for function fun_no_default,
generating default clauses from the specification. See -generated-spec-* options for more info
[eva] computing for function fun_no_default <- main.
diff --git a/tests/float/oracle/contract_special_float.2.res.oracle b/tests/float/oracle/contract_special_float.2.res.oracle
index 1a83bef8646..5204d3ea928 100644
--- a/tests/float/oracle/contract_special_float.2.res.oracle
+++ b/tests/float/oracle/contract_special_float.2.res.oracle
@@ -8,7 +8,7 @@
Called from contract_special_float.c:92.
[eva] using specification for function fun
[eva] Done for function fun
-[kernel:annot:missing-spec] contract_special_float.c:48: Warning:
+[kernel:annot:missing-spec] contract_special_float.c:94: Warning:
Neither code nor explicit assigns for function fun_no_default,
generating default clauses from the specification. See -generated-spec-* options for more info
[eva] computing for function fun_no_default <- main.
diff --git a/tests/float/oracle/s.res.oracle b/tests/float/oracle/s.res.oracle
index 97c595ce712..02edc7f29a8 100644
--- a/tests/float/oracle/s.res.oracle
+++ b/tests/float/oracle/s.res.oracle
@@ -244,7 +244,7 @@
G19 ∈ {0}
[eva] computing for function F4 <- main.
Called from s.i:260.
-[kernel:annot:missing-spec] s.i:9: Warning:
+[kernel:annot:missing-spec] s.i:230: Warning:
Neither code nor specification for function F1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function F1 <- F4 <- main.
@@ -253,7 +253,7 @@
[eva] Done for function F1
[eva:alarm] s.i:231: Warning: accessing out of bounds index. assert 0 ≤ V4;
[eva:alarm] s.i:231: Warning: accessing out of bounds index. assert V4 < 64;
-[kernel:annot:missing-spec] s.i:10: Warning:
+[kernel:annot:missing-spec] s.i:233: Warning:
Neither code nor specification for function F2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function F2 <- F4 <- main.
@@ -267,7 +267,7 @@
[eva] Done for function F2
[eva:alarm] s.i:242: Warning: accessing out of bounds index. assert 0 ≤ V6;
[eva:alarm] s.i:242: Warning: accessing out of bounds index. assert V6 < 64;
-[kernel:annot:missing-spec] s.i:12: Warning:
+[kernel:annot:missing-spec] s.i:244: Warning:
Neither code nor specification for function F3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function F3 <- F4 <- main.
diff --git a/tests/impact/oracle/call.0.res.oracle b/tests/impact/oracle/call.0.res.oracle
index a246c6de55a..7c1a8df24df 100644
--- a/tests/impact/oracle/call.0.res.oracle
+++ b/tests/impact/oracle/call.0.res.oracle
@@ -12,7 +12,7 @@
Called from call.i:16.
[eva] using specification for function p1
[eva] Done for function p1
-[kernel:annot:missing-spec] call.i:12: Warning:
+[kernel:annot:missing-spec] call.i:16: Warning:
Neither code nor specification for function p2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function p2 <- test <- main.
diff --git a/tests/impact/oracle/call.1.res.oracle b/tests/impact/oracle/call.1.res.oracle
index ed164092a6a..22222bc2aac 100644
--- a/tests/impact/oracle/call.1.res.oracle
+++ b/tests/impact/oracle/call.1.res.oracle
@@ -14,7 +14,7 @@
Called from call.i:16.
[eva] using specification for function p1
[eva] Done for function p1
-[kernel:annot:missing-spec] call.i:12: Warning:
+[kernel:annot:missing-spec] call.i:16: Warning:
Neither code nor specification for function p2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function p2 <- test <- call_test <- main2.
diff --git a/tests/impact/oracle/call.2.res.oracle b/tests/impact/oracle/call.2.res.oracle
index ce3a3c2a489..2d7016cb262 100644
--- a/tests/impact/oracle/call.2.res.oracle
+++ b/tests/impact/oracle/call.2.res.oracle
@@ -15,7 +15,7 @@
[eva] using specification for function p3
[eva] call.i:41: Warning: no \from part for clause 'assigns G;'
[eva] Done for function p3
-[kernel:annot:missing-spec] call.i:12: Warning:
+[kernel:annot:missing-spec] call.i:45: Warning:
Neither code nor specification for function p2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function p2 <- test3 <- call_test3 <- main3.
diff --git a/tests/impact/oracle/undef_function.res.oracle b/tests/impact/oracle/undef_function.res.oracle
index 9661edfc6e0..94f614cca0a 100644
--- a/tests/impact/oracle/undef_function.res.oracle
+++ b/tests/impact/oracle/undef_function.res.oracle
@@ -5,7 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
y ∈ {0}
-[kernel:annot:missing-spec] undef_function.i:5: Warning:
+[kernel:annot:missing-spec] undef_function.i:10: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/impact/oracle/variadic.res.oracle b/tests/impact/oracle/variadic.res.oracle
index 6b28d3e6c56..bd08bb92439 100644
--- a/tests/impact/oracle/variadic.res.oracle
+++ b/tests/impact/oracle/variadic.res.oracle
@@ -6,7 +6,7 @@
[eva:initial-state] Values of globals at initialization
y ∈ {0}
z ∈ {0}
-[kernel:annot:missing-spec] variadic.i:6: Warning:
+[kernel:annot:missing-spec] variadic.i:12: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index 1e501dfc8b4..b4d4733d917 100644
--- a/tests/libc/oracle/search_h.res.oracle
+++ b/tests/libc/oracle/search_h.res.oracle
@@ -35,7 +35,7 @@
[eva] Done for function strcpy
[eva:alarm] search_h.c:32: Warning:
out of bounds write. assert \valid(&elementptr->count);
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/search.h:61: Warning:
+[kernel:annot:missing-spec] search_h.c:34: Warning:
Neither code nor specification for function tsearch,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function tsearch <- main.
@@ -55,7 +55,7 @@
[eva] Done for function exit
[eva:alarm] search_h.c:40: Warning:
out of bounds read. assert \valid_read((struct element **)node);
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/search.h:64: Warning:
+[kernel:annot:missing-spec] search_h.c:46: Warning:
Neither code nor specification for function twalk,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function twalk <- main.
diff --git a/tests/libc/oracle/spawn_h.res.oracle b/tests/libc/oracle/spawn_h.res.oracle
index 3809bf3497a..01e765f74b0 100644
--- a/tests/libc/oracle/spawn_h.res.oracle
+++ b/tests/libc/oracle/spawn_h.res.oracle
@@ -11,7 +11,7 @@
[eva:garbled-mix:write] spawn_h.c:36:
Assigning imprecise value to opt.
The imprecision originates from Library function {spawn_h.c:36}
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:72: Warning:
+[kernel:annot:missing-spec] spawn_h.c:43: Warning:
Neither code nor specification for function posix_spawn_file_actions_init,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawn_file_actions_init <- main.
@@ -28,7 +28,7 @@
Called from spawn_h.c:45.
[eva] using specification for function exit
[eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:55: Warning:
+[kernel:annot:missing-spec] spawn_h.c:47: Warning:
Neither code nor specification for function posix_spawn_file_actions_addclose,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawn_file_actions_addclose <- main.
@@ -43,7 +43,7 @@
[eva] computing for function exit <- main.
Called from spawn_h.c:50.
[eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:97: Warning:
+[kernel:annot:missing-spec] spawn_h.c:60: Warning:
Neither code nor specification for function posix_spawnattr_init,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_init <- main.
@@ -58,7 +58,7 @@
[eva] computing for function exit <- main.
Called from spawn_h.c:62.
[eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:99: Warning:
+[kernel:annot:missing-spec] spawn_h.c:63: Warning:
Neither code nor specification for function posix_spawnattr_setflags,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_setflags <- main.
@@ -79,7 +79,7 @@
[eva] spawn_h.c:67:
function sigfillset: precondition 'valid_set' got status valid.
[eva] Done for function sigfillset
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:113: Warning:
+[kernel:annot:missing-spec] spawn_h.c:68: Warning:
Neither code nor specification for function posix_spawnattr_setsigmask,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_setsigmask <- main.
@@ -148,7 +148,7 @@
[eva] Done for function exit
[eva:alarm] spawn_h.c:82: Warning:
out of bounds read. assert \valid_read(argv + optind);
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:116: Warning:
+[kernel:annot:missing-spec] spawn_h.c:82: Warning:
Neither code nor specification for function posix_spawnp,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnp <- main.
@@ -163,7 +163,7 @@
[eva] computing for function exit <- main.
Called from spawn_h.c:85.
[eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:75: Warning:
+[kernel:annot:missing-spec] spawn_h.c:90: Warning:
Neither code nor specification for function posix_spawnattr_destroy,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawnattr_destroy <- main.
@@ -178,7 +178,7 @@
[eva] computing for function exit <- main.
Called from spawn_h.c:92.
[eva] Done for function exit
-[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:69: Warning:
+[kernel:annot:missing-spec] spawn_h.c:96: Warning:
Neither code nor specification for function posix_spawn_file_actions_destroy,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function posix_spawn_file_actions_destroy <- main.
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 1c624742fba..110353a5cca 100644
--- a/tests/pdg/oracle/bts1194.res.oracle
+++ b/tests/pdg/oracle/bts1194.res.oracle
@@ -213,7 +213,7 @@
Y ∈ {0}
[eva] computing for function f_slice_1 <- main.
Called from bts1194.c:32.
-[kernel:annot:missing-spec] bts1194.c:9: Warning:
+[kernel:annot:missing-spec] bts1194.c:13: Warning:
Neither code nor specification for function input,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function input <- f_slice_1 <- main.
diff --git a/tests/pdg/oracle/no_body.res.oracle b/tests/pdg/oracle/no_body.res.oracle
index 3c7b0748670..64da29a0597 100644
--- a/tests/pdg/oracle/no_body.res.oracle
+++ b/tests/pdg/oracle/no_body.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
G ∈ {0}
-[kernel:annot:missing-spec] no_body.c:13: Warning:
+[kernel:annot:missing-spec] no_body.c:24: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/pdg/oracle/pb_infinite_loop.2.res.oracle b/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
index a65568abcc4..18b970df444 100644
--- a/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
+++ b/tests/pdg/oracle/pb_infinite_loop.2.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
G ∈ [--..--]
-[kernel:annot:missing-spec] pb_infinite_loop.c:43: Warning:
+[kernel:annot:missing-spec] pb_infinite_loop.c:48: Warning:
Neither code nor specification for function exit,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function exit <- test_exit.
diff --git a/tests/pdg/oracle/variadic.res.oracle b/tests/pdg/oracle/variadic.res.oracle
index 5f0af4fe428..acf750f7fc7 100644
--- a/tests/pdg/oracle/variadic.res.oracle
+++ b/tests/pdg/oracle/variadic.res.oracle
@@ -6,7 +6,7 @@
[eva] computing for function f1 <- main.
Called from variadic.c:37.
-[kernel:annot:missing-spec] variadic.c:20: Warning:
+[kernel:annot:missing-spec] variadic.c:23: Warning:
Neither code nor specification for function lib_f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/scope/oracle/bts383.res.oracle b/tests/scope/oracle/bts383.res.oracle
index ba7c315cccf..975b6c1a98e 100644
--- a/tests/scope/oracle/bts383.res.oracle
+++ b/tests/scope/oracle/bts383.res.oracle
@@ -38,7 +38,7 @@
Called from bts383.c:62.
[eva:alarm] bts383.c:35: Warning: out of bounds read. assert \valid_read(value);
[eva:alarm] bts383.c:36: Warning: out of bounds read. assert \valid_read(value);
-[kernel:annot:missing-spec] bts383.c:32: Warning:
+[kernel:annot:missing-spec] bts383.c:36: Warning:
Neither code nor specification for function out_char,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function out_char <- out_string <- main.
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 0b6a82d32ee..9fd462bcb24 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -10,7 +10,7 @@
step ∈ {0}
[eva] computing for function lecture <- main.
Called from bts1768.i:45.
-[kernel:annot:missing-spec] bts1768.i:15: Warning:
+[kernel:annot:missing-spec] bts1768.i:18: Warning:
Neither code nor explicit assigns for function choisir,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function choisir <- lecture <- main.
diff --git a/tests/slicing/oracle/bts709.res.oracle b/tests/slicing/oracle/bts709.res.oracle
index 0a690a35fb3..cad1b060401 100644
--- a/tests/slicing/oracle/bts709.res.oracle
+++ b/tests/slicing/oracle/bts709.res.oracle
@@ -9,7 +9,7 @@
var2 IN {0}
[eva] computing for function inputsOf_testcase_func <- main.
Called from bts709.c:47.
-[kernel:annot:missing-spec] bts709.c:54: Warning:
+[kernel:annot:missing-spec] bts709.c:55: Warning:
Neither code nor specification for function nondet_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function nondet_int <- inputsOf_testcase_func <- main.
diff --git a/tests/slicing/oracle/combine.res.oracle b/tests/slicing/oracle/combine.res.oracle
index e77debabe4d..2cbd14ab48a 100644
--- a/tests/slicing/oracle/combine.res.oracle
+++ b/tests/slicing/oracle/combine.res.oracle
@@ -121,7 +121,7 @@ int main(int x)
[eva] computing for function f <- main.
Called from combine.i:24.
-[kernel:annot:missing-spec] combine.i:8: Warning:
+[kernel:annot:missing-spec] combine.i:17: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- f <- main.
diff --git a/tests/slicing/oracle/filter.res.oracle b/tests/slicing/oracle/filter.res.oracle
index f6036ecc4fa..073800f4115 100644
--- a/tests/slicing/oracle/filter.res.oracle
+++ b/tests/slicing/oracle/filter.res.oracle
@@ -11,7 +11,7 @@
[eva] Done for function bts806
[eva] computing for function unspec <- main.
Called from filter.i:43.
-[kernel:annot:missing-spec] filter.i:6: Warning:
+[kernel:annot:missing-spec] filter.i:36: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- unspec <- main.
diff --git a/tests/slicing/oracle/loops.15.res.oracle b/tests/slicing/oracle/loops.15.res.oracle
index dd18cad9e65..726662f7e0d 100644
--- a/tests/slicing/oracle/loops.15.res.oracle
+++ b/tests/slicing/oracle/loops.15.res.oracle
@@ -11,7 +11,7 @@
Z ∈ [--..--]
[eva] loops.i:68: assertion got status valid.
[eva] loops.i:66: starting to merge loop iterations
-[kernel:annot:missing-spec] loops.i:61: Warning:
+[kernel:annot:missing-spec] loops.i:70: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- stop_f1.
diff --git a/tests/slicing/oracle/loops.16.res.oracle b/tests/slicing/oracle/loops.16.res.oracle
index 0cda5b17cde..5d4fe926d54 100644
--- a/tests/slicing/oracle/loops.16.res.oracle
+++ b/tests/slicing/oracle/loops.16.res.oracle
@@ -11,7 +11,7 @@
Z ∈ [--..--]
[eva] loops.i:68: assertion got status valid.
[eva] loops.i:66: starting to merge loop iterations
-[kernel:annot:missing-spec] loops.i:61: Warning:
+[kernel:annot:missing-spec] loops.i:70: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- stop_f1.
diff --git a/tests/slicing/oracle/loops.17.res.oracle b/tests/slicing/oracle/loops.17.res.oracle
index 4f0b797442e..04a864ff382 100644
--- a/tests/slicing/oracle/loops.17.res.oracle
+++ b/tests/slicing/oracle/loops.17.res.oracle
@@ -11,7 +11,7 @@
Z ∈ [--..--]
[eva:alarm] loops.i:82: Warning: signed overflow. assert c + 10 ≤ 2147483647;
[eva:alarm] loops.i:88: Warning: assertion got status unknown.
-[kernel:annot:missing-spec] loops.i:61: Warning:
+[kernel:annot:missing-spec] loops.i:89: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- stop_f2.
diff --git a/tests/slicing/oracle/loops.18.res.oracle b/tests/slicing/oracle/loops.18.res.oracle
index 5ea6c7a008e..45e2e5b6191 100644
--- a/tests/slicing/oracle/loops.18.res.oracle
+++ b/tests/slicing/oracle/loops.18.res.oracle
@@ -11,7 +11,7 @@
Z ∈ [--..--]
[eva:alarm] loops.i:82: Warning: signed overflow. assert c + 10 ≤ 2147483647;
[eva:alarm] loops.i:88: Warning: assertion got status unknown.
-[kernel:annot:missing-spec] loops.i:61: Warning:
+[kernel:annot:missing-spec] loops.i:89: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- stop_f2.
diff --git a/tests/slicing/oracle/min_call.res.oracle b/tests/slicing/oracle/min_call.res.oracle
index 78aabc7629f..87f3dae909c 100644
--- a/tests/slicing/oracle/min_call.res.oracle
+++ b/tests/slicing/oracle/min_call.res.oracle
@@ -10,14 +10,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -58,7 +58,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/ptr_fct.res.oracle b/tests/slicing/oracle/ptr_fct.res.oracle
index 047a99c8e94..6c3bee4acf3 100644
--- a/tests/slicing/oracle/ptr_fct.res.oracle
+++ b/tests/slicing/oracle/ptr_fct.res.oracle
@@ -8,7 +8,7 @@
ptf ∈ {0}
[eva] computing for function g <- h.
Called from ptr_fct.i:23.
-[kernel:annot:missing-spec] ptr_fct.i:11: Warning:
+[kernel:annot:missing-spec] ptr_fct.i:17: Warning:
Neither code nor specification for function f2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f2 <- g <- h.
diff --git a/tests/slicing/oracle/select_by_annot.0.res.oracle b/tests/slicing/oracle/select_by_annot.0.res.oracle
index cde9b9ebdde..e5de9941760 100644
--- a/tests/slicing/oracle/select_by_annot.0.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.0.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.1.res.oracle b/tests/slicing/oracle/select_by_annot.1.res.oracle
index 63bfc9b7a27..9b4b2a0f20b 100644
--- a/tests/slicing/oracle/select_by_annot.1.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.1.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.10.res.oracle b/tests/slicing/oracle/select_by_annot.10.res.oracle
index 47a035a0d9f..178bb3278c0 100644
--- a/tests/slicing/oracle/select_by_annot.10.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.10.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.11.res.oracle b/tests/slicing/oracle/select_by_annot.11.res.oracle
index e3871fd3d87..a394bebd6a6 100644
--- a/tests/slicing/oracle/select_by_annot.11.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.11.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.12.res.oracle b/tests/slicing/oracle/select_by_annot.12.res.oracle
index fdcad002e61..f466ab7ac09 100644
--- a/tests/slicing/oracle/select_by_annot.12.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.12.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.13.res.oracle b/tests/slicing/oracle/select_by_annot.13.res.oracle
index a6bee706619..a85c8c1ecd4 100644
--- a/tests/slicing/oracle/select_by_annot.13.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.13.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.14.res.oracle b/tests/slicing/oracle/select_by_annot.14.res.oracle
index cd9c16cbac3..1f98d6f3ef1 100644
--- a/tests/slicing/oracle/select_by_annot.14.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.14.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.2.res.oracle b/tests/slicing/oracle/select_by_annot.2.res.oracle
index a0845a156c5..7918bf2ca4e 100644
--- a/tests/slicing/oracle/select_by_annot.2.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.2.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.3.res.oracle b/tests/slicing/oracle/select_by_annot.3.res.oracle
index b8d5147e844..988211d29e3 100644
--- a/tests/slicing/oracle/select_by_annot.3.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.3.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.4.res.oracle b/tests/slicing/oracle/select_by_annot.4.res.oracle
index 3b7aab4fe85..769500d84d8 100644
--- a/tests/slicing/oracle/select_by_annot.4.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.4.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.5.res.oracle b/tests/slicing/oracle/select_by_annot.5.res.oracle
index d8ef7a2822c..feed01b3a62 100644
--- a/tests/slicing/oracle/select_by_annot.5.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.5.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.6.res.oracle b/tests/slicing/oracle/select_by_annot.6.res.oracle
index db410543427..75357eb578c 100644
--- a/tests/slicing/oracle/select_by_annot.6.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.6.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.7.res.oracle b/tests/slicing/oracle/select_by_annot.7.res.oracle
index 77d7282f748..1c1c5920893 100644
--- a/tests/slicing/oracle/select_by_annot.7.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.7.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.8.res.oracle b/tests/slicing/oracle/select_by_annot.8.res.oracle
index 0ebb63a1996..2cf898dc544 100644
--- a/tests/slicing/oracle/select_by_annot.8.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.8.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_by_annot.9.res.oracle b/tests/slicing/oracle/select_by_annot.9.res.oracle
index e80af681484..9bab22454a4 100644
--- a/tests/slicing/oracle/select_by_annot.9.res.oracle
+++ b/tests/slicing/oracle/select_by_annot.9.res.oracle
@@ -18,7 +18,7 @@
signed overflow. assert S.a + a ≤ 2147483647;
[eva] Recording results for modifS
[eva] Done for function modifS
-[kernel:annot:missing-spec] select_by_annot.i:126: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:140: Warning:
Neither code nor specification for function new_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function new_int <- main.
diff --git a/tests/slicing/oracle/select_calls.0.res.oracle b/tests/slicing/oracle/select_calls.0.res.oracle
index 3959136da4c..04a122b6451 100644
--- a/tests/slicing/oracle/select_calls.0.res.oracle
+++ b/tests/slicing/oracle/select_calls.0.res.oracle
@@ -6,7 +6,7 @@
[eva:initial-state] Values of globals at initialization
c ∈ [--..--]
d ∈ [--..--]
-[kernel:annot:missing-spec] select_calls.i:8: Warning:
+[kernel:annot:missing-spec] select_calls.i:22: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f.
@@ -16,7 +16,7 @@
[eva] computing for function send <- f.
Called from select_calls.i:23.
[eva] Done for function send
-[kernel:annot:missing-spec] select_calls.i:10: Warning:
+[kernel:annot:missing-spec] select_calls.i:24: Warning:
Neither code nor specification for function crypt,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function crypt <- f.
@@ -29,7 +29,7 @@
[eva] computing for function send <- f.
Called from select_calls.i:28.
[eva] Done for function send
-[kernel:annot:missing-spec] select_calls.i:12: Warning:
+[kernel:annot:missing-spec] select_calls.i:30: Warning:
Neither code nor specification for function uncrypt,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function uncrypt <- f.
diff --git a/tests/slicing/oracle/select_calls.1.res.oracle b/tests/slicing/oracle/select_calls.1.res.oracle
index c3a0e8506c5..fd1fa6b4d75 100644
--- a/tests/slicing/oracle/select_calls.1.res.oracle
+++ b/tests/slicing/oracle/select_calls.1.res.oracle
@@ -6,7 +6,7 @@
[eva:initial-state] Values of globals at initialization
c ∈ [--..--]
d ∈ [--..--]
-[kernel:annot:missing-spec] select_calls.i:6: Warning:
+[kernel:annot:missing-spec] select_calls.i:42: Warning:
Neither code nor specification for function nothing,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function nothing <- g.
diff --git a/tests/slicing/oracle/select_return.0.res.oracle b/tests/slicing/oracle/select_return.0.res.oracle
index b934f52d140..e7783ec0de8 100644
--- a/tests/slicing/oracle/select_return.0.res.oracle
+++ b/tests/slicing/oracle/select_return.0.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.1.res.oracle b/tests/slicing/oracle/select_return.1.res.oracle
index 97efb95010b..333c77abdec 100644
--- a/tests/slicing/oracle/select_return.1.res.oracle
+++ b/tests/slicing/oracle/select_return.1.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.10.res.oracle b/tests/slicing/oracle/select_return.10.res.oracle
index 3d590ac884d..35cd5e8e21e 100644
--- a/tests/slicing/oracle/select_return.10.res.oracle
+++ b/tests/slicing/oracle/select_return.10.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.11.res.oracle b/tests/slicing/oracle/select_return.11.res.oracle
index 6d50c819a40..25abd7c442a 100644
--- a/tests/slicing/oracle/select_return.11.res.oracle
+++ b/tests/slicing/oracle/select_return.11.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.12.res.oracle b/tests/slicing/oracle/select_return.12.res.oracle
index 966959e2d01..71a60f4e33e 100644
--- a/tests/slicing/oracle/select_return.12.res.oracle
+++ b/tests/slicing/oracle/select_return.12.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.13.res.oracle b/tests/slicing/oracle/select_return.13.res.oracle
index c3a9979aff7..374b5e57876 100644
--- a/tests/slicing/oracle/select_return.13.res.oracle
+++ b/tests/slicing/oracle/select_return.13.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.14.res.oracle b/tests/slicing/oracle/select_return.14.res.oracle
index f7fe215fa0c..490fec97454 100644
--- a/tests/slicing/oracle/select_return.14.res.oracle
+++ b/tests/slicing/oracle/select_return.14.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.15.res.oracle b/tests/slicing/oracle/select_return.15.res.oracle
index 03b193f4a42..133365cf41b 100644
--- a/tests/slicing/oracle/select_return.15.res.oracle
+++ b/tests/slicing/oracle/select_return.15.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.16.res.oracle b/tests/slicing/oracle/select_return.16.res.oracle
index 9db6296f5e2..22f1c275ac6 100644
--- a/tests/slicing/oracle/select_return.16.res.oracle
+++ b/tests/slicing/oracle/select_return.16.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.17.res.oracle b/tests/slicing/oracle/select_return.17.res.oracle
index e8cb8185f8f..c2e59c2a942 100644
--- a/tests/slicing/oracle/select_return.17.res.oracle
+++ b/tests/slicing/oracle/select_return.17.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.18.res.oracle b/tests/slicing/oracle/select_return.18.res.oracle
index da8a8c63d9b..76d57c2c353 100644
--- a/tests/slicing/oracle/select_return.18.res.oracle
+++ b/tests/slicing/oracle/select_return.18.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.19.res.oracle b/tests/slicing/oracle/select_return.19.res.oracle
index 14dbc9a6b57..c4c03e484a9 100644
--- a/tests/slicing/oracle/select_return.19.res.oracle
+++ b/tests/slicing/oracle/select_return.19.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.2.res.oracle b/tests/slicing/oracle/select_return.2.res.oracle
index f5f8270f853..30dee131fa8 100644
--- a/tests/slicing/oracle/select_return.2.res.oracle
+++ b/tests/slicing/oracle/select_return.2.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.20.res.oracle b/tests/slicing/oracle/select_return.20.res.oracle
index 1d1b7c31dd1..21d015132d3 100644
--- a/tests/slicing/oracle/select_return.20.res.oracle
+++ b/tests/slicing/oracle/select_return.20.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.21.res.oracle b/tests/slicing/oracle/select_return.21.res.oracle
index e80ecd16453..1aedb324dc3 100644
--- a/tests/slicing/oracle/select_return.21.res.oracle
+++ b/tests/slicing/oracle/select_return.21.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.3.res.oracle b/tests/slicing/oracle/select_return.3.res.oracle
index c992fa8daa7..512580d2488 100644
--- a/tests/slicing/oracle/select_return.3.res.oracle
+++ b/tests/slicing/oracle/select_return.3.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.4.res.oracle b/tests/slicing/oracle/select_return.4.res.oracle
index dea84380dbf..0bdd4613f78 100644
--- a/tests/slicing/oracle/select_return.4.res.oracle
+++ b/tests/slicing/oracle/select_return.4.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.5.res.oracle b/tests/slicing/oracle/select_return.5.res.oracle
index 5d06e588806..b9b128bad9c 100644
--- a/tests/slicing/oracle/select_return.5.res.oracle
+++ b/tests/slicing/oracle/select_return.5.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.6.res.oracle b/tests/slicing/oracle/select_return.6.res.oracle
index 045c7b13ff6..2a25d0ccc94 100644
--- a/tests/slicing/oracle/select_return.6.res.oracle
+++ b/tests/slicing/oracle/select_return.6.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.7.res.oracle b/tests/slicing/oracle/select_return.7.res.oracle
index 80595d9f5e0..4f6a431dcc0 100644
--- a/tests/slicing/oracle/select_return.7.res.oracle
+++ b/tests/slicing/oracle/select_return.7.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.8.res.oracle b/tests/slicing/oracle/select_return.8.res.oracle
index a77fac918a0..24560b33d23 100644
--- a/tests/slicing/oracle/select_return.8.res.oracle
+++ b/tests/slicing/oracle/select_return.8.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return.9.res.oracle b/tests/slicing/oracle/select_return.9.res.oracle
index beffeb890cd..1aff238e6d1 100644
--- a/tests/slicing/oracle/select_return.9.res.oracle
+++ b/tests/slicing/oracle/select_return.9.res.oracle
@@ -11,14 +11,14 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return.i:44.
-[kernel:annot:missing-spec] select_return.i:28: Warning:
+[kernel:annot:missing-spec] select_return.i:35: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:32: Warning:
+[kernel:annot:missing-spec] select_return.i:39: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k <- g.
@@ -59,7 +59,7 @@
[eva] Done for function send_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return.i:30: Warning:
+[kernel:annot:missing-spec] select_return.i:53: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.0.res.oracle b/tests/slicing/oracle/select_return_bis.0.res.oracle
index eb0059d622e..1986a1f5e3a 100644
--- a/tests/slicing/oracle/select_return_bis.0.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.0.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.1.res.oracle b/tests/slicing/oracle/select_return_bis.1.res.oracle
index a810b5fdfcf..0b66bb17ec3 100644
--- a/tests/slicing/oracle/select_return_bis.1.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.1.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.10.res.oracle b/tests/slicing/oracle/select_return_bis.10.res.oracle
index 64ca689f84f..0a9c10c832f 100644
--- a/tests/slicing/oracle/select_return_bis.10.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.10.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.2.res.oracle b/tests/slicing/oracle/select_return_bis.2.res.oracle
index 7850686158e..77cabccd7a9 100644
--- a/tests/slicing/oracle/select_return_bis.2.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.2.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.3.res.oracle b/tests/slicing/oracle/select_return_bis.3.res.oracle
index 6d026acbd80..66d2c8939ba 100644
--- a/tests/slicing/oracle/select_return_bis.3.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.3.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.4.res.oracle b/tests/slicing/oracle/select_return_bis.4.res.oracle
index ce7ae154cf4..5b6b79c6c32 100644
--- a/tests/slicing/oracle/select_return_bis.4.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.4.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.5.res.oracle b/tests/slicing/oracle/select_return_bis.5.res.oracle
index 42af2bc0520..fb4196860a8 100644
--- a/tests/slicing/oracle/select_return_bis.5.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.5.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.6.res.oracle b/tests/slicing/oracle/select_return_bis.6.res.oracle
index a709300a7c3..f2a805d61eb 100644
--- a/tests/slicing/oracle/select_return_bis.6.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.6.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.7.res.oracle b/tests/slicing/oracle/select_return_bis.7.res.oracle
index 02c2717dbd5..8543cd69f05 100644
--- a/tests/slicing/oracle/select_return_bis.7.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.7.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.8.res.oracle b/tests/slicing/oracle/select_return_bis.8.res.oracle
index 3e445d2ee61..bfe24c784f6 100644
--- a/tests/slicing/oracle/select_return_bis.8.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.8.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/select_return_bis.9.res.oracle b/tests/slicing/oracle/select_return_bis.9.res.oracle
index 8b0e71e1bea..e0d303d726d 100644
--- a/tests/slicing/oracle/select_return_bis.9.res.oracle
+++ b/tests/slicing/oracle/select_return_bis.9.res.oracle
@@ -11,7 +11,7 @@
I ∈ [--..--]
[eva] computing for function k <- g.
Called from select_return_bis.i:35.
-[kernel:annot:missing-spec] select_return_bis.i:16: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:28: Warning:
Neither code nor specification for function get,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function get <- k <- g.
@@ -20,7 +20,7 @@
[eva] Done for function get
[eva] computing for function k_bis <- k <- g.
Called from select_return_bis.i:30.
-[kernel:annot:missing-spec] select_return_bis.i:19: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:24: Warning:
Neither code nor specification for function send_bis,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send_bis <- k_bis <- k <- g.
@@ -63,7 +63,7 @@
[eva] select_return_bis.i:30: Reusing old results for call to k_bis
[eva] Recording results for k
[eva] Done for function k
-[kernel:annot:missing-spec] select_return_bis.i:18: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:44: Warning:
Neither code nor specification for function send,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function send <- f <- g.
diff --git a/tests/slicing/oracle/slice_no_body.res.oracle b/tests/slicing/oracle/slice_no_body.res.oracle
index 41ec5343c90..7363f61184e 100644
--- a/tests/slicing/oracle/slice_no_body.res.oracle
+++ b/tests/slicing/oracle/slice_no_body.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
G ∈ [--..--]
-[kernel:annot:missing-spec] slice_no_body.i:9: Warning:
+[kernel:annot:missing-spec] slice_no_body.i:21: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- h.
diff --git a/tests/slicing/oracle/unravel-flavors.0.res.oracle b/tests/slicing/oracle/unravel-flavors.0.res.oracle
index ae79b26d9eb..9e74fb164a5 100644
--- a/tests/slicing/oracle/unravel-flavors.0.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.0.res.oracle
@@ -61,7 +61,7 @@
signed overflow. assert yellow + green ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-flavors.1.res.oracle b/tests/slicing/oracle/unravel-flavors.1.res.oracle
index 8dc524e7573..f16981aa519 100644
--- a/tests/slicing/oracle/unravel-flavors.1.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.1.res.oracle
@@ -61,7 +61,7 @@
signed overflow. assert yellow + green ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-flavors.2.res.oracle b/tests/slicing/oracle/unravel-flavors.2.res.oracle
index fd303d69636..a8135ee7087 100644
--- a/tests/slicing/oracle/unravel-flavors.2.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.2.res.oracle
@@ -61,7 +61,7 @@
signed overflow. assert yellow + green ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-flavors.3.res.oracle b/tests/slicing/oracle/unravel-flavors.3.res.oracle
index a439aa19915..9a83feb26ec 100644
--- a/tests/slicing/oracle/unravel-flavors.3.res.oracle
+++ b/tests/slicing/oracle/unravel-flavors.3.res.oracle
@@ -61,7 +61,7 @@
signed overflow. assert yellow + green ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-flavors.i:60.
-[kernel:annot:missing-spec] unravel-flavors.i:16: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:19: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.0.res.oracle b/tests/slicing/oracle/unravel-point.0.res.oracle
index 8a3f0ff6239..37844d3957e 100644
--- a/tests/slicing/oracle/unravel-point.0.res.oracle
+++ b/tests/slicing/oracle/unravel-point.0.res.oracle
@@ -36,7 +36,7 @@
signed overflow. assert *y + *x ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning:
+[kernel:annot:missing-spec] unravel-point.i:36: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.1.res.oracle b/tests/slicing/oracle/unravel-point.1.res.oracle
index a8e1db664dd..97703a34e75 100644
--- a/tests/slicing/oracle/unravel-point.1.res.oracle
+++ b/tests/slicing/oracle/unravel-point.1.res.oracle
@@ -36,7 +36,7 @@
signed overflow. assert *y + *x ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning:
+[kernel:annot:missing-spec] unravel-point.i:36: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.2.res.oracle b/tests/slicing/oracle/unravel-point.2.res.oracle
index 5a7ab392ed5..985169fe22a 100644
--- a/tests/slicing/oracle/unravel-point.2.res.oracle
+++ b/tests/slicing/oracle/unravel-point.2.res.oracle
@@ -36,7 +36,7 @@
signed overflow. assert *y + *x ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning:
+[kernel:annot:missing-spec] unravel-point.i:36: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.3.res.oracle b/tests/slicing/oracle/unravel-point.3.res.oracle
index bf41616d75e..1a4a5c83d40 100644
--- a/tests/slicing/oracle/unravel-point.3.res.oracle
+++ b/tests/slicing/oracle/unravel-point.3.res.oracle
@@ -36,7 +36,7 @@
signed overflow. assert *y + *x ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning:
+[kernel:annot:missing-spec] unravel-point.i:36: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
diff --git a/tests/slicing/oracle/unravel-point.4.res.oracle b/tests/slicing/oracle/unravel-point.4.res.oracle
index 675b48c03ef..e0f32464a55 100644
--- a/tests/slicing/oracle/unravel-point.4.res.oracle
+++ b/tests/slicing/oracle/unravel-point.4.res.oracle
@@ -36,7 +36,7 @@
signed overflow. assert *y + *x ≤ 2147483647;
[eva] computing for function send1 <- main.
Called from unravel-point.i:75.
-[kernel:annot:missing-spec] unravel-point.i:26: Warning:
+[kernel:annot:missing-spec] unravel-point.i:36: Warning:
Neither code nor specification for function printf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf <- send1 <- main.
@@ -140,7 +140,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] unravel-point.i:22: Warning:
+[kernel:annot:missing-spec] unravel-point.i:59: Warning:
Neither code nor specification for function scanf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function scanf <- main.
diff --git a/tests/slicing/oracle/unravel-variance.0.res.oracle b/tests/slicing/oracle/unravel-variance.0.res.oracle
index 513c0912072..e9aae04102c 100644
--- a/tests/slicing/oracle/unravel-variance.0.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.0.res.oracle
@@ -5,7 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning:
Neither code nor specification for function scanf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
[eva:alarm] unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning:
Neither code nor specification for function printf1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
[eva:alarm] unravel-variance.i:53: Warning:
overflow in conversion from floating-point to integer.
assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning:
Neither code nor specification for function printf2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
[eva:alarm] unravel-variance.i:54: Warning:
overflow in conversion from floating-point to integer.
assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning:
Neither code nor specification for function printf3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
[eva:alarm] unravel-variance.i:55: Warning:
overflow in conversion from floating-point to integer.
assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning:
Neither code nor specification for function printf4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
[eva:alarm] unravel-variance.i:56: Warning:
overflow in conversion from floating-point to integer.
assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning:
Neither code nor specification for function printf5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.1.res.oracle b/tests/slicing/oracle/unravel-variance.1.res.oracle
index 3c0aeed5612..2deb200cd14 100644
--- a/tests/slicing/oracle/unravel-variance.1.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.1.res.oracle
@@ -5,7 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning:
Neither code nor specification for function scanf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
[eva:alarm] unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning:
Neither code nor specification for function printf1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
[eva:alarm] unravel-variance.i:53: Warning:
overflow in conversion from floating-point to integer.
assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning:
Neither code nor specification for function printf2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
[eva:alarm] unravel-variance.i:54: Warning:
overflow in conversion from floating-point to integer.
assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning:
Neither code nor specification for function printf3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
[eva:alarm] unravel-variance.i:55: Warning:
overflow in conversion from floating-point to integer.
assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning:
Neither code nor specification for function printf4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
[eva:alarm] unravel-variance.i:56: Warning:
overflow in conversion from floating-point to integer.
assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning:
Neither code nor specification for function printf5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.2.res.oracle b/tests/slicing/oracle/unravel-variance.2.res.oracle
index 5f609480148..f6734df8ff5 100644
--- a/tests/slicing/oracle/unravel-variance.2.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.2.res.oracle
@@ -5,7 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning:
Neither code nor specification for function scanf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
[eva:alarm] unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning:
Neither code nor specification for function printf1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
[eva:alarm] unravel-variance.i:53: Warning:
overflow in conversion from floating-point to integer.
assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning:
Neither code nor specification for function printf2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
[eva:alarm] unravel-variance.i:54: Warning:
overflow in conversion from floating-point to integer.
assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning:
Neither code nor specification for function printf3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
[eva:alarm] unravel-variance.i:55: Warning:
overflow in conversion from floating-point to integer.
assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning:
Neither code nor specification for function printf4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
[eva:alarm] unravel-variance.i:56: Warning:
overflow in conversion from floating-point to integer.
assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning:
Neither code nor specification for function printf5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.3.res.oracle b/tests/slicing/oracle/unravel-variance.3.res.oracle
index 15cdd9f5420..dfb4b2c3bd6 100644
--- a/tests/slicing/oracle/unravel-variance.3.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.3.res.oracle
@@ -5,7 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning:
Neither code nor specification for function scanf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
[eva:alarm] unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning:
Neither code nor specification for function printf1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
[eva:alarm] unravel-variance.i:53: Warning:
overflow in conversion from floating-point to integer.
assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning:
Neither code nor specification for function printf2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
[eva:alarm] unravel-variance.i:54: Warning:
overflow in conversion from floating-point to integer.
assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning:
Neither code nor specification for function printf3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
[eva:alarm] unravel-variance.i:55: Warning:
overflow in conversion from floating-point to integer.
assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning:
Neither code nor specification for function printf4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
[eva:alarm] unravel-variance.i:56: Warning:
overflow in conversion from floating-point to integer.
assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning:
Neither code nor specification for function printf5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/unravel-variance.4.res.oracle b/tests/slicing/oracle/unravel-variance.4.res.oracle
index 556f2cf86e0..60f4918fed8 100644
--- a/tests/slicing/oracle/unravel-variance.4.res.oracle
+++ b/tests/slicing/oracle/unravel-variance.4.res.oracle
@@ -5,7 +5,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] unravel-variance.i:10: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:31: Warning:
Neither code nor specification for function scanf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function scanf <- main.
@@ -123,7 +123,7 @@
[eva:alarm] unravel-variance.i:52: Warning:
overflow in conversion from floating-point to integer.
assert var2 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:11: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:52: Warning:
Neither code nor specification for function printf1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf1 <- main.
@@ -136,7 +136,7 @@
[eva:alarm] unravel-variance.i:53: Warning:
overflow in conversion from floating-point to integer.
assert var3 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:12: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:53: Warning:
Neither code nor specification for function printf2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf2 <- main.
@@ -149,7 +149,7 @@
[eva:alarm] unravel-variance.i:54: Warning:
overflow in conversion from floating-point to integer.
assert var4 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:13: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:54: Warning:
Neither code nor specification for function printf3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf3 <- main.
@@ -162,7 +162,7 @@
[eva:alarm] unravel-variance.i:55: Warning:
overflow in conversion from floating-point to integer.
assert var5 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:14: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:55: Warning:
Neither code nor specification for function printf4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf4 <- main.
@@ -175,7 +175,7 @@
[eva:alarm] unravel-variance.i:56: Warning:
overflow in conversion from floating-point to integer.
assert var1 < 2147483648;
-[kernel:annot:missing-spec] unravel-variance.i:15: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:56: Warning:
Neither code nor specification for function printf5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function printf5 <- main.
diff --git a/tests/slicing/oracle/variadic.0.res.oracle b/tests/slicing/oracle/variadic.0.res.oracle
index 9606c29d72d..8c405ab8eb8 100644
--- a/tests/slicing/oracle/variadic.0.res.oracle
+++ b/tests/slicing/oracle/variadic.0.res.oracle
@@ -8,7 +8,7 @@
[eva] computing for function f1 <- main.
Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning:
Neither code nor specification for function lib_f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.1.res.oracle b/tests/slicing/oracle/variadic.1.res.oracle
index 14aaddde6b5..532c28c2066 100644
--- a/tests/slicing/oracle/variadic.1.res.oracle
+++ b/tests/slicing/oracle/variadic.1.res.oracle
@@ -8,7 +8,7 @@
[eva] computing for function f1 <- main.
Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning:
Neither code nor specification for function lib_f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.2.res.oracle b/tests/slicing/oracle/variadic.2.res.oracle
index b0835a0cf75..8650b514d9c 100644
--- a/tests/slicing/oracle/variadic.2.res.oracle
+++ b/tests/slicing/oracle/variadic.2.res.oracle
@@ -8,7 +8,7 @@
[eva] computing for function f1 <- main.
Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning:
Neither code nor specification for function lib_f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.3.res.oracle b/tests/slicing/oracle/variadic.3.res.oracle
index aa3e4f78d17..c8160927ebc 100644
--- a/tests/slicing/oracle/variadic.3.res.oracle
+++ b/tests/slicing/oracle/variadic.3.res.oracle
@@ -8,7 +8,7 @@
[eva] computing for function f1 <- main.
Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning:
Neither code nor specification for function lib_f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/slicing/oracle/variadic.4.res.oracle b/tests/slicing/oracle/variadic.4.res.oracle
index aa3e4f78d17..c8160927ebc 100644
--- a/tests/slicing/oracle/variadic.4.res.oracle
+++ b/tests/slicing/oracle/variadic.4.res.oracle
@@ -8,7 +8,7 @@
[eva] computing for function f1 <- main.
Called from tests/pdg/variadic.c:37.
-[kernel:annot:missing-spec] tests/pdg/variadic.c:20: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:23: Warning:
Neither code nor specification for function lib_f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function lib_f <- f1 <- main.
diff --git a/tests/sparecode/oracle/bts334.0.res.oracle b/tests/sparecode/oracle/bts334.0.res.oracle
index c23af3da53b..046c3ca1741 100644
--- a/tests/sparecode/oracle/bts334.0.res.oracle
+++ b/tests/sparecode/oracle/bts334.0.res.oracle
@@ -12,7 +12,7 @@
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
-[kernel:annot:missing-spec] bts334.i:61: Warning:
+[kernel:annot:missing-spec] bts334.i:66: Warning:
Neither code nor explicit assigns for function init,
generating default clauses from the specification. See -generated-spec-* options for more info
[eva] computing for function init <- main_init.
diff --git a/tests/sparecode/oracle/bts334.1.res.oracle b/tests/sparecode/oracle/bts334.1.res.oracle
index 28c6ec682d7..2f9cd063399 100644
--- a/tests/sparecode/oracle/bts334.1.res.oracle
+++ b/tests/sparecode/oracle/bts334.1.res.oracle
@@ -12,7 +12,7 @@
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
-[kernel:annot:missing-spec] bts334.i:61: Warning:
+[kernel:annot:missing-spec] bts334.i:66: Warning:
Neither code nor explicit assigns for function init,
generating default clauses from the specification. See -generated-spec-* options for more info
[eva] computing for function init <- main_init.
diff --git a/tests/sparecode/oracle/bts334.2.res.oracle b/tests/sparecode/oracle/bts334.2.res.oracle
index 96192455136..d88f06cdf73 100644
--- a/tests/sparecode/oracle/bts334.2.res.oracle
+++ b/tests/sparecode/oracle/bts334.2.res.oracle
@@ -11,7 +11,7 @@
s1 ∈ {0}
si[0..1] ∈ {0}
so[0..1] ∈ {0}
-[kernel:annot:missing-spec] bts334.i:61: Warning:
+[kernel:annot:missing-spec] bts334.i:66: Warning:
Neither code nor explicit assigns for function init,
generating default clauses from the specification. See -generated-spec-* options for more info
[eva] computing for function init <- main_init.
diff --git a/tests/sparecode/oracle/intra.0.res.oracle b/tests/sparecode/oracle/intra.0.res.oracle
index f8b3fcdd631..88889b31a6e 100644
--- a/tests/sparecode/oracle/intra.0.res.oracle
+++ b/tests/sparecode/oracle/intra.0.res.oracle
@@ -49,7 +49,7 @@
Called from intra.i:88.
[eva] Recording results for assign
[eva] Done for function assign
-[kernel:annot:missing-spec] intra.i:73: Warning:
+[kernel:annot:missing-spec] intra.i:91: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- main.
diff --git a/tests/sparecode/oracle/intra.1.res.oracle b/tests/sparecode/oracle/intra.1.res.oracle
index 4dc9557ce91..340b1dc3072 100644
--- a/tests/sparecode/oracle/intra.1.res.oracle
+++ b/tests/sparecode/oracle/intra.1.res.oracle
@@ -48,7 +48,7 @@
Called from intra.i:88.
[eva] Recording results for assign
[eva] Done for function assign
-[kernel:annot:missing-spec] intra.i:73: Warning:
+[kernel:annot:missing-spec] intra.i:91: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- main.
diff --git a/tests/sparecode/oracle/top.1.res.oracle b/tests/sparecode/oracle/top.1.res.oracle
index f2b7c795783..63bea7f723a 100644
--- a/tests/sparecode/oracle/top.1.res.oracle
+++ b/tests/sparecode/oracle/top.1.res.oracle
@@ -16,7 +16,7 @@
[eva] Done for function main_top
[eva] computing for function not_used_in_main_top <- main_call_top.
Called from top.i:27.
-[kernel:annot:missing-spec] top.i:7: Warning:
+[kernel:annot:missing-spec] top.i:10: Warning:
Neither code nor specification for function print,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function print <- not_used_in_main_top <- main_call_top.
diff --git a/tests/spec/oracle/assigns_void.1.res.oracle b/tests/spec/oracle/assigns_void.1.res.oracle
index c3356f555ee..b978ce8605c 100644
--- a/tests/spec/oracle/assigns_void.1.res.oracle
+++ b/tests/spec/oracle/assigns_void.1.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] assigns_void.c:7: Warning:
+[kernel:annot:missing-spec] assigns_void.c:11: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- g.
diff --git a/tests/spec/oracle/default_assigns_bts0966.res.oracle b/tests/spec/oracle/default_assigns_bts0966.res.oracle
index 5e34aa21316..728ce51af93 100644
--- a/tests/spec/oracle/default_assigns_bts0966.res.oracle
+++ b/tests/spec/oracle/default_assigns_bts0966.res.oracle
@@ -2,7 +2,7 @@
[eva] Analyzing a complete application starting at main
[eva:initial-state] Values of globals at initialization
auto_states[0..3] ∈ {0}
-[kernel:annot:missing-spec] default_assigns_bts0966.i:27: Warning:
+[kernel:annot:missing-spec] default_assigns_bts0966.i:34: Warning:
Neither code nor explicit assigns for function copy,
generating default clauses from the specification. See -generated-spec-* options for more info
[eva] using specification for function copy
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index aeb161d74fb..744d7aab558 100644
--- a/tests/value/oracle/assigns.res.oracle
+++ b/tests/value/oracle/assigns.res.oracle
@@ -102,21 +102,21 @@
[eva] using specification for function ff3
[eva] assigns.i:68: Warning: no \from part for clause 'assigns y1, y3;'
[eva] Done for function ff3
-[kernel:annot:missing-spec] assigns.i:71: Warning:
+[kernel:annot:missing-spec] assigns.i:79: Warning:
Neither code nor specification for function ff4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function ff4 <- main2 <- main.
Called from assigns.i:79.
[eva] using specification for function ff4
[eva] Done for function ff4
-[kernel:annot:missing-spec] assigns.i:73: Warning:
+[kernel:annot:missing-spec] assigns.i:80: Warning:
Neither code nor specification for function ff5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function ff5 <- main2 <- main.
Called from assigns.i:80.
[eva] using specification for function ff5
[eva] Done for function ff5
-[kernel:annot:missing-spec] assigns.i:62: Warning:
+[kernel:annot:missing-spec] assigns.i:82: Warning:
Neither code nor specification for function ff2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function ff2 <- main2 <- main.
@@ -133,7 +133,7 @@
pointer comparison. assert \pointer_comparable((void *)p, (void *)(&x));
[eva] Recording results for main2
[eva] Done for function main2
-[kernel:annot:missing-spec] assigns.i:92: Warning:
+[kernel:annot:missing-spec] assigns.i:112: Warning:
Neither code nor specification for function main3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function main3 <- main.
diff --git a/tests/value/oracle/assigns_from.res.oracle b/tests/value/oracle/assigns_from.res.oracle
index d149f5e7fee..002087f31ba 100644
--- a/tests/value/oracle/assigns_from.res.oracle
+++ b/tests/value/oracle/assigns_from.res.oracle
@@ -186,7 +186,7 @@
[eva] Done for function main9
[eva] computing for function main10 <- main.
Called from assigns_from.i:244.
-[kernel:annot:missing-spec] assigns_from.i:150: Warning:
+[kernel:annot:missing-spec] assigns_from.i:152: Warning:
Neither code nor specification for function c,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function c <- main10 <- main.
diff --git a/tests/value/oracle/automalloc.res.oracle b/tests/value/oracle/automalloc.res.oracle
index d2d671709e2..d7a242da662 100644
--- a/tests/value/oracle/automalloc.res.oracle
+++ b/tests/value/oracle/automalloc.res.oracle
@@ -4,14 +4,14 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] automalloc.i:6: Warning:
+[kernel:annot:missing-spec] automalloc.i:14: Warning:
Neither code nor specification for function malloc,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function malloc <- main.
Called from automalloc.i:14.
[eva] using specification for function malloc
[eva] Done for function malloc
-[kernel:annot:missing-spec] automalloc.i:7: Warning:
+[kernel:annot:missing-spec] automalloc.i:15: Warning:
Neither code nor specification for function realloc,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function realloc <- main.
diff --git a/tests/value/oracle/behaviors1.res.oracle b/tests/value/oracle/behaviors1.res.oracle
index 1124da3762a..980bd317335 100644
--- a/tests/value/oracle/behaviors1.res.oracle
+++ b/tests/value/oracle/behaviors1.res.oracle
@@ -337,7 +337,7 @@
[eva] Done for function test_assigns2
[eva] computing for function test_small1 <- main.
Called from behaviors1.i:649.
-[kernel:annot:missing-spec] behaviors1.i:502: Warning:
+[kernel:annot:missing-spec] behaviors1.i:506: Warning:
Neither code nor explicit assigns for function f3,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f3 <- test_small1 <- main.
@@ -352,7 +352,7 @@
[eva] Done for function test_small1
[eva] computing for function test_small2 <- main.
Called from behaviors1.i:650.
-[kernel:annot:missing-spec] behaviors1.i:517: Warning:
+[kernel:annot:missing-spec] behaviors1.i:521: Warning:
Neither code nor explicit assigns for function f4,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f4 <- test_small2 <- main.
@@ -371,7 +371,7 @@
[eva] Done for function test_small2
[eva] computing for function test_small3 <- main.
Called from behaviors1.i:651.
-[kernel:annot:missing-spec] behaviors1.i:531: Warning:
+[kernel:annot:missing-spec] behaviors1.i:534: Warning:
Neither code nor explicit assigns for function f5,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f5 <- test_small3 <- main.
@@ -382,7 +382,7 @@
[eva] Done for function test_small3
[eva] computing for function test_small4 <- main.
Called from behaviors1.i:652.
-[kernel:annot:missing-spec] behaviors1.i:545: Warning:
+[kernel:annot:missing-spec] behaviors1.i:548: Warning:
Neither code nor explicit assigns for function f6,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f6 <- test_small4 <- main.
@@ -393,7 +393,7 @@
[eva] Done for function test_small4
[eva] computing for function test_small5 <- main.
Called from behaviors1.i:653.
-[kernel:annot:missing-spec] behaviors1.i:558: Warning:
+[kernel:annot:missing-spec] behaviors1.i:561: Warning:
Neither code nor explicit assigns for function f7,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f7 <- test_small5 <- main.
diff --git a/tests/value/oracle/bitfield.res.oracle b/tests/value/oracle/bitfield.res.oracle
index 4562b5e6847..45acf789580 100644
--- a/tests/value/oracle/bitfield.res.oracle
+++ b/tests/value/oracle/bitfield.res.oracle
@@ -99,7 +99,7 @@
locals {v} escaping the scope of main_old through h
[eva] computing for function imprecise_bts_1671 <- main.
Called from bitfield.i:165.
-[kernel:annot:missing-spec] bitfield.i:61: Warning:
+[kernel:annot:missing-spec] bitfield.i:70: Warning:
Neither code nor specification for function leaf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function leaf <- imprecise_bts_1671 <- main.
diff --git a/tests/value/oracle/bts0506.0.res.oracle b/tests/value/oracle/bts0506.0.res.oracle
index f627390df62..c372fd704f0 100644
--- a/tests/value/oracle/bts0506.0.res.oracle
+++ b/tests/value/oracle/bts0506.0.res.oracle
@@ -10,7 +10,7 @@
[eva] Done for function f
[eva] computing for function main2 <- main.
Called from bts0506.i:49.
-[kernel:annot:missing-spec] bts0506.i:6: Warning:
+[kernel:annot:missing-spec] bts0506.i:15: Warning:
Neither code nor specification for function f1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f1 <- main2 <- main.
@@ -26,7 +26,7 @@
[eva] computing for function f1 <- main2 <- main.
Called from bts0506.i:18.
[eva] Done for function f1
-[kernel:annot:missing-spec] bts0506.i:7: Warning:
+[kernel:annot:missing-spec] bts0506.i:20: Warning:
Neither code nor specification for function f2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f2 <- main2 <- main.
@@ -39,7 +39,7 @@
[eva] computing for function f2 <- main2 <- main.
Called from bts0506.i:22.
[eva] Done for function f2
-[kernel:annot:missing-spec] bts0506.i:8: Warning:
+[kernel:annot:missing-spec] bts0506.i:24: Warning:
Neither code nor specification for function f3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f3 <- main2 <- main.
@@ -49,7 +49,7 @@
[eva] computing for function f3 <- main2 <- main.
Called from bts0506.i:25.
[eva] Done for function f3
-[kernel:annot:missing-spec] bts0506.i:9: Warning:
+[kernel:annot:missing-spec] bts0506.i:27: Warning:
Neither code nor specification for function f4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f4 <- main2 <- main.
@@ -65,7 +65,7 @@
[eva:alarm] bts0506.i:28: Warning:
non-finite float value. assert \is_finite(tmp_9);
(tmp_9 from f4())
-[kernel:annot:missing-spec] bts0506.i:10: Warning:
+[kernel:annot:missing-spec] bts0506.i:30: Warning:
Neither code nor specification for function f5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f5 <- main2 <- main.
@@ -84,7 +84,7 @@
[eva:alarm] bts0506.i:31: Warning:
non-finite double value. assert \is_finite(tmp_11);
(tmp_11 from f5())
-[kernel:annot:missing-spec] bts0506.i:11: Warning:
+[kernel:annot:missing-spec] bts0506.i:33: Warning:
Neither code nor specification for function f6,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f6 <- main2 <- main.
@@ -97,7 +97,7 @@
[eva] computing for function f6 <- main2 <- main.
Called from bts0506.i:35.
[eva] Done for function f6
-[kernel:annot:missing-spec] bts0506.i:12: Warning:
+[kernel:annot:missing-spec] bts0506.i:37: Warning:
Neither code nor specification for function f7,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f7 <- main2 <- main.
diff --git a/tests/value/oracle/bts0506.1.res.oracle b/tests/value/oracle/bts0506.1.res.oracle
index 468b9221629..715ab663ac3 100644
--- a/tests/value/oracle/bts0506.1.res.oracle
+++ b/tests/value/oracle/bts0506.1.res.oracle
@@ -10,7 +10,7 @@
[eva] Done for function f
[eva] computing for function main2 <- main.
Called from bts0506.i:49.
-[kernel:annot:missing-spec] bts0506.i:6: Warning:
+[kernel:annot:missing-spec] bts0506.i:15: Warning:
Neither code nor specification for function f1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f1 <- main2 <- main.
@@ -26,7 +26,7 @@
[eva] computing for function f1 <- main2 <- main.
Called from bts0506.i:18.
[eva] Done for function f1
-[kernel:annot:missing-spec] bts0506.i:7: Warning:
+[kernel:annot:missing-spec] bts0506.i:20: Warning:
Neither code nor specification for function f2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f2 <- main2 <- main.
@@ -39,7 +39,7 @@
[eva] computing for function f2 <- main2 <- main.
Called from bts0506.i:22.
[eva] Done for function f2
-[kernel:annot:missing-spec] bts0506.i:8: Warning:
+[kernel:annot:missing-spec] bts0506.i:24: Warning:
Neither code nor specification for function f3,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f3 <- main2 <- main.
@@ -49,7 +49,7 @@
[eva] computing for function f3 <- main2 <- main.
Called from bts0506.i:25.
[eva] Done for function f3
-[kernel:annot:missing-spec] bts0506.i:9: Warning:
+[kernel:annot:missing-spec] bts0506.i:27: Warning:
Neither code nor specification for function f4,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f4 <- main2 <- main.
@@ -62,7 +62,7 @@
[eva:alarm] bts0506.i:28: Warning:
non-finite float value. assert \is_finite(tmp_9);
(tmp_9 from f4())
-[kernel:annot:missing-spec] bts0506.i:10: Warning:
+[kernel:annot:missing-spec] bts0506.i:30: Warning:
Neither code nor specification for function f5,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f5 <- main2 <- main.
@@ -78,7 +78,7 @@
[eva] computing for function f5 <- main2 <- main.
Called from bts0506.i:31.
[eva] Done for function f5
-[kernel:annot:missing-spec] bts0506.i:11: Warning:
+[kernel:annot:missing-spec] bts0506.i:33: Warning:
Neither code nor specification for function f6,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f6 <- main2 <- main.
@@ -91,7 +91,7 @@
[eva] computing for function f6 <- main2 <- main.
Called from bts0506.i:35.
[eva] Done for function f6
-[kernel:annot:missing-spec] bts0506.i:12: Warning:
+[kernel:annot:missing-spec] bts0506.i:37: Warning:
Neither code nor specification for function f7,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f7 <- main2 <- main.
diff --git a/tests/value/oracle/bug0223.0.res.oracle b/tests/value/oracle/bug0223.0.res.oracle
index 07c96593eb8..2621ac4b4de 100644
--- a/tests/value/oracle/bug0223.0.res.oracle
+++ b/tests/value/oracle/bug0223.0.res.oracle
@@ -7,7 +7,7 @@
ch2 ∈ {{ NULL ; &S_ch2[0] }}
S_ch1[0..1] ∈ [--..--]
S_ch2[0..1] ∈ [--..--]
-[kernel:annot:missing-spec] bug0223.i:9: Warning:
+[kernel:annot:missing-spec] bug0223.i:33: Warning:
Neither code nor specification for function F,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function F <- main.
@@ -19,7 +19,7 @@
[eva] Done for function F
[eva] computing for function h2 <- main.
Called from bug0223.i:35.
-[kernel:annot:missing-spec] bug0223.i:11: Warning:
+[kernel:annot:missing-spec] bug0223.i:16: Warning:
Neither code nor specification for function my_strcnmp,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function my_strcnmp <- h2 <- main.
diff --git a/tests/value/oracle/bug0223.1.res.oracle b/tests/value/oracle/bug0223.1.res.oracle
index 07c96593eb8..2621ac4b4de 100644
--- a/tests/value/oracle/bug0223.1.res.oracle
+++ b/tests/value/oracle/bug0223.1.res.oracle
@@ -7,7 +7,7 @@
ch2 ∈ {{ NULL ; &S_ch2[0] }}
S_ch1[0..1] ∈ [--..--]
S_ch2[0..1] ∈ [--..--]
-[kernel:annot:missing-spec] bug0223.i:9: Warning:
+[kernel:annot:missing-spec] bug0223.i:33: Warning:
Neither code nor specification for function F,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function F <- main.
@@ -19,7 +19,7 @@
[eva] Done for function F
[eva] computing for function h2 <- main.
Called from bug0223.i:35.
-[kernel:annot:missing-spec] bug0223.i:11: Warning:
+[kernel:annot:missing-spec] bug0223.i:16: Warning:
Neither code nor specification for function my_strcnmp,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function my_strcnmp <- h2 <- main.
diff --git a/tests/value/oracle/bug_023.res.oracle b/tests/value/oracle/bug_023.res.oracle
index c6369e819e1..ab536314a0f 100644
--- a/tests/value/oracle/bug_023.res.oracle
+++ b/tests/value/oracle/bug_023.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
i ∈ {0}
x ∈ {0}
-[kernel:annot:missing-spec] bug_023.i:4: Warning:
+[kernel:annot:missing-spec] bug_023.i:8: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/value/oracle/call.res.oracle b/tests/value/oracle/call.res.oracle
index 71179e982ca..c81599c1696 100644
--- a/tests/value/oracle/call.res.oracle
+++ b/tests/value/oracle/call.res.oracle
@@ -11,7 +11,7 @@
[eva:alarm] call.i:19: Warning: out of bounds read. assert \valid_read(v + 1);
[eva:alarm] call.i:19: Warning:
pointer downcast. assert (unsigned int)*(v + 1) ≤ 2147483647;
-[kernel:annot:missing-spec] call.i:10: Warning:
+[kernel:annot:missing-spec] call.i:19: Warning:
Neither code nor specification for function leaf_fun_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function leaf_fun_int <- main.
@@ -19,7 +19,7 @@
[eva] using specification for function leaf_fun_int
[eva] Done for function leaf_fun_int
[eva:alarm] call.i:20: Warning: out of bounds read. assert \valid_read(v + 1);
-[kernel:annot:missing-spec] call.i:11: Warning:
+[kernel:annot:missing-spec] call.i:20: Warning:
Neither code nor specification for function leaf_fun_charp,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function leaf_fun_charp <- main.
diff --git a/tests/value/oracle/copy_stdin.res.oracle b/tests/value/oracle/copy_stdin.res.oracle
index 8ad9af9913f..2535d55b3d4 100644
--- a/tests/value/oracle/copy_stdin.res.oracle
+++ b/tests/value/oracle/copy_stdin.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] copy_stdin.i:1: Warning:
+[kernel:annot:missing-spec] copy_stdin.i:4: Warning:
Neither code nor specification for function leaf,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function leaf <- main.
diff --git a/tests/value/oracle/empty_struct.6.res.oracle b/tests/value/oracle/empty_struct.6.res.oracle
index 506b771445b..c67a99bfed4 100644
--- a/tests/value/oracle/empty_struct.6.res.oracle
+++ b/tests/value/oracle/empty_struct.6.res.oracle
@@ -12,7 +12,7 @@
[eva:garbled-mix:write] empty_struct.c:99:
Assigning imprecise value to r.
The imprecision originates from Library function {empty_struct.c:99}
-[kernel:annot:missing-spec] empty_struct.c:96: Warning:
+[kernel:annot:missing-spec] empty_struct.c:100: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main4.
diff --git a/tests/value/oracle/f1.res.oracle b/tests/value/oracle/f1.res.oracle
index b34af541127..fef780748fe 100644
--- a/tests/value/oracle/f1.res.oracle
+++ b/tests/value/oracle/f1.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] f1.i:2: Warning:
+[kernel:annot:missing-spec] f1.i:5: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/value/oracle/false.res.oracle b/tests/value/oracle/false.res.oracle
index 20f02f2e444..7ea38337faf 100644
--- a/tests/value/oracle/false.res.oracle
+++ b/tests/value/oracle/false.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] false.i:8: Warning:
+[kernel:annot:missing-spec] false.i:18: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/value/oracle/from_call.0.res.oracle b/tests/value/oracle/from_call.0.res.oracle
index c466d2d8ad7..88c6c5d8c6d 100644
--- a/tests/value/oracle/from_call.0.res.oracle
+++ b/tests/value/oracle/from_call.0.res.oracle
@@ -44,7 +44,7 @@
f_previous ∈ {{ &a }}
[eva] computing for function f <- main.
Called from from_call.i:81.
-[kernel:annot:missing-spec] from_call.i:13: Warning:
+[kernel:annot:missing-spec] from_call.i:20: Warning:
Neither code nor specification for function h,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function h <- f <- main.
diff --git a/tests/value/oracle/from_call.1.res.oracle b/tests/value/oracle/from_call.1.res.oracle
index da40280de1d..560d21d929a 100644
--- a/tests/value/oracle/from_call.1.res.oracle
+++ b/tests/value/oracle/from_call.1.res.oracle
@@ -44,7 +44,7 @@
f_previous ∈ {{ &a }}
[eva] computing for function f <- main.
Called from from_call.i:81.
-[kernel:annot:missing-spec] from_call.i:13: Warning:
+[kernel:annot:missing-spec] from_call.i:20: Warning:
Neither code nor specification for function h,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function h <- f <- main.
diff --git a/tests/value/oracle/ineq.res.oracle b/tests/value/oracle/ineq.res.oracle
index c2f6e5229f4..38ed36b32a0 100644
--- a/tests/value/oracle/ineq.res.oracle
+++ b/tests/value/oracle/ineq.res.oracle
@@ -12,7 +12,7 @@
l ∈ {1}
m ∈ {-1}
n ∈ {-1}
-[kernel:annot:missing-spec] ineq.c:1: Warning:
+[kernel:annot:missing-spec] ineq.c:6: Warning:
Neither code nor specification for function any_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function any_int <- main.
diff --git a/tests/value/oracle/infinite.res.oracle b/tests/value/oracle/infinite.res.oracle
index 127ab211d4d..e43d5267297 100644
--- a/tests/value/oracle/infinite.res.oracle
+++ b/tests/value/oracle/infinite.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
G ∈ {0}
-[kernel:annot:missing-spec] infinite.i:1: Warning:
+[kernel:annot:missing-spec] infinite.i:9: Warning:
Neither code nor specification for function pause,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function pause <- main.
diff --git a/tests/value/oracle/initialized_copy.0.res.oracle b/tests/value/oracle/initialized_copy.0.res.oracle
index 7320a7432c7..fec4520ecd5 100644
--- a/tests/value/oracle/initialized_copy.0.res.oracle
+++ b/tests/value/oracle/initialized_copy.0.res.oracle
@@ -96,7 +96,7 @@
==END OF DUMP==
[eva:alarm] initialized_copy.i:151: Warning:
accessing uninitialized left-value. assert \initialized(&a_8);
-[kernel:annot:missing-spec] initialized_copy.i:22: Warning:
+[kernel:annot:missing-spec] initialized_copy.i:151: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/initialized_copy.1.res.oracle b/tests/value/oracle/initialized_copy.1.res.oracle
index 878a548361d..1677d41e752 100644
--- a/tests/value/oracle/initialized_copy.1.res.oracle
+++ b/tests/value/oracle/initialized_copy.1.res.oracle
@@ -88,7 +88,7 @@
==END OF DUMP==
[eva:alarm] initialized_copy.i:151: Warning:
accessing uninitialized left-value. assert \initialized(&a_8);
-[kernel:annot:missing-spec] initialized_copy.i:22: Warning:
+[kernel:annot:missing-spec] initialized_copy.i:151: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/input.res.oracle b/tests/value/oracle/input.res.oracle
index bbd39cd72e4..541d5189697 100644
--- a/tests/value/oracle/input.res.oracle
+++ b/tests/value/oracle/input.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
a ∈ {0}
b ∈ {0}
-[kernel:annot:missing-spec] input.i:1: Warning:
+[kernel:annot:missing-spec] input.i:7: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index a233e82216b..7ccd5e0302a 100644
--- a/tests/value/oracle/leaf.res.oracle
+++ b/tests/value/oracle/leaf.res.oracle
@@ -29,7 +29,7 @@
st_tab3_int_3.t[0] ∈ {30}
.t[1] ∈ {31}
.t[2] ∈ {32}
-[kernel:annot:missing-spec] leaf.i:3: Warning:
+[kernel:annot:missing-spec] leaf.i:48: Warning:
Neither code nor specification for function f_int_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_int_int <- main.
@@ -57,35 +57,35 @@
[eva] leaf.i:57: Frama_C_show_each_F: {5}
[eva] leaf.i:59: Frama_C_show_each_G: {{ &g }}
[eva] leaf.i:60: Frama_C_show_each_F: {5}
-[kernel:annot:missing-spec] leaf.i:14: Warning:
+[kernel:annot:missing-spec] leaf.i:62: Warning:
Neither code nor specification for function f_star_int_cint,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_star_int_cint <- main.
Called from leaf.i:62.
[eva] using specification for function f_star_int_cint
[eva] Done for function f_star_int_cint
-[kernel:annot:missing-spec] leaf.i:17: Warning:
+[kernel:annot:missing-spec] leaf.i:64: Warning:
Neither code nor specification for function f_star_int_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_star_int_int <- main.
Called from leaf.i:64.
[eva] using specification for function f_star_int_int
[eva] Done for function f_star_int_int
-[kernel:annot:missing-spec] leaf.i:19: Warning:
+[kernel:annot:missing-spec] leaf.i:65: Warning:
Neither code nor specification for function f_tab3_int_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_tab3_int_int <- main.
Called from leaf.i:65.
[eva] using specification for function f_tab3_int_int
[eva] Done for function f_tab3_int_int
-[kernel:annot:missing-spec] leaf.i:18: Warning:
+[kernel:annot:missing-spec] leaf.i:66: Warning:
Neither code nor specification for function f_tab_int_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_tab_int_int <- main.
Called from leaf.i:66.
[eva] using specification for function f_tab_int_int
[eva] Done for function f_tab_int_int
-[kernel:annot:missing-spec] leaf.i:38: Warning:
+[kernel:annot:missing-spec] leaf.i:68: Warning:
Neither code nor specification for function f_st_star_cint_st_star_cint,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_st_star_cint_st_star_cint <- main.
@@ -95,7 +95,7 @@
[eva:garbled-mix:write] leaf.i:68:
Assigning imprecise value to st_star_cint_1.
The imprecision originates from Library function {leaf.i:68}
-[kernel:annot:missing-spec] leaf.i:39: Warning:
+[kernel:annot:missing-spec] leaf.i:69: Warning:
Neither code nor specification for function f_st_star_int_st_star_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_st_star_int_st_star_int <- main.
@@ -105,28 +105,28 @@
[eva:garbled-mix:write] leaf.i:69:
Assigning imprecise value to st_star_int_1.
The imprecision originates from Library function {leaf.i:69}
-[kernel:annot:missing-spec] leaf.i:40: Warning:
+[kernel:annot:missing-spec] leaf.i:70: Warning:
Neither code nor specification for function f_st_tab3_int_st_tab3_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_st_tab3_int_st_tab3_int <- main.
Called from leaf.i:70.
[eva] using specification for function f_st_tab3_int_st_tab3_int
[eva] Done for function f_st_tab3_int_st_tab3_int
-[kernel:annot:missing-spec] leaf.i:42: Warning:
+[kernel:annot:missing-spec] leaf.i:72: Warning:
Neither code nor specification for function f_star_st_star_cint_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_star_st_star_cint_int <- main.
Called from leaf.i:72.
[eva] using specification for function f_star_st_star_cint_int
[eva] Done for function f_star_st_star_cint_int
-[kernel:annot:missing-spec] leaf.i:43: Warning:
+[kernel:annot:missing-spec] leaf.i:73: Warning:
Neither code nor specification for function f_star_st_star_int_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_star_st_star_int_int <- main.
Called from leaf.i:73.
[eva] using specification for function f_star_st_star_int_int
[eva] Done for function f_star_st_star_int_int
-[kernel:annot:missing-spec] leaf.i:44: Warning:
+[kernel:annot:missing-spec] leaf.i:74: Warning:
Neither code nor specification for function f_star_st_tab3_int_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_star_st_tab3_int_int <- main.
diff --git a/tests/value/oracle/leaf2.res.oracle b/tests/value/oracle/leaf2.res.oracle
index 640d666d561..3f486d154c0 100644
--- a/tests/value/oracle/leaf2.res.oracle
+++ b/tests/value/oracle/leaf2.res.oracle
@@ -8,7 +8,7 @@
I ∈ {0}
[eva:alarm] leaf2.i:6: Warning:
pointer downcast. assert (unsigned int)(&I) ≤ 2147483647;
-[kernel:annot:missing-spec] leaf2.i:2: Warning:
+[kernel:annot:missing-spec] leaf2.i:6: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/value/oracle/leaf_spec.0.res.oracle b/tests/value/oracle/leaf_spec.0.res.oracle
index 7adfce4bcc8..9d1932aa482 100644
--- a/tests/value/oracle/leaf_spec.0.res.oracle
+++ b/tests/value/oracle/leaf_spec.0.res.oracle
@@ -4,28 +4,28 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] leaf_spec.i:9: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:19: Warning:
Neither code nor specification for function f1,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f1 <- main.
Called from leaf_spec.i:19.
[eva] using specification for function f1
[eva] Done for function f1
-[kernel:annot:missing-spec] leaf_spec.i:11: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:20: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
Called from leaf_spec.i:20.
[eva] using specification for function g
[eva] Done for function g
-[kernel:annot:missing-spec] leaf_spec.i:13: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:21: Warning:
Neither code nor specification for function h,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function h <- main.
Called from leaf_spec.i:21.
[eva] using specification for function h
[eva] Done for function h
-[kernel:annot:missing-spec] leaf_spec.i:15: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:22: Warning:
Neither code nor specification for function k,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function k <- main.
@@ -34,7 +34,7 @@
[eva:invalid-assigns] leaf_spec.i:22:
Completely invalid destination for assigns clause *l. Ignoring.
[eva] Done for function k
-[kernel:annot:missing-spec] leaf_spec.i:16: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:22: Warning:
Neither code nor specification for function k0,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function k0 <- main.
diff --git a/tests/value/oracle/leaf_spec.1.res.oracle b/tests/value/oracle/leaf_spec.1.res.oracle
index 91821a7fba1..f47d633f23a 100644
--- a/tests/value/oracle/leaf_spec.1.res.oracle
+++ b/tests/value/oracle/leaf_spec.1.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] leaf_spec.i:6: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:27: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main1.
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index adccceb6d27..3a3a113d638 100644
--- a/tests/value/oracle/library.res.oracle
+++ b/tests/value/oracle/library.res.oracle
@@ -76,7 +76,7 @@
S_1_0_S_q_ss[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
S_0_1_S_q_ss[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
S_1_1_S_q_ss[bits 0 to ..] ∈ [--..--] or UNINITIALIZED
-[kernel:annot:missing-spec] library.i:5: Warning:
+[kernel:annot:missing-spec] library.i:30: Warning:
Neither code nor specification for function f_int,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f_int <- main.
@@ -96,7 +96,7 @@
[eva:alarm] library.i:33: Warning:
out of bounds read. assert \valid_read(*(*G));
[eva:alarm] library.i:33: Warning: out of bounds write. assert \valid(*(*(*G)));
-[kernel:annot:missing-spec] library.i:18: Warning:
+[kernel:annot:missing-spec] library.i:37: Warning:
Neither code nor specification for function gen,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function gen <- main.
diff --git a/tests/value/oracle/local_variables.res.oracle b/tests/value/oracle/local_variables.res.oracle
index 5c1c6d008b5..441104cedc7 100644
--- a/tests/value/oracle/local_variables.res.oracle
+++ b/tests/value/oracle/local_variables.res.oracle
@@ -13,7 +13,7 @@
Called from local_variables.i:30.
[eva] computing for function w <- u <- main.
Called from local_variables.i:11.
-[kernel:annot:missing-spec] local_variables.i:4: Warning:
+[kernel:annot:missing-spec] local_variables.i:24: Warning:
Neither code nor specification for function unkn,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function unkn <- w <- u <- main.
diff --git a/tests/value/oracle/noreturn.res.oracle b/tests/value/oracle/noreturn.res.oracle
index c9131db1371..955ecabd508 100644
--- a/tests/value/oracle/noreturn.res.oracle
+++ b/tests/value/oracle/noreturn.res.oracle
@@ -16,14 +16,14 @@
Called from noreturn.i:28.
[eva] Recording results for warn_never_ends
[eva] Done for function warn_never_ends
-[kernel:annot:missing-spec] noreturn.i:1: Warning:
+[kernel:annot:missing-spec] noreturn.i:29: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function stop <- main.
Called from noreturn.i:29.
[eva] using specification for function stop
[eva] Done for function stop
-[kernel:annot:missing-spec] noreturn.i:3: Warning:
+[kernel:annot:missing-spec] noreturn.i:30: Warning:
Neither code nor specification for function haltme,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function haltme <- main.
diff --git a/tests/value/oracle/origin.0.res.oracle b/tests/value/oracle/origin.0.res.oracle
index a14d8d6d471..21313b3be75 100644
--- a/tests/value/oracle/origin.0.res.oracle
+++ b/tests/value/oracle/origin.0.res.oracle
@@ -110,7 +110,7 @@
[eva] Done for function origin_arithmetic_3
[eva] computing for function origin_leaf_1 <- main.
Called from origin.i:97.
-[kernel:annot:missing-spec] origin.i:30: Warning:
+[kernel:annot:missing-spec] origin.i:38: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- origin_leaf_1 <- main.
diff --git a/tests/value/oracle/origin.1.res.oracle b/tests/value/oracle/origin.1.res.oracle
index a6bb3080bd7..2d7eae48a93 100644
--- a/tests/value/oracle/origin.1.res.oracle
+++ b/tests/value/oracle/origin.1.res.oracle
@@ -52,7 +52,7 @@
.t[0] ∈ {{ &y }}
.t[1] ∈ {0}
S_gpp[0..1] ∈ [--..--]
-[kernel:annot:missing-spec] origin.i:7: Warning:
+[kernel:annot:missing-spec] origin.i:124: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- origin.
diff --git a/tests/value/oracle/output_leafs.res.oracle b/tests/value/oracle/output_leafs.res.oracle
index 928c51aa4ca..a2b97d84281 100644
--- a/tests/value/oracle/output_leafs.res.oracle
+++ b/tests/value/oracle/output_leafs.res.oracle
@@ -43,7 +43,7 @@
[eva] Done for function main2
[eva] computing for function main3 <- main.
Called from output_leafs.i:47.
-[kernel:annot:missing-spec] output_leafs.i:36: Warning:
+[kernel:annot:missing-spec] output_leafs.i:40: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main3 <- main.
diff --git a/tests/value/oracle/postcond_leaf.res.oracle b/tests/value/oracle/postcond_leaf.res.oracle
index d5444651d99..c667f6ecd05 100644
--- a/tests/value/oracle/postcond_leaf.res.oracle
+++ b/tests/value/oracle/postcond_leaf.res.oracle
@@ -3,7 +3,7 @@
[eva:initial-state] Values of globals at initialization
i ∈ [--..--]
j ∈ [--..--]
-[kernel:annot:missing-spec] postcond_leaf.c:22: Warning:
+[kernel:annot:missing-spec] postcond_leaf.c:109: Warning:
Neither code nor explicit assigns for function f1,
generating default clauses. See -generated-spec-* options for more info
[eva] using specification for function f1
diff --git a/tests/value/oracle/postcondition.res.oracle b/tests/value/oracle/postcondition.res.oracle
index d1287f10cc7..fcfd148f70a 100644
--- a/tests/value/oracle/postcondition.res.oracle
+++ b/tests/value/oracle/postcondition.res.oracle
@@ -17,7 +17,7 @@
Called from postcondition.i:84.
[eva] postcondition.i:84: function get_index: precondition got status valid.
[eva] postcondition.i:17: Frama_C_show_each_cmd: {1}
-[kernel:annot:missing-spec] postcondition.i:5: Warning:
+[kernel:annot:missing-spec] postcondition.i:20: Warning:
Neither code nor explicit assigns for function u,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function u <- get_index <- main.
@@ -75,7 +75,7 @@
[eva] computing for function u <- main.
Called from postcondition.i:88.
[eva] Done for function u
-[kernel:annot:missing-spec] postcondition.i:8: Warning:
+[kernel:annot:missing-spec] postcondition.i:89: Warning:
Neither code nor explicit assigns for function cap,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function cap <- main.
diff --git a/tests/value/oracle/precond.res.oracle b/tests/value/oracle/precond.res.oracle
index 450e321eef9..c7c6f73dfa1 100644
--- a/tests/value/oracle/precond.res.oracle
+++ b/tests/value/oracle/precond.res.oracle
@@ -17,7 +17,7 @@
[eva] precond.c:32: function f: precondition 'i' got status valid.
[eva] Recording results for f
[eva] Done for function f
-[kernel:annot:missing-spec] precond.c:25: Warning:
+[kernel:annot:missing-spec] precond.c:34: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function g <- main.
@@ -27,7 +27,7 @@
[eva] Done for function g
[eva] computing for function aux <- main.
Called from precond.c:36.
-[kernel:annot:missing-spec] precond.c:16: Warning:
+[kernel:annot:missing-spec] precond.c:21: Warning:
Neither code nor explicit assigns for function f2,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function f2 <- aux <- main.
diff --git a/tests/value/oracle/precond2.0.res.oracle b/tests/value/oracle/precond2.0.res.oracle
index c2f33d78730..2d9a1fc7536 100644
--- a/tests/value/oracle/precond2.0.res.oracle
+++ b/tests/value/oracle/precond2.0.res.oracle
@@ -19,7 +19,7 @@
function f: precondition 'i' got status invalid.
[eva] Recording results for f
[eva] Done for function f
-[kernel:annot:missing-spec] precond2.c:17: Warning:
+[kernel:annot:missing-spec] precond2.c:24: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/precond2.1.res.oracle b/tests/value/oracle/precond2.1.res.oracle
index 9200a22a04a..8924205852c 100644
--- a/tests/value/oracle/precond2.1.res.oracle
+++ b/tests/value/oracle/precond2.1.res.oracle
@@ -17,7 +17,7 @@
function f: precondition 'i' got status invalid.
[eva] Recording results for f
[eva] Done for function f
-[kernel:annot:missing-spec] precond2.c:17: Warning:
+[kernel:annot:missing-spec] precond2.c:24: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/resolve.res.oracle b/tests/value/oracle/resolve.res.oracle
index e17390ebcbc..d39a8926209 100644
--- a/tests/value/oracle/resolve.res.oracle
+++ b/tests/value/oracle/resolve.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] resolve.i:3: Warning:
+[kernel:annot:missing-spec] resolve.i:12: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
diff --git a/tests/value/oracle/semaphore.res.oracle b/tests/value/oracle/semaphore.res.oracle
index fbe8d53985f..12339ab0661 100644
--- a/tests/value/oracle/semaphore.res.oracle
+++ b/tests/value/oracle/semaphore.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
Sa ∈ {0}
Sb ∈ {0}
-[kernel:annot:missing-spec] semaphore.i:6: Warning:
+[kernel:annot:missing-spec] semaphore.i:31: Warning:
Neither code nor specification for function V,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function V <- g.
@@ -23,7 +23,7 @@
Called from semaphore.i:31.
[eva] Done for function V
[eva] semaphore.i:28: starting to merge loop iterations
-[kernel:annot:missing-spec] semaphore.i:6: Warning:
+[kernel:annot:missing-spec] semaphore.i:34: Warning:
Neither code nor specification for function P,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function P <- g.
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
index 8c0e0d9b030..17a53f17bdc 100644
--- a/tests/value/oracle/strings.res.oracle
+++ b/tests/value/oracle/strings.res.oracle
@@ -40,7 +40,7 @@
Z ∈ {0}
[eva] computing for function string_reads <- main.
Called from strings.i:142.
-[kernel:annot:missing-spec] strings.i:15: Warning:
+[kernel:annot:missing-spec] strings.i:39: Warning:
Neither code nor specification for function u,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function u <- string_reads <- main.
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 0b65451110d..65b9fa9ca02 100644
--- a/tests/value/oracle/summary.3.res.oracle
+++ b/tests/value/oracle/summary.3.res.oracle
@@ -52,14 +52,14 @@
assertion got status invalid (stopping propagation).
[eva] Recording results for logic
[eva] Done for function logic
-[kernel:annot:missing-spec] summary.i:48: Warning:
+[kernel:annot:missing-spec] summary.i:64: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
Called from summary.i:64.
[eva] using specification for function f
[eva] Done for function f
-[kernel:annot:missing-spec] summary.i:49: Warning:
+[kernel:annot:missing-spec] summary.i:65: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/summary.4.res.oracle b/tests/value/oracle/summary.4.res.oracle
index c016f68b72a..78f84b5adc2 100644
--- a/tests/value/oracle/summary.4.res.oracle
+++ b/tests/value/oracle/summary.4.res.oracle
@@ -74,14 +74,14 @@
assertion got status invalid (stopping propagation).
[eva] Recording results for logic
[eva] Done for function logic
-[kernel:annot:missing-spec] summary.i:48: Warning:
+[kernel:annot:missing-spec] summary.i:64: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function f <- main.
Called from summary.i:64.
[eva] using specification for function f
[eva] Done for function f
-[kernel:annot:missing-spec] summary.i:49: Warning:
+[kernel:annot:missing-spec] summary.i:65: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/switch2.res.oracle b/tests/value/oracle/switch2.res.oracle
index 03159449108..ba43fc436ae 100644
--- a/tests/value/oracle/switch2.res.oracle
+++ b/tests/value/oracle/switch2.res.oracle
@@ -8,7 +8,7 @@
Called from switch2.i:13.
[eva] Recording results for f
[eva] Done for function f
-[kernel:annot:missing-spec] switch2.i:7: Warning:
+[kernel:annot:missing-spec] switch2.i:13: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/use_spec.0.res.oracle b/tests/value/oracle/use_spec.0.res.oracle
index 90b425ae5cb..860675533da 100644
--- a/tests/value/oracle/use_spec.0.res.oracle
+++ b/tests/value/oracle/use_spec.0.res.oracle
@@ -14,7 +14,7 @@
Called from use_spec.i:25.
[eva] using specification for function f
[eva] Done for function f
-[kernel:annot:missing-spec] use_spec.i:13: Warning:
+[kernel:annot:missing-spec] use_spec.i:26: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/use_spec.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index fb4b4c41a4f..88fa49960f6 100644
--- a/tests/value/oracle/use_spec.1.res.oracle
+++ b/tests/value/oracle/use_spec.1.res.oracle
@@ -14,7 +14,7 @@
Called from use_spec.i:25.
[eva] using specification for function f
[eva] Done for function f
-[kernel:annot:missing-spec] use_spec.i:13: Warning:
+[kernel:annot:missing-spec] use_spec.i:26: Warning:
Neither code nor specification for function g,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function g <- main.
diff --git a/tests/value/oracle/volatile.res.oracle b/tests/value/oracle/volatile.res.oracle
index 5f3ac9c064e..d8d0bd4dec7 100644
--- a/tests/value/oracle/volatile.res.oracle
+++ b/tests/value/oracle/volatile.res.oracle
@@ -55,7 +55,7 @@
signed overflow. assert x_0 + y_0 ≤ 2147483647;
[eva] Recording results for fn1
[eva] Done for function fn1
-[kernel:annot:missing-spec] volatile.c:20: Warning:
+[kernel:annot:missing-spec] volatile.c:40: Warning:
Neither code nor specification for function fn2,
generating default assigns. See -generated-spec-* options for more info
[eva] computing for function fn2 <- main1 <- main.
--
GitLab