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 9d7049d26d3e5a2f5e601c0181fe78ad91a40506..8cc9fe1473e97162af7392dafb7d6f087abaa39b 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 b5b842d5b2f6138213bd05c42fe685eca08c60df..b55d3bc882179d6fa400f66b8b496a347840a329 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 67745c5779d052fc5f9d8e06f730b6de85791c61..4a5816b86a6ae0b38e600e4e27e653fbed159261 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 67745c5779d052fc5f9d8e06f730b6de85791c61..4a5816b86a6ae0b38e600e4e27e653fbed159261 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 aa890a27d2eaf81204b2679e9b652c55f84e7505..a7964a7178444b83d18f141968cd2436c4717eb4 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 f6c71b561f1d57dda05ff590ad68ec28d4e2725f..1583f80fac71fdb1219177bc5ae8845b5b6ee423 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 04e470cae084770d27509d7d77a08100446f0b4e..574cd52a0069be1934bf553a6c84a1a8705518d1 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 1ad19f92ff2ead1802feb431b5e74cefa320c970..210bc3fcccd9d22840a20e01bb926ca77762e03c 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 612c1e14816c0e33dad259cb05b25515cff2ef49..fe76bf39773e4048f625546be213aa2935acb512 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 546cc9cbc967bf5527eb98b1756b7fcb0ea5a3fa..d71e190f20c4c590988ad47950016ebb59b48cde 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 8856945b2de6fdfa24223f52d7f1a3cbf28cf0bc..9a4ba24083246bfb3bc2604909ac060a1b753a3f 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 f59a25caa33749eac1627834a0653f79e5f8432d..72bb0792e2b205bfdcd7b0fd685a05064d38c409 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 c47d7de999a531a3245ac5691bfe0d1a10b210a3..c3a46f89849a1e640932ea178a30c7216f3df892 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 bc7ed6281c8f4f33bfc79c027ebc4c0a10ccb3d4..b77faefc9d613a0106df282b2ef5979964433b20 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 b2c0657c754f9d9d0032b7b71b7aa9cb78166113..3d7544a2bcc9e2209d69c52f5b35b51b595bf064 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 73007ab0ccb49e2c3c57f1386ad2f9c1bc0b4baf..5c1cc2988c42d317d063f920b774f25ede003a76 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 58717791f3583a56a1d5ed9efd929a3614c3f27c..a9c2ce7a4bf39fcfecfc3b8c378e394f247c6d3c 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 5fbb9d01fa79fd95978b20155226b37111d641b8..a900ef19ea712935c05706281be977d7d7275378 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 3ffbfe423b847caaab95f29168927be1e2dc59a5..0c9e683b20cbf32d474846a6aba8292cd3f4680d 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 6e687acfe0e60bad387485f5ab3e703bfad13aa9..8025cbd92d5a2054d0e5d95a26a083d0e3bc7512 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 8725172d792b04b485a64cc11abcbe48da6f4d9c..54ea4910750e8d63276caab770ef90859aa68357 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 ab60728bd8eb478cf20ba97268972c6bd8a80227..bd5b5017ddb73a6a15fc3c8dc6add36a05d4dbc0 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 a9bee4f8d44eab51b8818d92839475b15e28066f..b0f695ca4af462d87d907df540d33461fcdc16a9 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 2fa079d75a88f9f318196ed66399bcd884c14431..5d7bccf0c5814ace1caa8cbbde5aa950981a5041 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 74ea04f2c8f1a5bfd993c56fc4632ae881ab3cb7..db382b8430b52d2ff580dccedea27581e62e376d 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 da138c294e84e0e06e29e3c8f708054cd5cd47d3..c5b43790ae077d785ff5686b38e79d1decbd6728 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 fd420fb5cefb91ed5483fef95dfad77e0c1dc24f..7814251c927f4204a00d3da286851e805f873c77 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 6550a1739aa7e28d8ff5842aaa332d86dc229598..c45e5c55e42286d073d36c97efe49649e0278e39 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 b7ac263ec2058e01fc0fdded3128440de3340ec9..f332052289ba16f68075e0f3a99506af0ed3a7d8 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 96c9680ea4b2dab373d1c3ef0f45d8451e8ee2f8..a6bd5f6a94dbe6176b9d68cd0d55f644fe489a8b 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 4bc1b2c08cd50b61c5c8daf12624e722166eac3b..d89586c515938a81c024ae110fb64ae6f28a756e 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 24ae14ef3edf4177b13465a291293e5c01f92332..83a51e8e270e8514626c540b1318d7c95991802e 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 c9e134a8954e6b7227facbf6cfca62ae548aece6..16e5f57c14eea74cf2b275b36afeb9172f543eda 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 1808e3fca99efc16fae27d2920e7681d46b05b64..c2759c1dc2d513c7b615922ca13ba4b7894e69b1 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 e78d5fcf6c39b1013e03118655f6afb409c88ba6..6e56a2ecd321d5fc5b0d0f4df12f211ca508962f 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 284392617d094b7ad2fc0fa002c2fef5cfa82bfd..8686a159f654afac7917930664644e810df87329 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 220dc834c2ce47b08d130a1baa34b50e89c5af1d..b75471e832b42aac3b06fa802006378cd910043f 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 a868d9e01d27c4635adc9ef5610668dfbdd888c6..c4b916a505881c87138186d7ae57ef16c8f2ed12 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 e08205f29c522495446ab79c096e8925206ac8aa..5c05ca58156728597c2b39923ce8a79f19b3a075 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 b6025b1fb434f0aaf0d561fd636c6dea1025ffb4..41b947831b30ab22135de6b0340821d5e455f785 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 f152e8322484ade5b77ea3849d8012e381a54e70..7f261f2b181248ea1907806ffb30351b06873fdf 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 028dbf91926150af06ae7760f138a4cf76f2963a..aa6880fb7a8002659ad6b2f83d476c67186e2d60 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 5ca07d1938303d67aa23bf2d0d3e2a504edf7d4d..51d45ab1772c5636baf79ca63584ed8e1c572742 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 6ef2f2ba5281d73009c20c2f5b7542e8fd0d13bb..08f6f3da3ece39ff45a5efa82360599d881fb4fb 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 b28bec3b1e277a83b5aec7e646eb5ee5d1c16c62..5f674e1efb19b5cca4d23449fa51f4439e906cc7 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 5d8a5fcbfe26238f13127a8ec8bd283d677ed44c..64468eccfdc352be842a36574fa385f9d9fad9e7 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 58f50450f29b50e08658fd4f5c1c2c176f8faf79..1a2ff51103f65b9a6bcd3762988e9d3a0b464d79 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 100e72638ff7cf080bec2d2a7866dde5463832ff..8aba1396eac93c41a6d29490d79527feb3bef3bf 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 f011ba6e6199f72ba1a31102846bdb9bb6243404..ae45c27a84982e4e0716dadc4e323addcbc86c3d 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 08ba9fda9b40432487b453bfe6edcdc5959f401b..cedccb6ee995a9b68bc85daf9d9e115b36f1583e 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 5600c67c9f14886e9b4c74acf3be65cbc057d543..206fb19d1e16059d6386998404471148087b2dde 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 53454a8d95afda5cb9ac32385d31b842dac540db..e1e2237a8bd39e1ba095c0a30e7c34072d9f668e 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 ad445cb36a89cfbe6e3c03c1632afbc249659b1d..487fdfde99fb540a8085280c1dac002c8a4723c8 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 077a078f07a34509b34f9759f7ba4b4c0e6ed411..fb52594bcc87e022e725f4b16d2423838dd39ebe 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 c67d9c625156eb0cb6007b71533980469dc4ac25..3393e5f23a8d7578b823bc935b6f06169afd2e12 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 ece1dcad13ecc6b3f27fe571056806fa07724f48..d496878a57a0a33a83c722b13b8ea574d2d02185 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 e2a91126f380366f181b2d6c42275e0d64496fec..972163f389dd6016ac0442b7cd086d804742e725 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 0cf211b553ef4211e67e8e3fa41cf9657684630a..2790756ca0486198539da3fb7b5f9aeb9cac2e0e 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 d53a7574678abe2dabaa5c7d6a8f92b51fa191aa..e87e5788748006fe91385a00275223b6b376375e 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 78f5911e4a7156b32bdb70911a968f71588d15cf..7fac07c71df46632ad095c82f6fb57c7b3894264 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 d60e59736dae844128a526ced2351e97259e0580..66f5e7acb19f0bc61eccf5c873bd071da5814bbb 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 f48689966c0cf9953790f7308aeadfc8ba1bc7b0..23779fce06431748fbb48bf87b23110835db43a8 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 8973bd52e7ae00df74630f74bc0f08dcb1310efb..603ca3e28447eb42cc349eb133735d440d779ce1 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 373717bf271970cd9a1fb8557738f03d7a43db03..0984fa19a4d8bfe359417cf813ca8fc0915768a1 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 2bee8bfd762594ed074162de4968e047b5bb3679..7498622c2453df307ff71a8603a1327b62805841 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 b0e4f5db096019533a7a5b2b8d2b3bb05ef34761..412c259fd50a05d426f9adfd9a10c597ac125982 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 df508e5d6c438ce1183c97d92858bec5ec444d34..e657b964114e2f938796dd663bd6663e6e9ae815 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 d4ee8d50d032f1e6fab60ad84fd84d05c8c2ebb1..27ada191a3293b330b02f2b6628ec92dc85ab075 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 bc169708e5bc2c84ecf6d7b2538ebbd7611b688d..5ad0f3b323bec4976f7e66ce4c0913b73e6e4c44 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 a45058cb8989af726b3b2a7bf0a2c492dc9ebfb1..15dda274f30c93b3e53ef8efc797f8e498cda9ae 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 b64143a7e576c1148033632a3cd74eb5c60b700e..6e978274306531d7caac1812e92ad911a9f0854e 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 6d32745d1b02c8ceb79e92661cd9edcd9f5e2e39..30155d0cc1776fa23c3cd7ff162dd3e21689e1de 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 7eb8cbc512c7dd7ab1147b4af4cd2b2f96c0cb07..69eb74ce4a3573000101f550cb1b72f670bc6ce8 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 111eb5994768076770f4d454cf8a250aaab34eb6..c8d7e2c4d4bf3a767ade19f8640f1d4d159ffe6a 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 4e3111b5d0022849d862d4e99052c71296088d30..89383cc7912f957fcf57508bbfc238374816bf7c 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 5204d3ea928f2d8fbe653da4f87da396e2b61ff1..1a83bef8646e5edabade9faf9fdaae9bfd547d77 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 02edc7f29a86b826e15843e165912a83db6b1ad0..97c595ce7123f275f517c8d29dfab4ddc0c33347 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 7c1a8df24dfd5588a74ff523baecdf85e80cafae..a246c6de55ace8eb47c79ef356569dad91fea2a1 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 22222bc2aacbc192c237b75bdfeaab4314b2524d..ed164092a6a5636ee93f30314702c6152c6d3dd5 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 2d7016cb262fe25ca6633576337ee357d677d885..ce3a3c2a489e3974a489992a3833c95b2a0c6f31 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 94f614cca0a6e7b07b3f7808deae7b0815ca8f4d..9661edfc6e0768a0a4563b88216ef26f8a628299 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 bd08bb92439b4a8d2587a467ada84ee624dad90e..6b28d3e6c56f30952dd9cc79d8ab36e362ad4e16 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 b4d4733d9174d88e24ffc687e25e4d15ddd5ee7d..1e501dfc8b4f34b5641d32ab5a0392d4a07167fe 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 01e765f74b0657f98adf4531504ffc36c9823a12..3809bf3497a8d3961e3dd33a0ebbd6ffd79c5716 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 efe7d6c6398778a26d99ed6f277347db93974573..ca9ab8cc5bcc6c435eb0ad90ecd87e50aad7e1be 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 110353a5ccae0759dc0d84687ede9424937008d5..1c624742fba9506d0120b3bcd157ed8f875d7db2 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 64da29a0597d3ac282529251b632843281f4bc38..3c7b07486709c52c638820f8ba9a7fb060fc7218 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 18b970df444e4038f62bb14eb64e5ec612adf242..a65568abcc482a114b14543cd979eb1c64d2a69d 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 acf750f7fc7e2883c21e4d48825ddcb1e2ec726d..5f0af4fe428f4817ad8b2b0d766957331093244c 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 975b6c1a98e84a8e0643d1da38f45494b0abc795..ba7c315cccff32e487c7a13a20cbb5e51cfebfdc 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 9fd462bcb24a07984cbe4e86e1297a9fd5df86cd..0b6a82d32ee8b5c28fd50601fba918bf8633d474 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 cad1b0604013ea4845ec40726675fb0f82bbe53d..0a690a35fb37b5d92740f20cee83a57a6976d9ee 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 2cbd14ab48a28ebb45bb2cfe59ee6c74106e51fe..e77debabe4d2e33c529827d1aed3170b6ca86972 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 073800f4115f851f671343769145367192e6bd12..f6036ecc4faca35c662ee49c9362c3c865719fa9 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 726662f7e0d78991f8844cfe11f1397ebcf12813..dd18cad9e65de7931c553886d7c8d82281763e99 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 5d4fe926d54fd6c5ae44a737db8e2b65b8d5677b..0cda5b17cded23521736dd27086a8128142a0dad 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 04a864ff382a7e169421e1efe1e4401581e57c13..4f0b797442e5aee255518da1bfd2ca6fd92c4632 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 45e2e5b619105ffb3de4db6326acc4030ba4beec..5ea6c7a008e2ae116df40663fcb0f2af34757530 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 87f3dae909c810ed7d3196bc2c408d991520897d..78aabc7629ff42349f136b72a65752af5436553b 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 6c3bee4acf315ca851431a8100aabe48967a83da..047a99c8e945a61c3d67d735fc227b6f54e1bb2c 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 e5de9941760551310d3e1f26e7eaa08f9c620de0..cde9b9ebdde2198a18aa75377bf1f6aeed29ef40 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 9b4b2a0f20bc28ddc7bd898f667559691ded6fe4..63bfc9b7a277633c38d91090de66323fe8b341a4 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 178bb3278c02a3efd47381de335569cabf167d45..47a035a0d9f816ae1828c875bc9c37302cda39e0 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 a394bebd6a6ab71789f0fd759e5a1c5525b68034..e3871fd3d87fc33e5d60e17c0ab00a0560c912c9 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 f466ab7ac093c409ed262244406e15fcaf842df4..fdcad002e61f1ecb7e2d2cffd19d925d9170c366 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 a85c8c1ecd4694880e5d4949e0d4a5fa8a51dbe7..a6bee706619a94a3b5c2bfcf3e84b364161772c2 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 1f98d6f3ef1062090ecc386a21c7e46ef9898341..cd9c16cbac368d3dc7d86067e46ca10b7e6a0fee 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 7918bf2ca4e2372101e792bb98d50a7251183de8..a0845a156c5d74f5deb8bbb903c2421f9eae1891 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 988211d29e3251d1434e265cc473a9b7a675e687..b8d5147e8449383517a5a34c71853c661d8975a3 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 769500d84d8314be9f397932a125b0d26fd6adf5..3b7aab4fe8567889ca90168d7d5ee8ec9d412842 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 feed01b3a62a32da6addde70735ad325af67505c..d8ef7a2822cc0dfbdc223681d986bb8871f77d91 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 75357eb578c2958a0b6622c63eb334667610ce94..db410543427d0dcc1cc73e0c03caebf11985490f 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 1c1c5920893b474fb648f90eb55916b0c4a134da..77d7282f7485e1238d8b6ffab084a13256e6d2e1 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 2cf898dc5445295a4764781ccfcf2930d69ad397..0ebb63a19965f94b66189469f1fb162343dfd50c 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 9bab22454a4ca0a5c5d1eb898c853b19ee727335..e80af681484c8703d1d0f79ccb1b708e08f07893 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 04a122b64516b8f528ae86e0cf9450df1463929f..3959136da4ceaebcadb17e718d3cd053d06d4ae5 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 fd1fa6b4d75cbdc0245114504702972c1b332b30..c3a0e8506c5b87e33fa4ac27b39f32177e443d32 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 e7783ec0de811be1c04a2ee8eebde4910c4d27f6..b934f52d140f92573e6a4b0e1c79c3970af1e60c 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 333c77abdecacf5ac181f11235928ed98ab43e6a..97efb95010b49572c6062ffb9ff76e6dc6c66472 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 35cd5e8e21eb83704a80a654c59603fbf3c1e96d..3d590ac884dd22d217421a5250b3d0574efb2f47 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 25abd7c442aa93c7ad063c8e3989c3dc0674b07e..6d50c819a40bc6581d14d59398dec2b984d54a3e 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 71a60f4e33e15d0d464f1d2f159717960f91d55d..966959e2d01dcf4327d94bb4fd867d8f8f8bec14 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 374b5e578764b4891273f5c1627004a2bfa24f5f..c3a9979aff7c068c856b9714877be1f8a9bbcb20 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 490fec9745427b9e85e9e5085cf96bb2da4654d0..f7fe215fa0c78dea22e1ada7321be5a870123272 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 133365cf41b2999b102ee518bc1bdeda74a6a391..03b193f4a42a76130e92d1e0c344abfbea4d9235 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 22f1c275ac6b52a593a0c791694839a8cde3e40c..9db6296f5e25a3f6d0ab62dceb8f25d954ba4889 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 c2e59c2a9427289d81812b4d653f651f21ed1a8a..e8cb8185f8f10df8591e6e56d655b4610afbfc46 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 76d57c2c3535dd9adb61d6a4f2b87df92fa4dba7..da8a8c63d9bb0fc49f3b85f8cd7be3aea62ebc4a 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 c4c03e484a928e1f29c50395046b0a7b9501550c..14dbc9a6b57a5b3e1f97981206234c9bf0be8e25 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 30dee131fa871ac96f413368a1dfedf93387e935..f5f8270f8535643169d06dddf701d5512f816d89 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 21d015132d357fc1d31c4f33db37966b38664d7a..1d1b7c31dd1c003de86a702e2aa30e01d47e7218 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 1aedb324dc395086c2a3b9b7270efde9edee146e..e80ecd16453c91a18b427268fff08470fc5b80f6 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 512580d248886fb56b1842c5db96c01a31b74a47..c992fa8daa7b0bd9bbcf6c01a6838394d065b1be 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 0bdd4613f7806fd5e1e2fdca4118bcc864b80afa..dea84380dbf6320266d3ddccee608f4b43673542 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 b9b128bad9c1cbda8f696b28830c677e356c37e0..5d06e5888064e3c7a8d8f6d40fdaeb76e44e81ae 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 2a25d0ccc9411c94fdac081176c72eec32317b15..045c7b13ff6ea63b03b0cee3cabf8b425d29c411 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 4f6a431dcc0bbeebf9682b6d4a9328ea1100950b..80595d9f5e0ddc33267673b1da87cb65c238a1a1 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 24560b33d23b5d67824a153a3a76014d300dc0c2..a77fac918a0cffd1dc285664d6d43804c77036e6 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 1aff238e6d11794e8df6f5bb26a74905e86e1015..beffeb890cd9c55950639b78e7e33dd0f15a9d0f 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 1986a1f5e3acae8a42ccbfff0539ce6e58d672af..eb0059d622e8779783da09ecaaced90068b84bdf 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 0b66bb17ec39fc3aef7101f8b3216057365a516f..a810b5fdfcf631eb56a67e3e5296cc523352c949 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 0a9c10c832f9694dc26c279a627e8db65ecfa4de..64ca689f84f1885fe97d11c9d5ca9730e19d08c2 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 77cabccd7a93c56b2af0ebead53f5ae64093c6b4..7850686158e8a9f0b08215169999c5ce7e781c02 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 66d2c8939ba6cc1a5e72a993939498f530b7922c..6d026acbd80d0d0db1232c13b51a8371ef6e625d 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 5b6b79c6c3273b7b0181ba75668b10a753852bd7..ce7ae154cf42007a31d32068ce415fd770b27fdb 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 fb4196860a838d812844a6f7f39e0e4689f8dd63..42af2bc05208f6640bc25f832c101960482a944d 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 f2a805d61ebcab10eb8ffed699629f3d5d4db38a..a709300a7c3c960240afb3b83b6cd441c9fceb73 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 8543cd69f0576d2e3509e25d28eeead1781fc0d6..02c2717dbd5bc41c8b91d54ae103cef10aff51a7 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 bfe24c784f68a522a6c45c3eeb6d8f346f579a0e..3e445d2ee61d9004c2bb38673b8dcb3042cd63bc 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 e0d303d726da106b32b701381aaf68fd1b1eeb53..8b0e71e1beae5867d5e70d8664a9fb82cc1e9ba4 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 7363f61184e4ad68104452285ae3331fe8fbe153..41ec5343c9080aa8e73ec770609a0459e3e36eac 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 9e74fb164a5a63cc7ad12e92e361720fe5b30f93..ae79b26d9eba6c5fe60e613fa7b6d51e46dc3636 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 f16981aa5190127039b88f0addd54103c6223579..8dc524e75733120acf9050dd1bbc19ca46cbd4e0 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 a8135ee708771ca78a171d66ef670fc1c381e99b..fd303d6963633fe30f901799fe59bbe12a1e9746 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 9a83feb26ecab703c3a44dd68bce6420826dfb93..a439aa19915f68afe48ae2604870f08e530db0b4 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 37844d3957e7991eb0b2e6a9372e847eef0557d6..8a3f0ff6239bad95fa818992cf182f29751854d9 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 97703a34e75a4f48cd0ca75a4c9322a08532979e..a8e1db664dd129b3cb83d33ad805eb8b3ee809a3 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 985169fe22a2d69004506302c2567c9ef8e124f1..5a7ab392ed5ab4805ae09ac79e7d9a99db9a2e75 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 1a4a5c83d40bd85634809e53317f239f4869268f..bf41616d75ef10bde14b689e1ddd064222ab2d42 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 e0f32464a55fa4ff846a3de523c421e046cb6e15..675b48c03ef063b32784a520ebcb7b115e241632 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 e9aae04102cf11c25c4360d0765e4289e730a57a..513c091207216e9ae380f0886948c57eda519f49 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 2deb200cd14fa733adb3adaa914f5d8afa878cab..3c0aeed56124850440c8b4824a99113fa77f5e7e 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 f6734df8ff538b1ce63fbaedd30545ddd52fe50e..5f609480148ac5fe0f9f5a6d6a32863b73f4d214 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 dfb4b2c3bd69eec1ad6d2126ae79b54f4b7c6f85..15cdd9f542007368e215c2cdd80119efb78f5f7d 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 60f4918fed83591558a3c37f5878d032927a55cc..556f2cf86e09b57274d59a1aeef92d3c151b0ce1 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 8c405ab8eb899726c07780bab2c2089e2033a4cb..9606c29d72d93c1ed25a7b4fa52b3739ace74462 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 532c28c20668a2d58a952e25c9379c6172a0f9c2..14aaddde6b5543582b5319c9f6f497e8d0201ae3 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 8650b514d9c9e1748034d9d4b547e795ca8d87c6..b0835a0cf758aefdceb7288ac0f385f4ba48d562 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 c8160927ebcc4cdb540c643528cc75c9bad3d4d2..aa3e4f78d17cf2f32ef1feb087b2ccaecfaa7b98 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 c8160927ebcc4cdb540c643528cc75c9bad3d4d2..aa3e4f78d17cf2f32ef1feb087b2ccaecfaa7b98 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 046c3ca1741d5bc1d9dcbcc01efa4b654984b5ef..c23af3da53b7376765cc26d3c74e96b534f1ad5e 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 2f9cd06339971284b46828e43f46b1e27d071083..28c6ec682d7781f9212b7023ad44692eeeb1633f 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 d88f06cdf7383cf35330ccce0e3350561587299f..961924551365472a8bcf0098b2755db738189a4e 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 88889b31a6ebb87782521310d609136c564fb618..f8b3fcdd6311cec46e955d01b47e8fdb3ff007a1 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 340b1dc3072098bf7696d0552e94c0fd40938195..4dc9557ce91aa5534d0f3b16117d192181580495 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 18fac29622d188087b1d0a1a7305cd4ca3305650..93f6885a56ad9fcc44ba15452f34b35cfa3c2b0a 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 17ee15d0759ab215edf84c5c835ff616cb038eb5..5c19b7f3ac33f90fdc057eb791448064478c7a44 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 63bea7f723a610d40fe8c49a5a6d9eebb8e81509..f2b7c7957835d7f1b921728b116f24f56501fb95 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 aa92fa03ae2833c28187479f8cae08109ebebbc3..b567c18cda80532edbe47cc792a71480f6b9257c 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 a3d53ee69861eeab31ce2f70ad358ddb667555b4..dfd2d66bfc890ead448d1a55f0f476a200138a05 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 b978ce8605c38f7a96761359bc6ed8d186a2f4eb..c3356f555eed6716403169166315e5a00f7547d3 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 728ce51af93543be68e905a91274e29a393ded31..5e34aa21316d28649bf142b8cfa6524e349eb07d 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 720ca104b63c74ffef25d0c52b4a492790d5c412..e54b238e14f0b61295452af3d4a016efaaf93490 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 0841097ed270800ecff3e6d4c1897adf0e059a15..8502e33961180d58162260707d1561f433f9666f 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 8b3889333f7004b422daeebb545e1a8f7aefc2a7..f3c764eeca96e30d3f705bde31cf5d2f426b1167 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 286ed55307b6f1575fa74f51b4b6cbbd891b150d..b731f757a61d7f70694c149e063da2645fa401b8 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 b88fb59fe31c1f4c1ea8a8e5f298cff5d9533ab9..68a09a7507ffdd181575ed6c024370900eaa197a 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 26d552ea577ab80091bde8d2bdd06be1d4eb15ea..78fff7dc521e9b55b651f06401a9629fd669497d 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 a330ade6cc97a3b5880801493ef4e0bb9d53d98b..85761c8d8bbbb1d2922643f3bd4b37af08e44c00 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 00c309f12714144030ab6c61729cca8f29b8841c..1e6e902f9357867d48dcf93252318547e1d5b75f 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 dfede74e22055e1ce8147114462dd4c006b52cb1..9dbaf0735f618c9a503619b4c408d748b3d08615 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 ac0f46d51624134e11a9feb2237a26b50d19aeae..ec63e420cacbf9b4253d6632a1e10ad991321f50 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 744d7aab558ef0bcada92ce5326773be1186e880..aeb161d74fb1c943a0c6498837de72dabf40ae2d 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 002087f31ba8abd39638d82d19e0589a787a698a..d149f5e7fee3176c7bac0fb21cc75b712919aa94 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 d7a242da6622f0d09f81179c562781b550a91ec5..d2d671709e27d2725f41508e714dd8e75508a4db 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 980bd317335a3fc4d47b65acd11b2e391f2e1c3b..1124da3762a7e24c52124cf328fe41cf71268b53 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 45acf78958063456e7bd3d636503dc555b6f337a..4562b5e6847a1f10ecf340b74606e3067d46b318 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 c372fd704f02d2887858b5cef8cbacb7dfdc6538..f627390df62fbac9456554edead6233f2054895b 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 715ab663ac3f5bd499eda86d27aeb439fd4c55f2..468b9221629aaff380c30367b5fe62d1f3cba505 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 2621ac4b4de53272c25dbca64d9e597927472140..07c96593eb86d7332b68ff7008d1e91c8ed21904 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 2621ac4b4de53272c25dbca64d9e597927472140..07c96593eb86d7332b68ff7008d1e91c8ed21904 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 ab536314a0fea188dd3003ff411aca43274b0bf4..c6369e819e15f9ec3e0c235c7c776b43bcde96ea 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 c81599c1696fd0f2b15e0b6e7c4e2e99f82cdf04..71179e982ca3c33b180bad82a9fef8156e79e77c 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 2535d55b3d4599d9c46d52d07d8f890d1fc21d60..8ad9af9913f57f1a546f3d30cce4f88ce96ec707 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 c67a99bfed4c23f7e2f3276860441cc21fd2ad5f..506b771445b86bf078569652c5e7bd712d00b59f 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 fef780748fe34299784b7ffd26a2c428f1efadc7..b34af5411275132527ff82b086087bc33548de07 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 7ea38337fafe1df2dc07348e408bb561903658a0..20f02f2e4449d7a8787b9580fb5606253bc5fe79 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 88c6c5d8c6d416983f927de6f9655687531bbebf..c466d2d8ad711cca58ae20346ddaaf4da479bc1b 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 560d21d929a84ba7eec01b95ef43454445de32a5..da40280de1d449c499d3cc363c11c5f972ea7a78 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 38ed36b32a0f241d5ae8041f18fc436abe50c118..c2f6e5229f4e7e9610249663eb48e4323342853d 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 e43d5267297845bfc74c8316c725f4dcf71806c7..127ab211d4dbaf3d185c6ab9f36ea73bbe7fdf8c 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 fec4520ecd5e94367e2890286d05e3ac8c299baa..7320a7432c759f299172509931b87ffccdf76974 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 1677d41e75209c183f1158c9395466d3e5e020b8..878a548361d1bc08e0af09fba8a15570ca5a8dce 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 541d5189697e32fffaa76c7d04371a3348d1d0e3..bbd39cd72e44541bbb912112a80814ffe9d7081f 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 c9ec64c7b4440c59cd2e14b0aee366e1921edc85..624bfc42e3560e6a6cb254edba0fa107d190c792 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 7ccd5e0302a676eb3ee7293c6683d039208b0eca..a233e82216b0c479caf3ad5bc2c193ab1d9eadb3 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 3f486d154c0c0f64d200520942925f611f485b1d..640d666d56183fac609c60cfad8abb8e780df2a8 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 9d1932aa482eece15fb1af19cb6a2e1c98beb281..7adfce4bcc88cb2f795ae464c9131bbe9bc6c05f 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 f47d633f23ac1ee42e1fc1f98b1918dfbd95d7a4..91821a7fba1fd39ca073bf9028b810a5e4762a53 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 3a3a113d63804454659655d9caeb4b00194905de..adccceb6d27877ea5faee59cc926a814a5e263ba 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 441104cedc724e860e17e463d445524e240a514c..5c1c6d008b5143a5875d87dd5ced5934eb26d1eb 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 955ecabd5080090c944da30f12759bd3a50a0f61..c9131db13713726af019c2c2a6eaf68db5f73aad 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 21313b3be754e82c6d4c9570db9f1ae65208e409..a14d8d6d471f2d77f43d01edd894de4da5348dce 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 2d7eae48a93c4432e4dac6e0f18275b4fdc43432..a6bb3080bd7126ef1ce1c4e5ee0ed473a316487b 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 a2b97d84281ca7503ade5338b8e41e9965588c11..928c51aa4ca5ab0cdca657fa2f8818aaa4001e29 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 c667f6ecd05deecab8b4a69cdd4a9433b6dd14ac..d5444651d9968404388ff92d571b577bf431639d 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 fcfd148f70a8b458c58ae8c8daccdeb8d74be096..d1287f10cc7f44b1a5e897e92a5a7c7ecb9df523 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 c7c6f73dfa1e2cc2ff7c62247190ba84d74f8899..450e321eef9a9de3c1211abddc972010236bd63c 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 2d9a1fc75369fceade9e8e1a44cbf918fc2f2935..c2f33d78730097749ad37db31c749de5a2523471 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 8924205852c56a0c05aa8786e6209be420a706c3..9200a22a04a9873349f0ad16dae49ca79ef983a1 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 251b8e5d9bdf0ad5860a3a1b2ed82eae62b7d86f..673913069bd1f12ad42ce7a73b41d608cabc5b5e 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 d39a8926209e0a0824c168db6e5b23f109460d5a..e17390ebcbc2958fdf124494f6e52878910f5925 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 12339ab06615a383b8a0d157b84099221cd74e6a..fbe8d53985fe4d5b33edd0c1a43802243305f2e2 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 17a53f17bdc53a87de17f235c7ae66c7f93e46f1..8c0e0d9b03025094ce24f384ac44ca4617ef87d7 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 75383d8c9f69149787004165cbdf2d52204e292b..7a401c5741b41c2854d7ca4267bc2771c0b9fe95 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 65b9fa9ca02d563fb33cab39721eedcf84ad9f11..0b65451110d25e3ca57c7fbed5ff0928e33cd0ba 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 78f84b5adc28a23ea09391128d089ce0c39e5da7..c016f68b72a8853f972d3552238d4ddd7e0ad153 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 ba43fc436aed196825091b57f2c702586fce25c7..031594491084e4815a1827666ba750ab6503676c 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 860675533da474100fdec794e7fa88d4b497a4d1..90b425ae5cb8d3c589344375e8563f217aa685ad 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 88fa49960f6ea16fb0c275670748ff79cfa95df0..fb4b4c41a4fa710b822eb5dc598ed31acb91b0bb 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 d8d0bd4dec754e5d4993a0ea299b78db456953f4..5f3ac9c064e23c84d968e1fcac001d3e42260a33 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.