From 0131463ebd839b9343162b2fa4ede83d36456d86 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 4 Oct 2023 11:14:02 +0200
Subject: [PATCH] [tests] Update test oracles
---
.../oracle_prove/declared_function.res.oracle | 2 +-
.../ya/oracle_prove/incorrect.res.oracle | 2 +-
.../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 +-
.../tests/nonterm/oracle/n5.res.oracle | 4 +--
.../report/tests/report/oracle/csv.res.oracle | 2 +-
.../tests/report/oracle/hyp.0.res.oracle | 2 +-
.../tests/report/oracle/hyp.1.res.oracle | 4 +--
.../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/wp/oracle/bad_cast_call.res.oracle | 2 +-
.../wp/oracle/exit_post_scope.res.oracle | 2 +-
.../wp/oracle/stmtcompiler_test.res.oracle | 2 +-
.../tests/wp/oracle/wp_call_pre.0.res.oracle | 4 +--
.../tests/wp/oracle/wp_call_pre.2.res.oracle | 4 +--
.../tests/wp/oracle/wp_call_pre.3.res.oracle | 2 +-
.../wp/oracle_qualif/bad_cast_call.res.oracle | 2 +-
.../oracle_qualif/exit_post_scope.res.oracle | 2 +-
.../stmtcompiler_test.res.oracle | 2 +-
.../wp/oracle_qualif/wp_call_pre.res.oracle | 4 +--
.../oracle/garbled_opaque_struct.res.oracle | 2 +-
.../wp_acsl/oracle/init_label.res.oracle | 2 +-
.../oracle/initialized_shift_array.res.oracle | 2 +-
.../wp_acsl/oracle/opaque_struct.res.oracle | 2 +-
.../oracle/unsupported_builtin.res.oracle | 2 +-
.../garbled_opaque_struct.res.oracle | 2 +-
.../oracle_qualif/init_label.res.oracle | 2 +-
.../initialized_shift_array.res.oracle | 2 +-
.../oracle_qualif/opaque_struct.res.oracle | 2 +-
.../wp_bts/oracle/issue_715_a.res.oracle | 2 +-
.../wp_bts/oracle/issue_715_b.res.oracle | 2 +-
.../oracle_qualif/issue_715_a.res.oracle | 2 +-
.../oracle_qualif/issue_715_b.res.oracle | 2 +-
.../wp_plugin/oracle/invertible.res.oracle | 2 +-
.../tests/wp_typed/oracle/avar.0.res.oracle | 2 +-
.../tests/wp_typed/oracle/avar.1.res.oracle | 2 +-
.../tests/wp_typed/oracle/mvar.0.res.oracle | 2 +-
.../tests/wp_typed/oracle/mvar.1.res.oracle | 2 +-
.../wp_typed/oracle/unit_call.0.res.oracle | 2 +-
.../wp_typed/oracle/unit_call.1.res.oracle | 2 +-
.../wp_typed/oracle_qualif/avar.res.oracle | 2 +-
.../wp_typed/oracle_qualif/mvar.res.oracle | 2 +-
.../oracle_qualif/unit_call.res.oracle | 2 +-
.../wp_usage/oracle/code_spec.res.oracle | 4 +--
.../wp/tests/wp_usage/oracle/reads.res.oracle | 2 +-
.../builtins/oracle/assert_builtin.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/misc/oracle/vis_spec.res.oracle | 2 +-
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/intra.2.res.oracle | 2 +-
tests/sparecode/oracle/top.0.res.oracle | 2 +-
tests/sparecode/oracle/top.1.res.oracle | 2 +-
tests/sparecode/oracle/top.2.res.oracle | 2 +-
tests/spec/oracle/assigns_from_kf.res.oracle | 28 +++++++++----------
tests/spec/oracle/assigns_void.1.res.oracle | 2 +-
.../oracle/default_assigns_bts0966.res.oracle | 2 +-
.../oracle/default_spec_combine.0.res.oracle | 24 ++++++++--------
.../oracle/default_spec_combine.1.res.oracle | 24 ++++++++--------
.../oracle/default_spec_combine.2.res.oracle | 24 ++++++++--------
.../oracle/default_spec_custom.0.res.oracle | 4 +--
.../oracle/default_spec_custom.1.res.oracle | 4 +--
.../oracle/default_spec_mode.0.res.oracle | 12 ++++----
.../oracle/default_spec_mode.1.res.oracle | 6 ++--
.../oracle/default_spec_mode.2.res.oracle | 16 +++++------
.../oracle/default_spec_mode.3.res.oracle | 16 +++++------
.../oracle/default_spec_mode.4.res.oracle | 10 +++----
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 +-
.../value/oracle/invalid_lval_arg.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/protomain.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.0.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 +-
241 files changed, 472 insertions(+), 472 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
index 9d7049d26d3..8cc9fe1473e 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/declared_function.res.oracle
@@ -1,6 +1,6 @@
[kernel] Parsing declared_function.i (no preprocessing)
[kernel] Parsing TMPDIR/aorai_declared_function_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:112: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_declared_function_0_prove.i:4: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
diff --git a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
index b5b842d5b2f..b55d3bc8821 100644
--- a/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle_prove/incorrect.res.oracle
@@ -2,6 +2,6 @@
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing TMPDIR/aorai_incorrect_0_prove.i (no preprocessing)
[wp] Warning: Missing RTE guards
-[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:77: Warning:
+[kernel:annot:missing-spec] TMPDIR/aorai_incorrect_0_prove.i:6: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
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 67745c5779d..4a5816b86a6 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] parallel_threads.c:121: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: 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 67745c5779d..4a5816b86a6 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] parallel_threads.c:121: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/pthread.h:311: 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 aa890a27d2e..a7964a71784 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] hidden_malloc.c:11: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: 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 f6c71b561f1..1583f80fac7 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] t_fun_lib.c:19: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdlib.h:754: 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/nonterm/tests/nonterm/oracle/n5.res.oracle b/src/plugins/nonterm/tests/nonterm/oracle/n5.res.oracle
index 04e470cae08..574cd52a006 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:21: Warning:
+[kernel:annot:missing-spec] n5.i:9: 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:12: Warning:
+[kernel:annot:missing-spec] n5.i:5: 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 1ad19f92ff2..210bc3fcccd 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:21: Warning:
+[kernel:annot:missing-spec] csv.c: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 <- main2 <- main.
diff --git a/src/plugins/report/tests/report/oracle/hyp.0.res.oracle b/src/plugins/report/tests/report/oracle/hyp.0.res.oracle
index 612c1e14816..fe76bf39773 100644
--- a/src/plugins/report/tests/report/oracle/hyp.0.res.oracle
+++ b/src/plugins/report/tests/report/oracle/hyp.0.res.oracle
@@ -3,7 +3,7 @@
--------------------------------------------------------------------------------
--- No status to report
--------------------------------------------------------------------------------
-[kernel:annot:missing-spec] hyp.i:25: Warning:
+[kernel:annot:missing-spec] hyp.i:7: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[kernel] SETTING STATUS OF assert \false; TO unknown
diff --git a/src/plugins/report/tests/report/oracle/hyp.1.res.oracle b/src/plugins/report/tests/report/oracle/hyp.1.res.oracle
index 546cc9cbc96..d71e190f20c 100644
--- a/src/plugins/report/tests/report/oracle/hyp.1.res.oracle
+++ b/src/plugins/report/tests/report/oracle/hyp.1.res.oracle
@@ -3,10 +3,10 @@
--------------------------------------------------------------------------------
--- No status to report
--------------------------------------------------------------------------------
-[kernel:annot:missing-spec] hyp.i:25: Warning:
+[kernel:annot:missing-spec] hyp.i:7: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] hyp.i:25: Warning:
+[kernel:annot:missing-spec] hyp.i:8: Warning:
Neither code nor specification for function f2,
generating default assigns. See -generated-spec-* options for more info
[kernel] NEVER_TRIED + NEVER_TRIED
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 8856945b2de..9a4ba240832 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:8: Warning:
+[kernel:annot:missing-spec] empty-vpar-with-ghost.i:5: 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 f59a25caa33..72bb0792e2b 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:8: Warning:
+[kernel:annot:missing-spec] empty-vpar.i:5: 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 c47d7de999a..c3a46f89849 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:2: Warning:
+[kernel:annot:missing-spec] function-ptr-with-ghost.i:4: 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 bc7ed6281c8..b77faefc9d6 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:8: Warning:
+[kernel:annot:missing-spec] label.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/multi.res.oracle b/src/plugins/variadic/tests/declared/oracle/multi.res.oracle
index b2c0657c754..3d7544a2bcc 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:18: Warning:
+[kernel:annot:missing-spec] multi.i:15: 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:9: Warning:
+[kernel:annot:missing-spec] multi.i:6: 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 73007ab0ccb..5c1cc2988c4 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:4: Warning:
+[kernel:annot:missing-spec] no-va-with-ghost.i:1: 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 58717791f35..a9c2ce7a4bf 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:4: Warning:
+[kernel:annot:missing-spec] no-va.i:1: 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 5fbb9d01fa7..a900ef19ea7 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:5: Warning:
+[kernel:annot:missing-spec] rvalues-with-ghost.i:1: 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 3ffbfe423b8..0c9e683b20c 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:5: Warning:
+[kernel:annot:missing-spec] rvalues.i:1: 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 6e687acfe0e..8025cbd92d5 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:9: Warning:
+[kernel:annot:missing-spec] simple-with-ghost.i:6: 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 8725172d792..54ea4910750 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:9: Warning:
+[kernel:annot:missing-spec] simple.i:6: 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 ab60728bd8e..bd5b5017ddb 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:10: Warning:
+[kernel:annot:missing-spec] struct.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-with-ghost.res.oracle b/src/plugins/variadic/tests/declared/oracle/typedefed_function-with-ghost.res.oracle
index a9bee4f8d44..b0f695ca4af 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:5: Warning:
+[kernel:annot:missing-spec] typedefed_function-with-ghost.i:2: 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 2fa079d75a8..5d7bccf0c58 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:5: Warning:
+[kernel:annot:missing-spec] typedefed_function.i:2: 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 74ea04f2c8f..db382b8430b 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] exec.c:15: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/unistd.h:821: 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 da138c294e8..c5b43790ae0 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] fcntl.c:16: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:129: 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] fcntl.c:28: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:129: 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 fd420fb5cef..7814251c927 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] open.c:9: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:136: 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 6550a1739aa..c45e5c55e42 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] open_wrong.c:13: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:136: 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 b7ac263ec20..f332052289b 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] openat.c:10: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/fcntl.h:143: 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 96c9680ea4b..a6bd5f6a94d 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] printf.c:71: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: 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 4bc1b2c08cd..d89586c5159 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] printf_wrong_arity.c:9: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: 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 24ae14ef3ed..83a51e8e270 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] printf_wrong_types.c:18: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/stdio.h:211: 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/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
index c9e134a8954..16e5f57c14e 100644
--- a/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/bad_cast_call.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing bad_cast_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] bad_cast_call.i:6: Warning:
+[kernel:annot:missing-spec] bad_cast_call.i:4: Warning:
Neither code nor explicit assigns for function m,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle b/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
index 1808e3fca99..c2759c1dc2d 100644
--- a/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/exit_post_scope.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing exit_post_scope.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] exit_post_scope.i:7: Warning:
+[kernel:annot:missing-spec] exit_post_scope.i:1: Warning:
Neither code nor specification for function bar,
generating default assigns. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
index e78d5fcf6c3..6e56a2ecd32 100644
--- a/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/stmtcompiler_test.res.oracle
@@ -3,7 +3,7 @@
[kernel:CERT:MSC:37] stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
-[kernel:annot:missing-spec] stmtcompiler_test.i:167: Warning:
+[kernel:annot:missing-spec] stmtcompiler_test.i:104: Warning:
Neither code nor explicit assigns for function behavior1,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
index 284392617d0..8686a159f65 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.0.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:22: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:18: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
index 220dc834c2c..b75471e832b 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.2.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:22: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:18: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
index a868d9e01d2..c4b916a5058 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_call_pre.3.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-model 'Hoare' [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:18: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
index e08205f29c5..5c05ca58156 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/bad_cast_call.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing bad_cast_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] bad_cast_call.i:6: Warning:
+[kernel:annot:missing-spec] bad_cast_call.i:4: Warning:
Neither code nor explicit assigns for function m,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
index b6025b1fb43..41b947831b3 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/exit_post_scope.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing exit_post_scope.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] exit_post_scope.i:7: Warning:
+[kernel:annot:missing-spec] exit_post_scope.i:1: Warning:
Neither code nor specification for function bar,
generating default assigns. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
index f152e832248..7f261f2b181 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle
@@ -3,7 +3,7 @@
[kernel:CERT:MSC:37] stmtcompiler_test.i:136: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
-[kernel:annot:missing-spec] stmtcompiler_test.i:167: Warning:
+[kernel:annot:missing-spec] stmtcompiler_test.i:104: Warning:
Neither code nor explicit assigns for function behavior1,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
index 028dbf91926..aa6880fb7a8 100644
--- a/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle_qualif/wp_call_pre.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp [...]
[kernel] Parsing wp_call_pre.c (with preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:18: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] wp_call_pre.c:47: Warning:
+[kernel:annot:missing-spec] wp_call_pre.c:22: Warning:
Neither code nor explicit assigns for function g,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/garbled_opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/garbled_opaque_struct.res.oracle
index 5ca07d19383..51d45ab1772 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/garbled_opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/garbled_opaque_struct.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing garbled_opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] garbled_opaque_struct.i:2: Warning:
+[kernel:annot:missing-spec] garbled_opaque_struct.i:1: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
index 6ef2f2ba528..08f6f3da3ec 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/init_label.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing init_label.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] init_label.i:27: Warning:
+[kernel:annot:missing-spec] init_label.i:14: Warning:
Neither code nor explicit assigns for function main,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
index b28bec3b1e2..5f674e1efb1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/initialized_shift_array.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing initialized_shift_array.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] initialized_shift_array.i:52: Warning:
+[kernel:annot:missing-spec] initialized_shift_array.i:4: Warning:
Neither code nor explicit assigns for function test,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
index 5d8a5fcbfe2..64468eccfdc 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/opaque_struct.res.oracle
@@ -7,7 +7,7 @@
[rte:annot] annotating function chunk_typing
[rte:annot] annotating function initialized_assigns
[rte:annot] annotating function uninitialized_assigns
-[kernel:annot:missing-spec] opaque_struct.i:79: Warning:
+[kernel:annot:missing-spec] opaque_struct.i:76: Warning:
Neither code nor specification for function use,
generating default assigns. See -generated-spec-* options for more info
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
index 58f50450f29..1a2ff51103f 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unsupported_builtin.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing unsupported_builtin.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] unsupported_builtin.i:11: Warning:
+[kernel:annot:missing-spec] unsupported_builtin.i:9: Warning:
Neither code nor explicit assigns for function foo,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/garbled_opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/garbled_opaque_struct.res.oracle
index 100e72638ff..8aba1396eac 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/garbled_opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/garbled_opaque_struct.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing garbled_opaque_struct.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] garbled_opaque_struct.i:2: Warning:
+[kernel:annot:missing-spec] garbled_opaque_struct.i:1: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
index f011ba6e619..ae45c27a849 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/init_label.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing init_label.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] init_label.i:27: Warning:
+[kernel:annot:missing-spec] init_label.i:14: Warning:
Neither code nor explicit assigns for function main,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
index 08ba9fda9b4..cedccb6ee99 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/initialized_shift_array.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing initialized_shift_array.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] initialized_shift_array.i:52: Warning:
+[kernel:annot:missing-spec] initialized_shift_array.i:4: Warning:
Neither code nor explicit assigns for function test,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
index 5600c67c9f1..206fb19d1e1 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/opaque_struct.res.oracle
@@ -7,7 +7,7 @@
[rte:annot] annotating function chunk_typing
[rte:annot] annotating function initialized_assigns
[rte:annot] annotating function uninitialized_assigns
-[kernel:annot:missing-spec] opaque_struct.i:79: Warning:
+[kernel:annot:missing-spec] opaque_struct.i:76: Warning:
Neither code nor specification for function use,
generating default assigns. See -generated-spec-* options for more info
[wp] 15 goals scheduled
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
index 53454a8d95a..e1e2237a8bd 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_a.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_a.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] issue_715_a.i:6: Warning:
+[kernel:annot:missing-spec] issue_715_a.i:4: Warning:
Neither code nor explicit assigns for function dummy,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
index ad445cb36a8..487fdfde99f 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_715_b.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_b.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] issue_715_b.i:9: Warning:
+[kernel:annot:missing-spec] issue_715_b.i:7: Warning:
Neither code nor explicit assigns for function dummy,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
index 077a078f07a..fb52594bcc8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_a.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_a.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] issue_715_a.i:6: Warning:
+[kernel:annot:missing-spec] issue_715_a.i:4: Warning:
Neither code nor explicit assigns for function dummy,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
index c67d9c62515..3393e5f23a8 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_715_b.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing issue_715_b.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] issue_715_b.i:9: Warning:
+[kernel:annot:missing-spec] issue_715_b.i:7: Warning:
Neither code nor explicit assigns for function dummy,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
index ece1dcad13e..d496878a57a 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/invertible.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing invertible.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] invertible.i:17: Warning:
+[kernel:annot:missing-spec] invertible.i:32: Warning:
Neither code nor explicit assigns for function main,
generating default clauses. See -generated-spec-* options for more info
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
index e2a91126f38..972163f389d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/avar.0.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] avar.i:4: Warning:
+[kernel:annot:missing-spec] avar.i:2: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
index 0cf211b553e..2790756ca04 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/avar.1.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] avar.i:4: Warning:
+[kernel:annot:missing-spec] avar.i:2: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
index d53a7574678..e87e5788748 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.0.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] mvar.i:14: Warning:
+[kernel:annot:missing-spec] mvar.i:8: Warning:
Neither code nor explicit assigns for function Write,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
index 78f5911e4a7..7fac07c71df 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/mvar.1.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] mvar.i:14: Warning:
+[kernel:annot:missing-spec] mvar.i:8: Warning:
Neither code nor explicit assigns for function Write,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
index d60e59736da..66f5e7acb19 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.0.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] unit_call.i:7: Warning:
+[kernel:annot:missing-spec] unit_call.i:5: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
index f48689966c0..23779fce064 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/unit_call.1.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp -wp-model 'Typed (Ref)' [...]
[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] unit_call.i:7: Warning:
+[kernel:annot:missing-spec] unit_call.i:5: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
index 8973bd52e7a..603ca3e2844 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/avar.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing avar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] avar.i:4: Warning:
+[kernel:annot:missing-spec] avar.i:2: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
index 373717bf271..0984fa19a4d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/mvar.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing mvar.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] mvar.i:14: Warning:
+[kernel:annot:missing-spec] mvar.i:8: Warning:
Neither code nor explicit assigns for function Write,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
index 2bee8bfd762..7498622c245 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/unit_call.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing unit_call.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] unit_call.i:7: Warning:
+[kernel:annot:missing-spec] unit_call.i:5: Warning:
Neither code nor explicit assigns for function f,
generating default clauses. See -generated-spec-* options for more info
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
index b0e4f5db096..412c259fd50 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/code_spec.res.oracle
@@ -1,10 +1,10 @@
# frama-c -wp [...]
[kernel] Parsing code_spec.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] code_spec.i:126: Warning:
+[kernel:annot:missing-spec] code_spec.i:73: Warning:
Neither code nor explicit assigns for function by_addr_in_spec,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] code_spec.i:126: Warning:
+[kernel:annot:missing-spec] code_spec.i:76: Warning:
Neither code nor explicit assigns for function by_array_in_spec,
generating default clauses. See -generated-spec-* options for more info
.................................................
diff --git a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
index df508e5d6c4..e657b964114 100644
--- a/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
+++ b/src/plugins/wp/tests/wp_usage/oracle/reads.res.oracle
@@ -1,7 +1,7 @@
# frama-c -wp [...]
[kernel] Parsing reads.i (no preprocessing)
[wp] Running WP plugin...
-[kernel:annot:missing-spec] reads.i:86: Warning:
+[kernel:annot:missing-spec] reads.i:87: Warning:
Neither code nor explicit assigns for function recursive_usage,
generating default clauses. See -generated-spec-* options for more info
.................................................
diff --git a/tests/builtins/oracle/assert_builtin.res.oracle b/tests/builtins/oracle/assert_builtin.res.oracle
index d4ee8d50d03..27ada191a32 100644
--- a/tests/builtins/oracle/assert_builtin.res.oracle
+++ b/tests/builtins/oracle/assert_builtin.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing assert_builtin.i (no preprocessing)
-[kernel:annot:missing-spec] assert_builtin.i:5: Warning:
+[kernel:annot:missing-spec] assert_builtin.i:3: Warning:
Neither code nor specification for function Frama_C_assert,
generating default assigns. See -generated-spec-* options for more info
[eva] Analyzing a complete application starting at main
diff --git a/tests/builtins/oracle/imprecise.res.oracle b/tests/builtins/oracle/imprecise.res.oracle
index bc169708e5b..5ad0f3b323b 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:75: Warning:
+[kernel:annot:missing-spec] imprecise.c:72: 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 a45058cb898..15dda274f30 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:8: Warning:
+[kernel:annot:missing-spec] fct_ptr.i: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 <- main.
diff --git a/tests/fc_script/make-wrapper.t/run.t b/tests/fc_script/make-wrapper.t/run.t
index b64143a7e57..6e978274306 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:29: Warning:
+ [kernel:annot:missing-spec] make-wrapper.c:14: 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 6d32745d1b0..30155d0cc17 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:21: Warning:
+[kernel:annot:missing-spec] alarms.i:11: 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 7eb8cbc512c..69eb74ce4a3 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:21: Warning:
+[kernel:annot:missing-spec] alarms.i:11: 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 111eb599476..c8d7e2c4d4b 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:21: Warning:
+[kernel:annot:missing-spec] alarms.i:11: 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 4e3111b5d00..89383cc7912 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:94: Warning:
+[kernel:annot:missing-spec] contract_special_float.c:48: 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 5204d3ea928..1a83bef8646 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:94: Warning:
+[kernel:annot:missing-spec] contract_special_float.c:48: 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 02edc7f29a8..97c595ce712 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:230: Warning:
+[kernel:annot:missing-spec] s.i:9: 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:233: Warning:
+[kernel:annot:missing-spec] s.i:10: 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:244: Warning:
+[kernel:annot:missing-spec] s.i:12: 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 7c1a8df24df..a246c6de55a 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:16: Warning:
+[kernel:annot:missing-spec] call.i:12: 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 22222bc2aac..ed164092a6a 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:16: Warning:
+[kernel:annot:missing-spec] call.i:12: 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 2d7016cb262..ce3a3c2a489 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:45: Warning:
+[kernel:annot:missing-spec] call.i:12: 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 94f614cca0a..9661edfc6e0 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:10: Warning:
+[kernel:annot:missing-spec] undef_function.i:5: 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 bd08bb92439..6b28d3e6c56 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:12: Warning:
+[kernel:annot:missing-spec] variadic.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/libc/oracle/search_h.res.oracle b/tests/libc/oracle/search_h.res.oracle
index b4d4733d917..1e501dfc8b4 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] search_h.c:34: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/search.h:61: 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] search_h.c:46: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/search.h:64: 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 01e765f74b0..3809bf3497a 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] spawn_h.c:43: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:72: 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] spawn_h.c:47: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:55: 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] spawn_h.c:60: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:97: 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] spawn_h.c:63: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:99: 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] spawn_h.c:68: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:113: 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] spawn_h.c:82: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:116: 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] spawn_h.c:90: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:75: 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] spawn_h.c:96: Warning:
+[kernel:annot:missing-spec] FRAMAC_SHARE/libc/spawn.h:69: 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/misc/oracle/vis_spec.res.oracle b/tests/misc/oracle/vis_spec.res.oracle
index efe7d6c6398..ca9ab8cc5bc 100644
--- a/tests/misc/oracle/vis_spec.res.oracle
+++ b/tests/misc/oracle/vis_spec.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing vis_spec.i (no preprocessing)
-[kernel:annot:missing-spec] vis_spec.i:10: Warning:
+[kernel:annot:missing-spec] vis_spec.i:7: Warning:
Neither code nor explicit exits for function g,
generating default clauses. See -generated-spec-* options for more info
Starting visit
diff --git a/tests/pdg/oracle/bts1194.res.oracle b/tests/pdg/oracle/bts1194.res.oracle
index 110353a5cca..1c624742fba 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:13: Warning:
+[kernel:annot:missing-spec] bts1194.c:9: 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 64da29a0597..3c7b0748670 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:24: Warning:
+[kernel:annot:missing-spec] no_body.c:13: 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 18b970df444..a65568abcc4 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:48: Warning:
+[kernel:annot:missing-spec] pb_infinite_loop.c:43: 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 acf750f7fc7..5f0af4fe428 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:23: Warning:
+[kernel:annot:missing-spec] variadic.c:20: 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 975b6c1a98e..ba7c315cccf 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:36: Warning:
+[kernel:annot:missing-spec] bts383.c:32: 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 9fd462bcb24..0b6a82d32ee 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:18: Warning:
+[kernel:annot:missing-spec] bts1768.i:15: 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 cad1b060401..0a690a35fb3 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:55: Warning:
+[kernel:annot:missing-spec] bts709.c:54: 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 2cbd14ab48a..e77debabe4d 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:17: Warning:
+[kernel:annot:missing-spec] combine.i:8: 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 073800f4115..f6036ecc4fa 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:36: Warning:
+[kernel:annot:missing-spec] filter.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 <- unspec <- main.
diff --git a/tests/slicing/oracle/loops.15.res.oracle b/tests/slicing/oracle/loops.15.res.oracle
index 726662f7e0d..dd18cad9e65 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:70: Warning:
+[kernel:annot:missing-spec] loops.i:61: 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 5d4fe926d54..0cda5b17cde 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:70: Warning:
+[kernel:annot:missing-spec] loops.i:61: 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 04a864ff382..4f0b797442e 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:89: Warning:
+[kernel:annot:missing-spec] loops.i:61: 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 45e2e5b6191..5ea6c7a008e 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:89: Warning:
+[kernel:annot:missing-spec] loops.i:61: 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 87f3dae909c..78aabc7629f 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 6c3bee4acf3..047a99c8e94 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:17: Warning:
+[kernel:annot:missing-spec] ptr_fct.i:11: 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 e5de9941760..cde9b9ebdde 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 9b4b2a0f20b..63bfc9b7a27 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 178bb3278c0..47a035a0d9f 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 a394bebd6a6..e3871fd3d87 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 f466ab7ac09..fdcad002e61 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 a85c8c1ecd4..a6bee706619 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 1f98d6f3ef1..cd9c16cbac3 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 7918bf2ca4e..a0845a156c5 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 988211d29e3..b8d5147e844 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 769500d84d8..3b7aab4fe85 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 feed01b3a62..d8ef7a2822c 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 75357eb578c..db410543427 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 1c1c5920893..77d7282f748 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 2cf898dc544..0ebb63a1996 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 9bab22454a4..e80af681484 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:140: Warning:
+[kernel:annot:missing-spec] select_by_annot.i:126: 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 04a122b6451..3959136da4c 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:22: Warning:
+[kernel:annot:missing-spec] select_calls.i:8: 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:24: Warning:
+[kernel:annot:missing-spec] select_calls.i:10: 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:30: Warning:
+[kernel:annot:missing-spec] select_calls.i:12: 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 fd1fa6b4d75..c3a0e8506c5 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:42: Warning:
+[kernel:annot:missing-spec] select_calls.i:6: 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 e7783ec0de8..b934f52d140 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 333c77abdec..97efb95010b 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 35cd5e8e21e..3d590ac884d 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 25abd7c442a..6d50c819a40 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 71a60f4e33e..966959e2d01 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 374b5e57876..c3a9979aff7 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 490fec97454..f7fe215fa0c 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 133365cf41b..03b193f4a42 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 22f1c275ac6..9db6296f5e2 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 c2e59c2a942..e8cb8185f8f 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 76d57c2c353..da8a8c63d9b 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 c4c03e484a9..14dbc9a6b57 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 30dee131fa8..f5f8270f853 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 21d015132d3..1d1b7c31dd1 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 1aedb324dc3..e80ecd16453 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 512580d2488..c992fa8daa7 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 0bdd4613f78..dea84380dbf 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 b9b128bad9c..5d06e588806 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 2a25d0ccc94..045c7b13ff6 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 4f6a431dcc0..80595d9f5e0 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 24560b33d23..a77fac918a0 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 1aff238e6d1..beffeb890cd 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:35: Warning:
+[kernel:annot:missing-spec] select_return.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.
Called from select_return.i:35.
[eva] using specification for function get
[eva] Done for function get
-[kernel:annot:missing-spec] select_return.i:39: Warning:
+[kernel:annot:missing-spec] select_return.i:32: 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:53: Warning:
+[kernel:annot:missing-spec] select_return.i:30: 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 1986a1f5e3a..eb0059d622e 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 0b66bb17ec3..a810b5fdfcf 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 0a9c10c832f..64ca689f84f 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 77cabccd7a9..7850686158e 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 66d2c8939ba..6d026acbd80 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 5b6b79c6c32..ce7ae154cf4 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 fb4196860a8..42af2bc0520 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 f2a805d61eb..a709300a7c3 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 8543cd69f05..02c2717dbd5 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 bfe24c784f6..3e445d2ee61 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 e0d303d726d..8b0e71e1bea 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:28: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:16: 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:24: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:19: 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:44: Warning:
+[kernel:annot:missing-spec] select_return_bis.i:18: 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 7363f61184e..41ec5343c90 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:21: Warning:
+[kernel:annot:missing-spec] slice_no_body.i:9: 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 9e74fb164a5..ae79b26d9eb 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:19: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:16: 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 f16981aa519..8dc524e7573 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:19: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:16: 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 a8135ee7087..fd303d69636 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:19: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:16: 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 9a83feb26ec..a439aa19915 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:19: Warning:
+[kernel:annot:missing-spec] unravel-flavors.i:16: 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 37844d3957e..8a3f0ff6239 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:36: Warning:
+[kernel:annot:missing-spec] unravel-point.i:26: 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 97703a34e75..a8e1db664dd 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:36: Warning:
+[kernel:annot:missing-spec] unravel-point.i:26: 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 985169fe22a..5a7ab392ed5 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:36: Warning:
+[kernel:annot:missing-spec] unravel-point.i:26: 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 1a4a5c83d40..bf41616d75e 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:36: Warning:
+[kernel:annot:missing-spec] unravel-point.i:26: 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 e0f32464a55..675b48c03ef 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:36: Warning:
+[kernel:annot:missing-spec] unravel-point.i:26: 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:59: Warning:
+[kernel:annot:missing-spec] unravel-point.i:22: 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 e9aae04102c..513c0912072 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:31: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:10: 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:52: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:11: 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:53: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:12: 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:54: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:13: 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:55: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:14: 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:56: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:15: 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 2deb200cd14..3c0aeed5612 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:31: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:10: 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:52: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:11: 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:53: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:12: 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:54: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:13: 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:55: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:14: 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:56: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:15: 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 f6734df8ff5..5f609480148 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:31: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:10: 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:52: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:11: 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:53: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:12: 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:54: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:13: 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:55: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:14: 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:56: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:15: 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 dfb4b2c3bd6..15cdd9f5420 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:31: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:10: 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:52: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:11: 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:53: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:12: 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:54: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:13: 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:55: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:14: 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:56: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:15: 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 60f4918fed8..556f2cf86e0 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:31: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:10: 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:52: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:11: 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:53: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:12: 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:54: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:13: 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:55: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:14: 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:56: Warning:
+[kernel:annot:missing-spec] unravel-variance.i:15: 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 8c405ab8eb8..9606c29d72d 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:23: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:20: 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 532c28c2066..14aaddde6b5 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:23: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:20: 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 8650b514d9c..b0835a0cf75 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:23: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:20: 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 c8160927ebc..aa3e4f78d17 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:23: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:20: 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 c8160927ebc..aa3e4f78d17 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:23: Warning:
+[kernel:annot:missing-spec] tests/pdg/variadic.c:20: 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 046c3ca1741..c23af3da53b 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:66: Warning:
+[kernel:annot:missing-spec] bts334.i:61: 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 2f9cd063399..28c6ec682d7 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:66: Warning:
+[kernel:annot:missing-spec] bts334.i:61: 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 d88f06cdf73..96192455136 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:66: Warning:
+[kernel:annot:missing-spec] bts334.i:61: 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 88889b31a6e..f8b3fcdd631 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:91: Warning:
+[kernel:annot:missing-spec] intra.i:73: 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 340b1dc3072..4dc9557ce91 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:91: Warning:
+[kernel:annot:missing-spec] intra.i:73: 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.2.res.oracle b/tests/sparecode/oracle/intra.2.res.oracle
index 18fac29622d..93f6885a56a 100644
--- a/tests/sparecode/oracle/intra.2.res.oracle
+++ b/tests/sparecode/oracle/intra.2.res.oracle
@@ -40,7 +40,7 @@
[pdg] Bottom for function spare_called_fct
[pdg] computing for function stop
[from] Computing for function stop
-[kernel:annot:missing-spec] intra.i:93: Warning:
+[kernel:annot:missing-spec] intra.i:73: Warning:
Neither code nor specification for function stop,
generating default assigns. See -generated-spec-* options for more info
[from] Done for function stop
diff --git a/tests/sparecode/oracle/top.0.res.oracle b/tests/sparecode/oracle/top.0.res.oracle
index 17ee15d0759..5c19b7f3ac3 100644
--- a/tests/sparecode/oracle/top.0.res.oracle
+++ b/tests/sparecode/oracle/top.0.res.oracle
@@ -45,7 +45,7 @@
[sparecode] look for annotations in function print
[pdg] computing for function print
[from] Computing for function print
-[kernel:annot:missing-spec] top.i:16: Warning:
+[kernel:annot:missing-spec] top.i:7: Warning:
Neither code nor specification for function print,
generating default assigns. See -generated-spec-* options for more info
[from] Done for function print
diff --git a/tests/sparecode/oracle/top.1.res.oracle b/tests/sparecode/oracle/top.1.res.oracle
index 63bea7f723a..f2b7c795783 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:10: Warning:
+[kernel:annot:missing-spec] top.i:7: 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/sparecode/oracle/top.2.res.oracle b/tests/sparecode/oracle/top.2.res.oracle
index aa92fa03ae2..b567c18cda8 100644
--- a/tests/sparecode/oracle/top.2.res.oracle
+++ b/tests/sparecode/oracle/top.2.res.oracle
@@ -46,7 +46,7 @@
[sparecode] look for annotations in function print
[pdg] computing for function print
[from] Computing for function print
-[kernel:annot:missing-spec] top.i:22: Warning:
+[kernel:annot:missing-spec] top.i:7: Warning:
Neither code nor specification for function print,
generating default assigns. See -generated-spec-* options for more info
[from] Done for function print
diff --git a/tests/spec/oracle/assigns_from_kf.res.oracle b/tests/spec/oracle/assigns_from_kf.res.oracle
index a3d53ee6986..dfd2d66bfc8 100644
--- a/tests/spec/oracle/assigns_from_kf.res.oracle
+++ b/tests/spec/oracle/assigns_from_kf.res.oracle
@@ -1,44 +1,44 @@
[kernel] Parsing assigns_from_kf.i (no preprocessing)
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:17: Warning:
Neither code nor specification for function both,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:18: Warning:
Neither code nor specification for function both_r,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:25: Warning:
Neither code nor specification for function g_both,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:26: Warning:
Neither code nor specification for function g_both_r,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:21: Warning:
Neither code nor specification for function g_nothing,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:22: Warning:
Neither code nor specification for function g_nothing_r,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:23: Warning:
Neither code nor specification for function g_something_non_ghost,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:24: Warning:
Neither code nor specification for function g_something_non_ghost_r,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:8: Warning:
Neither code nor specification for function nothing,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:9: Warning:
Neither code nor specification for function nothing_r,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:12: Warning:
Neither code nor specification for function something_ghost,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:15: Warning:
Neither code nor specification for function something_ghost_r,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:11: Warning:
Neither code nor specification for function something_non_ghost,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] assigns_from_kf.i:29: Warning:
+[kernel:annot:missing-spec] assigns_from_kf.i:14: Warning:
Neither code nor specification for function something_non_ghost_r,
generating default assigns. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/assigns_void.1.res.oracle b/tests/spec/oracle/assigns_void.1.res.oracle
index b978ce8605c..c3356f555ee 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:11: Warning:
+[kernel:annot:missing-spec] assigns_void.c:7: 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 728ce51af93..5e34aa21316 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:34: Warning:
+[kernel:annot:missing-spec] default_assigns_bts0966.i:27: 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/spec/oracle/default_spec_combine.0.res.oracle b/tests/spec/oracle/default_spec_combine.0.res.oracle
index 720ca104b63..e54b238e14f 100644
--- a/tests/spec/oracle/default_spec_combine.0.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.0.res.oracle
@@ -1,39 +1,39 @@
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:45: Warning:
Neither code nor explicit exits for function f1_complete,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:59: Warning:
Neither code nor explicit exits for function f1_guarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:27: Warning:
Neither code nor explicit exits for function f1_unguarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:90: Warning:
Neither code nor explicit assigns for function f2_complete,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:106: Warning:
Neither code nor explicit assigns for function f2_guarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:73: Warning:
Neither code nor explicit assigns for function f2_unguarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:138: Warning:
Neither code nor explicit requires for function f3_complete,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:154: Warning:
Neither code nor explicit requires for function f3_guarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:121: Warning:
Neither code nor explicit requires for function f3_unguarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:191: Warning:
Neither code nor explicit allocates for function f4_complete,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:210: Warning:
Neither code nor explicit allocates for function f4_guarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:171: Warning:
Neither code nor explicit allocates for function f4_unguarded,
generating default clauses from the specification. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_combine.1.res.oracle b/tests/spec/oracle/default_spec_combine.1.res.oracle
index 0841097ed27..8502e339611 100644
--- a/tests/spec/oracle/default_spec_combine.1.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.1.res.oracle
@@ -1,39 +1,39 @@
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:45: Warning:
Neither code nor explicit exits and requires for function f1_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:59: Warning:
Neither code nor explicit exits and requires for function f1_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:27: Warning:
Neither code nor explicit exits and requires for function f1_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:90: Warning:
Neither code nor explicit assigns and requires for function f2_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:106: Warning:
Neither code nor explicit assigns and requires for function f2_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:73: Warning:
Neither code nor explicit assigns and requires for function f2_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:138: Warning:
Neither code nor explicit requires for function f3_complete,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:154: Warning:
Neither code nor explicit requires for function f3_guarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:121: Warning:
Neither code nor explicit requires for function f3_unguarded,
generating default clauses from the specification. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:191: Warning:
Neither code nor explicit requires and allocates for function f4_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:210: Warning:
Neither code nor explicit requires and allocates for function f4_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:171: Warning:
Neither code nor explicit requires and allocates for function f4_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_combine.2.res.oracle b/tests/spec/oracle/default_spec_combine.2.res.oracle
index 8b3889333f7..f3c764eeca9 100644
--- a/tests/spec/oracle/default_spec_combine.2.res.oracle
+++ b/tests/spec/oracle/default_spec_combine.2.res.oracle
@@ -1,39 +1,39 @@
Registering an mode that does nothing
[kernel] Parsing default_spec_combine.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:45: Warning:
Neither code nor explicit exits, assigns and allocates for function f1_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:59: Warning:
Neither code nor explicit exits, assigns and allocates for function f1_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:27: Warning:
Neither code nor explicit exits, assigns and allocates for function f1_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:90: Warning:
Neither code nor explicit exits, assigns and allocates for function f2_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:106: Warning:
Neither code nor explicit exits, assigns and allocates for function f2_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:73: Warning:
Neither code nor explicit exits, assigns and allocates for function f2_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:138: Warning:
Neither code nor explicit exits, assigns, requires and allocates for function f3_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:154: Warning:
Neither code nor explicit exits, assigns, requires and allocates for function f3_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:121: Warning:
Neither code nor explicit exits, assigns, requires and allocates for function f3_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:191: Warning:
Neither code nor explicit exits, assigns and allocates for function f4_complete,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:210: Warning:
Neither code nor explicit exits, assigns and allocates for function f4_guarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_combine.i:194: Warning:
+[kernel:annot:missing-spec] default_spec_combine.i:171: Warning:
Neither code nor explicit exits, assigns and allocates for function f4_unguarded,
generating default clauses (some from the specification). See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_custom.0.res.oracle b/tests/spec/oracle/default_spec_custom.0.res.oracle
index 286ed55307b..b731f757a61 100644
--- a/tests/spec/oracle/default_spec_custom.0.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.0.res.oracle
@@ -6,14 +6,14 @@ Registering a new spec generation mode
[kernel] Warning: Custom generation from mode emptymode not defined for requires, using frama-c mode instead
[kernel] Warning: Custom generation from mode emptymode not defined for allocates, using frama-c mode instead
[kernel] Warning: Custom generation from mode emptymode not defined for terminates, using frama-c mode instead
-[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+[kernel:annot:missing-spec] default_spec_custom.i:9: Warning:
Neither code nor specification for function f1,
generating default exits, assigns, allocates and terminates. See -generated-spec-* options for more info
[kernel] Warning: Custom status from mode emptymode not defined for exits
[kernel] Warning: Custom status from mode emptymode not defined for assigns
[kernel] Warning: Custom status from mode emptymode not defined for allocates
[kernel] Warning: Custom status from mode emptymode not defined for terminates
-[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+[kernel:annot:missing-spec] default_spec_custom.i:16: Warning:
Neither code nor specification for function f3,
generating default exits, assigns, allocates and terminates. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_custom.1.res.oracle b/tests/spec/oracle/default_spec_custom.1.res.oracle
index b88fb59fe31..68a09a7507f 100644
--- a/tests/spec/oracle/default_spec_custom.1.res.oracle
+++ b/tests/spec/oracle/default_spec_custom.1.res.oracle
@@ -1,10 +1,10 @@
Registering an empty spec generation mode
Registering a new spec generation mode
[kernel] Parsing default_spec_custom.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+[kernel:annot:missing-spec] default_spec_custom.i:9: Warning:
Neither code nor specification for function f1,
generating default exits, assigns, requires, allocates and terminates. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_custom.i:18: Warning:
+[kernel:annot:missing-spec] default_spec_custom.i:16: Warning:
Neither code nor specification for function f3,
generating default exits, assigns, requires, allocates and terminates. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_mode.0.res.oracle b/tests/spec/oracle/default_spec_mode.0.res.oracle
index 26d552ea577..78fff7dc521 100644
--- a/tests/spec/oracle/default_spec_mode.0.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.0.res.oracle
@@ -1,20 +1,20 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor specification for function f1,
generating default exits. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit allocates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit terminates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit exits for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit allocates for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit terminates for function f3,
generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_mode.1.res.oracle b/tests/spec/oracle/default_spec_mode.1.res.oracle
index a330ade6cc9..85761c8d8bb 100644
--- a/tests/spec/oracle/default_spec_mode.1.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.1.res.oracle
@@ -1,11 +1,11 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor specification for function f1,
generating default requires. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit terminates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit terminates for function f3,
generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_mode.2.res.oracle b/tests/spec/oracle/default_spec_mode.2.res.oracle
index 00c309f1271..1e6e902f935 100644
--- a/tests/spec/oracle/default_spec_mode.2.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.2.res.oracle
@@ -1,26 +1,26 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor specification for function f1,
generating default exits. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit assigns for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit allocates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit terminates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit exits for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit assigns for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit allocates for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit terminates for function f3,
generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_mode.3.res.oracle b/tests/spec/oracle/default_spec_mode.3.res.oracle
index dfede74e220..9dbaf0735f6 100644
--- a/tests/spec/oracle/default_spec_mode.3.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.3.res.oracle
@@ -1,28 +1,28 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
[kernel] Warning: Mode skip is only available via -generated-spec-custom.
The mode frama-c will be used instead
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor specification for function f1,
generating default exits. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit assigns for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit allocates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit terminates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit exits for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit assigns for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit allocates for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit terminates for function f3,
generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/spec/oracle/default_spec_mode.4.res.oracle b/tests/spec/oracle/default_spec_mode.4.res.oracle
index ac0f46d5162..ec63e420cac 100644
--- a/tests/spec/oracle/default_spec_mode.4.res.oracle
+++ b/tests/spec/oracle/default_spec_mode.4.res.oracle
@@ -1,17 +1,17 @@
[kernel] Parsing default_spec_mode.i (no preprocessing)
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor specification for function f1,
generating default assigns. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit requires for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:14: Warning:
Neither code nor explicit terminates for function f1,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit assigns for function f3,
generating default clauses. See -generated-spec-* options for more info
-[kernel:annot:missing-spec] default_spec_mode.i:30: Warning:
+[kernel:annot:missing-spec] default_spec_mode.i:24: Warning:
Neither code nor explicit terminates for function f3,
generating default clauses. See -generated-spec-* options for more info
/* Generated by Frama-C */
diff --git a/tests/value/oracle/assigns.res.oracle b/tests/value/oracle/assigns.res.oracle
index 744d7aab558..aeb161d74fb 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:79: Warning:
+[kernel:annot:missing-spec] assigns.i:71: 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:80: Warning:
+[kernel:annot:missing-spec] assigns.i:73: 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:82: Warning:
+[kernel:annot:missing-spec] assigns.i:62: 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:112: Warning:
+[kernel:annot:missing-spec] assigns.i:92: 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 002087f31ba..d149f5e7fee 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:152: Warning:
+[kernel:annot:missing-spec] assigns_from.i:150: 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 d7a242da662..d2d671709e2 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:14: Warning:
+[kernel:annot:missing-spec] automalloc.i:6: 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:15: Warning:
+[kernel:annot:missing-spec] automalloc.i:7: 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 980bd317335..1124da3762a 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:506: Warning:
+[kernel:annot:missing-spec] behaviors1.i:502: 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:521: Warning:
+[kernel:annot:missing-spec] behaviors1.i:517: 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:534: Warning:
+[kernel:annot:missing-spec] behaviors1.i:531: 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:548: Warning:
+[kernel:annot:missing-spec] behaviors1.i:545: 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:561: Warning:
+[kernel:annot:missing-spec] behaviors1.i:558: 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 45acf789580..4562b5e6847 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:70: Warning:
+[kernel:annot:missing-spec] bitfield.i:61: 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 c372fd704f0..f627390df62 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:15: Warning:
+[kernel:annot:missing-spec] bts0506.i:6: 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:20: Warning:
+[kernel:annot:missing-spec] bts0506.i:7: 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:24: Warning:
+[kernel:annot:missing-spec] bts0506.i:8: 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:27: Warning:
+[kernel:annot:missing-spec] bts0506.i:9: 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:30: Warning:
+[kernel:annot:missing-spec] bts0506.i:10: 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:33: Warning:
+[kernel:annot:missing-spec] bts0506.i:11: 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:37: Warning:
+[kernel:annot:missing-spec] bts0506.i:12: 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 715ab663ac3..468b9221629 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:15: Warning:
+[kernel:annot:missing-spec] bts0506.i:6: 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:20: Warning:
+[kernel:annot:missing-spec] bts0506.i:7: 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:24: Warning:
+[kernel:annot:missing-spec] bts0506.i:8: 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:27: Warning:
+[kernel:annot:missing-spec] bts0506.i:9: 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:30: Warning:
+[kernel:annot:missing-spec] bts0506.i:10: 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:33: Warning:
+[kernel:annot:missing-spec] bts0506.i:11: 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:37: Warning:
+[kernel:annot:missing-spec] bts0506.i:12: 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 2621ac4b4de..07c96593eb8 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:33: Warning:
+[kernel:annot:missing-spec] bug0223.i:9: 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:16: Warning:
+[kernel:annot:missing-spec] bug0223.i:11: 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 2621ac4b4de..07c96593eb8 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:33: Warning:
+[kernel:annot:missing-spec] bug0223.i:9: 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:16: Warning:
+[kernel:annot:missing-spec] bug0223.i:11: 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 ab536314a0f..c6369e819e1 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:8: Warning:
+[kernel:annot:missing-spec] bug_023.i:4: 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 c81599c1696..71179e982ca 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:19: Warning:
+[kernel:annot:missing-spec] call.i:10: 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:20: Warning:
+[kernel:annot:missing-spec] call.i:11: 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 2535d55b3d4..8ad9af9913f 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:4: Warning:
+[kernel:annot:missing-spec] copy_stdin.i:1: 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 c67a99bfed4..506b771445b 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:100: Warning:
+[kernel:annot:missing-spec] empty_struct.c:96: 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 fef780748fe..b34af541127 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:5: Warning:
+[kernel:annot:missing-spec] f1.i:2: 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 7ea38337faf..20f02f2e444 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:18: Warning:
+[kernel:annot:missing-spec] false.i:8: 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 88c6c5d8c6d..c466d2d8ad7 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:20: Warning:
+[kernel:annot:missing-spec] from_call.i:13: 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 560d21d929a..da40280de1d 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:20: Warning:
+[kernel:annot:missing-spec] from_call.i:13: 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 38ed36b32a0..c2f6e5229f4 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:6: Warning:
+[kernel:annot:missing-spec] ineq.c:1: 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 e43d5267297..127ab211d4d 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:9: Warning:
+[kernel:annot:missing-spec] infinite.i:1: 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 fec4520ecd5..7320a7432c7 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:151: Warning:
+[kernel:annot:missing-spec] initialized_copy.i:22: 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 1677d41e752..878a548361d 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:151: Warning:
+[kernel:annot:missing-spec] initialized_copy.i:22: 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 541d5189697..bbd39cd72e4 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:7: Warning:
+[kernel:annot:missing-spec] input.i:1: 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/invalid_lval_arg.res.oracle b/tests/value/oracle/invalid_lval_arg.res.oracle
index c9ec64c7b44..624bfc42e35 100644
--- a/tests/value/oracle/invalid_lval_arg.res.oracle
+++ b/tests/value/oracle/invalid_lval_arg.res.oracle
@@ -19,7 +19,7 @@
assertion 'Eva,mem_access' got final status invalid.
[eva] invalid_lval_arg.i:19:
assertion 'Eva,mem_access' got final status invalid.
-[kernel:annot:missing-spec] invalid_lval_arg.i:15: Warning:
+[kernel:annot:missing-spec] invalid_lval_arg.i:1: Warning:
Neither code nor specification for function f,
generating default assigns. See -generated-spec-* options for more info
[eva] ====== VALUES COMPUTED ======
diff --git a/tests/value/oracle/leaf.res.oracle b/tests/value/oracle/leaf.res.oracle
index 7ccd5e0302a..a233e82216b 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:48: Warning:
+[kernel:annot:missing-spec] leaf.i:3: 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:62: Warning:
+[kernel:annot:missing-spec] leaf.i:14: 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:64: Warning:
+[kernel:annot:missing-spec] leaf.i:17: 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:65: Warning:
+[kernel:annot:missing-spec] leaf.i:19: 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:66: Warning:
+[kernel:annot:missing-spec] leaf.i:18: 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:68: Warning:
+[kernel:annot:missing-spec] leaf.i:38: 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:69: Warning:
+[kernel:annot:missing-spec] leaf.i:39: 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:70: Warning:
+[kernel:annot:missing-spec] leaf.i:40: 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:72: Warning:
+[kernel:annot:missing-spec] leaf.i:42: 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:73: Warning:
+[kernel:annot:missing-spec] leaf.i:43: 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:74: Warning:
+[kernel:annot:missing-spec] leaf.i:44: 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 3f486d154c0..640d666d561 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:6: Warning:
+[kernel:annot:missing-spec] leaf2.i:2: 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 9d1932aa482..7adfce4bcc8 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:19: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:9: 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:20: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:11: 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:21: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:13: 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:22: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:15: 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:22: Warning:
+[kernel:annot:missing-spec] leaf_spec.i:16: 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 f47d633f23a..91821a7fba1 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:27: Warning:
+[kernel:annot:missing-spec] leaf_spec.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 <- main1.
diff --git a/tests/value/oracle/library.res.oracle b/tests/value/oracle/library.res.oracle
index 3a3a113d638..adccceb6d27 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:30: Warning:
+[kernel:annot:missing-spec] library.i:5: 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:37: Warning:
+[kernel:annot:missing-spec] library.i:18: 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 441104cedc7..5c1c6d008b5 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:24: Warning:
+[kernel:annot:missing-spec] local_variables.i:4: 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 955ecabd508..c9131db1371 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:29: Warning:
+[kernel:annot:missing-spec] noreturn.i:1: 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:30: Warning:
+[kernel:annot:missing-spec] noreturn.i:3: 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 21313b3be75..a14d8d6d471 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:38: Warning:
+[kernel:annot:missing-spec] origin.i:30: 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 2d7eae48a93..a6bb3080bd7 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:124: Warning:
+[kernel:annot:missing-spec] origin.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 <- origin.
diff --git a/tests/value/oracle/output_leafs.res.oracle b/tests/value/oracle/output_leafs.res.oracle
index a2b97d84281..928c51aa4ca 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:40: Warning:
+[kernel:annot:missing-spec] output_leafs.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 <- main3 <- main.
diff --git a/tests/value/oracle/postcond_leaf.res.oracle b/tests/value/oracle/postcond_leaf.res.oracle
index c667f6ecd05..d5444651d99 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:109: Warning:
+[kernel:annot:missing-spec] postcond_leaf.c:22: 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 fcfd148f70a..d1287f10cc7 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:20: Warning:
+[kernel:annot:missing-spec] postcondition.i:5: 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:89: Warning:
+[kernel:annot:missing-spec] postcondition.i:8: 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 c7c6f73dfa1..450e321eef9 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:34: Warning:
+[kernel:annot:missing-spec] precond.c:25: 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:21: Warning:
+[kernel:annot:missing-spec] precond.c:16: 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 2d9a1fc7536..c2f33d78730 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:24: Warning:
+[kernel:annot:missing-spec] precond2.c:17: 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 8924205852c..9200a22a04a 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:24: Warning:
+[kernel:annot:missing-spec] precond2.c:17: 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/protomain.res.oracle b/tests/value/oracle/protomain.res.oracle
index 251b8e5d9bd..673913069bd 100644
--- a/tests/value/oracle/protomain.res.oracle
+++ b/tests/value/oracle/protomain.res.oracle
@@ -4,7 +4,7 @@
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization
-[kernel:annot:missing-spec] :0: Warning:
+[kernel:annot:missing-spec] protomain.i:5: Warning:
Neither code nor specification for function main,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function main
diff --git a/tests/value/oracle/resolve.res.oracle b/tests/value/oracle/resolve.res.oracle
index d39a8926209..e17390ebcbc 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:12: Warning:
+[kernel:annot:missing-spec] resolve.i:3: 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 12339ab0661..fbe8d53985f 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:31: Warning:
+[kernel:annot:missing-spec] semaphore.i:6: 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:34: Warning:
+[kernel:annot:missing-spec] semaphore.i:6: 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 17a53f17bdc..8c0e0d9b030 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:39: Warning:
+[kernel:annot:missing-spec] strings.i:15: 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.0.res.oracle b/tests/value/oracle/summary.0.res.oracle
index 75383d8c9f6..7a401c5741b 100644
--- a/tests/value/oracle/summary.0.res.oracle
+++ b/tests/value/oracle/summary.0.res.oracle
@@ -5,7 +5,7 @@
[eva:initial-state] Values of globals at initialization
undet ∈ [--..--]
volatile_d ∈ [--..--]
-[kernel:annot:missing-spec] summary.i:19: Warning:
+[kernel:annot:missing-spec] summary.i:10: Warning:
Neither code nor specification for function minimalist,
generating default assigns. See -generated-spec-* options for more info
[eva] using specification for function minimalist
diff --git a/tests/value/oracle/summary.3.res.oracle b/tests/value/oracle/summary.3.res.oracle
index 65b9fa9ca02..0b65451110d 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:64: Warning:
+[kernel:annot:missing-spec] summary.i:48: 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:65: Warning:
+[kernel:annot:missing-spec] summary.i:49: 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 78f84b5adc2..c016f68b72a 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:64: Warning:
+[kernel:annot:missing-spec] summary.i:48: 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:65: Warning:
+[kernel:annot:missing-spec] summary.i:49: 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 ba43fc436ae..03159449108 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:13: Warning:
+[kernel:annot:missing-spec] switch2.i:7: 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 860675533da..90b425ae5cb 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:26: Warning:
+[kernel:annot:missing-spec] use_spec.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.1.res.oracle b/tests/value/oracle/use_spec.1.res.oracle
index 88fa49960f6..fb4b4c41a4f 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:26: Warning:
+[kernel:annot:missing-spec] use_spec.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/volatile.res.oracle b/tests/value/oracle/volatile.res.oracle
index d8d0bd4dec7..5f3ac9c064e 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:40: Warning:
+[kernel:annot:missing-spec] volatile.c:20: 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