diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index 666053a2830b8b449ef19dc859732f997842f7bc..ff02e392e7f225814783f4b13bae33b1c1ec1801 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 0000000000000000000000000000000000000000..b95ec14c2063a28ceb6331afc1d8f28408e29c3e --- /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 0000000000000000000000000000000000000000..90e1020b409d79ace1a1904892f8cba0dee9e883 --- /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. +}