diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 88758722b35b4392d5cd6f5992a3453ff4db83d8..cd635b8e0305290704c644f46d887cdd3fad8de4 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 5f4ee04ee6ffdd79f6143e2bcd7b2cbcd7c9bd36..868d4d0e33c65f43115fbe4a9f7106cac2f673d2 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 5fc89c0dd2dda67a2ccfcccaf525e50b20d48ed5..dd664411222826146e76a9badfdb3c5a3eeac885 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 a954072f5cd6a74b22846cef82539cde84f1b323..9eb04c5c869d7e5639526aebec450390ee9b6da3 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 03163696bd5ddfb298785dce8b9645c62b36fe2b..ac13268d3f3b619039669269dca7e9f107595582 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 4a1393123e19554421d78748b6751f1109942a4e..a31502ad99e2832eb3faabd36931f827124eb3f2 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 497136c44c5477f9adf7df0bf6afe5f6c2300dba..b1c0da8451dba83ec07bafa6d224454de4d17fef 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 bae30a7ef5a11bb4af12f713e1150f946ec853f7..18da0e0c968c55fdbf22e7452c0f5d4c758bee6f 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 88333fa15d09fa47b3bdaa0243ba7fe31769aaa3..348ad3debfee0a5e49b9c024e5dd1c54a8304d08 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 288f587fc4ced8a89e18b78bfecf6f03a7e9a0cd..b621c0e9c33bfcb4ec5bff0caf5b703c58f082de 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 96cf184dbb2786103bf326fbf029fbafd6add876..4f0a21cbe7d8e33e926d182a6aa88e7b741ea762 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 6b88253698403a3e87872419f16fb096da8c6559..5e4482172743410aeb94d7e518cc9675c428198c 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 7dabe5398d5293a332b7025fb2e6e1cc19738130..229134d6c791211c00349241044a3b4fe5bbc83f 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