From 4c4123a3878c49610a6faa7c83f3e5f3e1a319a0 Mon Sep 17 00:00:00 2001
From: Benjamin Jorge <benjamin.jorge@cea.fr>
Date: Tue, 28 Jan 2025 16:59:03 +0100
Subject: [PATCH] [cabs2cil] better handling of statement expressions
---
src/kernel_internals/typing/cabs2cil.ml | 11 ++++++++--
.../wrong_statement_expression.0.res.oracle | 8 +++++++
.../wrong_statement_expression.1.res.oracle | 10 +++++++++
.../wrong_statement_expression.2.res.oracle | 10 +++++++++
tests/syntax/wrong_statement_expression.c | 21 +++++++++++++++++++
5 files changed, 58 insertions(+), 2 deletions(-)
create mode 100644 tests/syntax/oracle/wrong_statement_expression.0.res.oracle
create mode 100644 tests/syntax/oracle/wrong_statement_expression.1.res.oracle
create mode 100644 tests/syntax/oracle/wrong_statement_expression.2.res.oracle
create mode 100644 tests/syntax/wrong_statement_expression.c
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index e3fd461d5c..26d178cbb6 100644
--- a/src/kernel_internals/typing/cabs2cil.ml
+++ b/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
diff --git a/tests/syntax/oracle/wrong_statement_expression.0.res.oracle b/tests/syntax/oracle/wrong_statement_expression.0.res.oracle
new file mode 100644
index 0000000000..039049cc6a
--- /dev/null
+++ b/tests/syntax/oracle/wrong_statement_expression.0.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing wrong_statement_expression.c (with preprocessing)
+/* Generated by Frama-C */
+void f(int x)
+{
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/wrong_statement_expression.1.res.oracle b/tests/syntax/oracle/wrong_statement_expression.1.res.oracle
new file mode 100644
index 0000000000..990d7169eb
--- /dev/null
+++ b/tests/syntax/oracle/wrong_statement_expression.1.res.oracle
@@ -0,0 +1,10 @@
+[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.
diff --git a/tests/syntax/oracle/wrong_statement_expression.2.res.oracle b/tests/syntax/oracle/wrong_statement_expression.2.res.oracle
new file mode 100644
index 0000000000..b998294b68
--- /dev/null
+++ b/tests/syntax/oracle/wrong_statement_expression.2.res.oracle
@@ -0,0 +1,10 @@
+[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.
diff --git a/tests/syntax/wrong_statement_expression.c b/tests/syntax/wrong_statement_expression.c
new file mode 100644
index 0000000000..ddd33cf763
--- /dev/null
+++ b/tests/syntax/wrong_statement_expression.c
@@ -0,0 +1,21 @@
+/* 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
--
GitLab