From a7b40a45d3405f21cd952ddf1af5c560149ccf52 Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Wed, 31 Jan 2024 11:22:55 +0100
Subject: [PATCH] Set falls-through loc to the end of the function
---
src/kernel_internals/typing/cabs2cil.ml | 1 +
.../wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle | 2 +-
tests/cil/oracle/bts297.res.oracle | 2 +-
tests/misc/oracle/bts0452.res.oracle | 4 ++--
tests/slicing/oracle/use_spec.0.res.oracle | 2 +-
tests/slicing/oracle/use_spec.1.res.oracle | 2 +-
tests/syntax/oracle/exit.res.oracle | 2 +-
tests/syntax/oracle/inline_calls.0.res.oracle | 2 +-
tests/syntax/oracle/inline_calls.1.res.oracle | 2 +-
tests/syntax/oracle/inline_calls.2.res.oracle | 2 +-
tests/syntax/oracle/one_ret_assert.res.oracle | 2 +-
tests/syntax/oracle/vla_switch.res.oracle | 2 +-
tests/value/oracle/imprecise_invalid_write.res.oracle | 6 +++---
13 files changed, 16 insertions(+), 15 deletions(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 88758722b35..cd635b8e030 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/src/kernel_internals/typing/cabs2cil.ml
@@ -9485,6 +9485,7 @@ and doDecl local_env (isglobal: bool) (def: Cabs.definition) : chunk =
(* Now see whether we can fall through to the end of the function *)
if blockFallsThrough !currentFunctionFDEC.sbody then begin
let loc = endloc in
+ let* CurrentLocUpdated = endloc in
let protect_return,retval =
(* Guard the [return] instructions we add with an
[\assert \false]*)
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 5f4ee04ee6f..868d4d0e33c 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
@@ -1,6 +1,6 @@
# frama-c -wp [...]
[kernel] Parsing stmtcompiler_test.i (no preprocessing)
-[kernel:CERT:MSC:37] stmtcompiler_test.i:135: Warning:
+[kernel:CERT:MSC:37] stmtcompiler_test.i:142: Warning:
Body of function if_assert falls-through. Adding a return statement
[wp] Running WP plugin...
[kernel:annot:missing-spec] stmtcompiler_test.i:103: Warning:
diff --git a/tests/cil/oracle/bts297.res.oracle b/tests/cil/oracle/bts297.res.oracle
index 5fc89c0dd2d..dd664411222 100644
--- a/tests/cil/oracle/bts297.res.oracle
+++ b/tests/cil/oracle/bts297.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts297.c (with preprocessing)
-[kernel:CERT:MSC:37] bts297.c:4: Warning:
+[kernel:CERT:MSC:37] bts297.c:10: Warning:
Body of function abrupt falls-through. Adding a return statement
/* Generated by Frama-C */
int abrupt(int x)
diff --git a/tests/misc/oracle/bts0452.res.oracle b/tests/misc/oracle/bts0452.res.oracle
index a954072f5cd..9eb04c5c869 100644
--- a/tests/misc/oracle/bts0452.res.oracle
+++ b/tests/misc/oracle/bts0452.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing bts0452.i (no preprocessing)
-[kernel:CERT:MSC:37] bts0452.i:13: Warning:
+[kernel:CERT:MSC:37] bts0452.i:15: Warning:
Body of function f falls-through. Adding a return statement
-[kernel:CERT:MSC:37] bts0452.i:27: Warning:
+[kernel:CERT:MSC:37] bts0452.i:29: Warning:
Body of function h falls-through. Adding a return statement
diff --git a/tests/slicing/oracle/use_spec.0.res.oracle b/tests/slicing/oracle/use_spec.0.res.oracle
index 03163696bd5..ac13268d3f3 100644
--- a/tests/slicing/oracle/use_spec.0.res.oracle
+++ b/tests/slicing/oracle/use_spec.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing use_spec.i (no preprocessing)
-[kernel:CERT:MSC:37] use_spec.i:18: Warning:
+[kernel:CERT:MSC:37] use_spec.i:19: Warning:
Body of function f falls-through. Adding a return statement
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main
diff --git a/tests/slicing/oracle/use_spec.1.res.oracle b/tests/slicing/oracle/use_spec.1.res.oracle
index 4a1393123e1..a31502ad99e 100644
--- a/tests/slicing/oracle/use_spec.1.res.oracle
+++ b/tests/slicing/oracle/use_spec.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing use_spec.i (no preprocessing)
-[kernel:CERT:MSC:37] use_spec.i:18: Warning:
+[kernel:CERT:MSC:37] use_spec.i:19: Warning:
Body of function f falls-through. Adding a return statement
[slicing] slicing requests in progress...
[eva] Analyzing a complete application starting at main2
diff --git a/tests/syntax/oracle/exit.res.oracle b/tests/syntax/oracle/exit.res.oracle
index 497136c44c5..b1c0da8451d 100644
--- a/tests/syntax/oracle/exit.res.oracle
+++ b/tests/syntax/oracle/exit.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing exit.c (with preprocessing)
-[kernel:CERT:MSC:37] exit.c:16: Warning:
+[kernel:CERT:MSC:37] exit.c:21: Warning:
Body of function g falls-through. Adding a return statement
/* Generated by Frama-C */
#include "errno.h"
diff --git a/tests/syntax/oracle/inline_calls.0.res.oracle b/tests/syntax/oracle/inline_calls.0.res.oracle
index bae30a7ef5a..18da0e0c968 100644
--- a/tests/syntax/oracle/inline_calls.0.res.oracle
+++ b/tests/syntax/oracle/inline_calls.0.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing inline_calls.i (no preprocessing)
-[kernel:CERT:MSC:37] inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] inline_calls.i:43: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/inline_calls.1.res.oracle b/tests/syntax/oracle/inline_calls.1.res.oracle
index 88333fa15d0..348ad3debfe 100644
--- a/tests/syntax/oracle/inline_calls.1.res.oracle
+++ b/tests/syntax/oracle/inline_calls.1.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing inline_calls.i (no preprocessing)
-[kernel:CERT:MSC:37] inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] inline_calls.i:43: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/inline_calls.2.res.oracle b/tests/syntax/oracle/inline_calls.2.res.oracle
index 288f587fc4c..b621c0e9c33 100644
--- a/tests/syntax/oracle/inline_calls.2.res.oracle
+++ b/tests/syntax/oracle/inline_calls.2.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing inline_calls.i (no preprocessing)
-[kernel:CERT:MSC:37] inline_calls.i:40: Warning:
+[kernel:CERT:MSC:37] inline_calls.i:43: Warning:
Body of function f1 falls-through. Adding a return statement
/* Generated by Frama-C */
int f(void)
diff --git a/tests/syntax/oracle/one_ret_assert.res.oracle b/tests/syntax/oracle/one_ret_assert.res.oracle
index 96cf184dbb2..4f0a21cbe7d 100644
--- a/tests/syntax/oracle/one_ret_assert.res.oracle
+++ b/tests/syntax/oracle/one_ret_assert.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing one_ret_assert.i (no preprocessing)
-[kernel:CERT:MSC:37] one_ret_assert.i:8: Warning:
+[kernel:CERT:MSC:37] one_ret_assert.i:9: Warning:
Body of function g falls-through. Adding a return statement
/* Generated by Frama-C */
int X;
diff --git a/tests/syntax/oracle/vla_switch.res.oracle b/tests/syntax/oracle/vla_switch.res.oracle
index 6b882536984..5e448217274 100644
--- a/tests/syntax/oracle/vla_switch.res.oracle
+++ b/tests/syntax/oracle/vla_switch.res.oracle
@@ -1,5 +1,5 @@
[kernel] Parsing vla_switch.i (no preprocessing)
-[kernel:CERT:MSC:37] vla_switch.i:16: Warning:
+[kernel:CERT:MSC:37] vla_switch.i:20: Warning:
Body of function case3 falls-through. Adding a return statement
[kernel] User Error: vla_switch.i:7, cannot jump from switch statement bypassing initialization of variable b, declared at vla_switch.i:9
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/value/oracle/imprecise_invalid_write.res.oracle b/tests/value/oracle/imprecise_invalid_write.res.oracle
index 7dabe5398d5..229134d6c79 100644
--- a/tests/value/oracle/imprecise_invalid_write.res.oracle
+++ b/tests/value/oracle/imprecise_invalid_write.res.oracle
@@ -1,9 +1,9 @@
[kernel] Parsing imprecise_invalid_write.i (no preprocessing)
-[kernel:CERT:MSC:37] imprecise_invalid_write.i:5: Warning:
+[kernel:CERT:MSC:37] imprecise_invalid_write.i:6: Warning:
Body of function main1 falls-through. Adding a return statement
-[kernel:CERT:MSC:37] imprecise_invalid_write.i:10: Warning:
+[kernel:CERT:MSC:37] imprecise_invalid_write.i:11: Warning:
Body of function main2 falls-through. Adding a return statement
-[kernel:CERT:MSC:37] imprecise_invalid_write.i:17: Warning:
+[kernel:CERT:MSC:37] imprecise_invalid_write.i:18: Warning:
Body of function main3 falls-through. Adding a return statement
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
--
GitLab