Set falls-through loc to the end of the function

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]*)

src/plugins/wp/tests/wp/oracle_qualif/stmtcompiler_test.res.oracle

 # 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: 

tests/cil/oracle/bts297.res.oracle

 [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)

tests/misc/oracle/bts0452.res.oracle

 [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

tests/slicing/oracle/use_spec.0.res.oracle

 [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

tests/slicing/oracle/use_spec.1.res.oracle

 [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

tests/syntax/oracle/exit.res.oracle

 [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"

tests/syntax/oracle/inline_calls.0.res.oracle

 [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)

tests/syntax/oracle/inline_calls.1.res.oracle

 [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)

tests/syntax/oracle/inline_calls.2.res.oracle

 [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)

tests/syntax/oracle/one_ret_assert.res.oracle

 [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;

tests/syntax/oracle/vla_switch.res.oracle

 [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.

tests/value/oracle/imprecise_invalid_write.res.oracle

 [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