From 5baea9a06124fc0aa2f837b5a8ffb77ca629e997 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 27 Mar 2020 17:40:52 +0100
Subject: [PATCH] [parser] reject label at end of block
---
src/kernel_internals/parsing/cparser.mly | 4 ----
tests/syntax/oracle/wrong_label.res.oracle | 10 ++++++++++
tests/syntax/wrong_label.i | 7 +++++++
3 files changed, 17 insertions(+), 4 deletions(-)
create mode 100644 tests/syntax/oracle/wrong_label.res.oracle
create mode 100644 tests/syntax/wrong_label.i
diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly
index 666053a2830..ff02e392e7f 100644
--- a/src/kernel_internals/parsing/cparser.mly
+++ b/src/kernel_internals/parsing/cparser.mly
@@ -875,10 +875,6 @@ block_element_list:
| annot_list_opt statement block_element_list
{ $1 @ $2 @ $3 }
| annot_list_opt pragma block_element_list { $1 @ $3 }
-/*(* GCC accepts a label at the end of a block *)*/
-| annot_list_opt id_or_typename_as_id COLON
- { let loc = Cil_datatype.Location.of_lexing_loc (Parsing.rhs_start_pos 2, Parsing.rhs_end_pos 3) in
- $1 @ no_ghost [LABEL ($2, no_ghost_stmt (NOP loc), loc)] }
;
annot_list_opt:
diff --git a/tests/syntax/oracle/wrong_label.res.oracle b/tests/syntax/oracle/wrong_label.res.oracle
new file mode 100644
index 00000000000..b95ec14c206
--- /dev/null
+++ b/tests/syntax/oracle/wrong_label.res.oracle
@@ -0,0 +1,10 @@
+[kernel] Parsing tests/syntax/wrong_label.i (no preprocessing)
+[kernel] tests/syntax/wrong_label.i:6:
+ syntax error:
+ Location: line 6, between columns 3 and 8, before or at token: }
+ 4
+ 5 void main() {
+ 6 {_LOR:} // KO: labels can't be at the end of a block.
+ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ 7 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/wrong_label.i b/tests/syntax/wrong_label.i
new file mode 100644
index 00000000000..90e1020b409
--- /dev/null
+++ b/tests/syntax/wrong_label.i
@@ -0,0 +1,7 @@
+void f() {
+ /*@ assert \true; */
+}
+
+void main() {
+ {_LOR:} // KO: labels can't be at the end of a block.
+}
--
GitLab