Merge branch '1475-failure-when-a-gnu-body-does-not-end-with-a-cabs-computation' into 'master'

Resolve "Failure when a GNU.body does not end with a Cabs.COMPUTATION"

Closes #1475

See merge request frama-c/frama-c!4905

src/kernel_internals/typing/cabs2cil.ml

@@ -7395,6 +7395,11 @@ and doExp local_env
             end
         end
       end
+
+    | Cabs.GNU_BODY _ when !currentFunctionFDEC == dummy_function ->
+      abort_context
+        "statement expression forbidden outside function definition"
+
     | Cabs.GNU_BODY b -> begin
         (* Find the last Cabs.COMPUTATION and remember it. This one is invoked
          * on the reversed list of statements. *)
@@ -7425,7 +7430,7 @@ and doExp local_env
           | _ ->
             try findLastComputation (List.rev b.Cabs.bstmts), false
             with Not_found ->
-              Kernel.fatal ~current:true "Cannot find COMPUTATION in GNU.body"
+              abort_context "void value not ignored as it ought to be"
               (*                Cabs.NOP cabslu, true *)
         in
         let loc = Cabshelper.get_statementloc lastComp in
@@ -7441,7 +7446,9 @@ and doExp local_env
         match !data with
         | None when isvoidbody ->
           finishExp [] se (zero ~loc:e.expr_loc) voidType
-        | None -> abort_context "Cannot find COMPUTATION in GNU.body"
+        | None ->
+          Kernel.fatal ~current:true
+            "statement expression without COMPUTATION, which should be caught by findLastComputation"
         | Some (e, t) ->
           let se, e =
             match se.stmts with

tests/syntax/oracle/wrong_statement_expression.0.res.oracle

+[kernel] Parsing wrong_statement_expression.c (with preprocessing)
+/* Generated by Frama-C */
+void f(int x)
+{
+  return;
+}
+
+

tests/syntax/oracle/wrong_statement_expression.1.res.oracle

+[kernel] Parsing wrong_statement_expression.c (with preprocessing)
+[kernel] wrong_statement_expression.c:19: User Error: 
+  void value not ignored as it ought to be
+  17    #ifdef MISSING_COMPUTATION
+  18    int main(int x){
+  19      x = x + ({;});
+                  ^^^^^
+  20    }
+  21    #endif
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/oracle/wrong_statement_expression.2.res.oracle

+[kernel] Parsing wrong_statement_expression.c (with preprocessing)
+[kernel] wrong_statement_expression.c:14: User Error: 
+  statement expression forbidden outside function definition
+  12    
+  13    #ifdef OUTSIDE_FDEC
+  14      int x = ({ 42; });
+                  ^^^^^^^^^
+  15    #endif
+  16
+[kernel] Frama-C aborted: invalid user input.

tests/syntax/wrong_statement_expression.c

+/* run.config*
+ STDOPT:
+ EXIT: 1
+   STDOPT: #"-cpp-extra-args=-DMISSING_COMPUTATION"
+   STDOPT: #"-cpp-extra-args=-DOUTSIDE_FDEC"
+ */
+
+/* This is expected to work */
+void f(int x){
+  ({;});
+}
+
+#ifdef OUTSIDE_FDEC
+  int x = ({ 42; });
+#endif
+
+#ifdef MISSING_COMPUTATION
+int main(int x){
+  x = x + ({;});
+}
+#endif