diff --git a/src/kernel_internals/parsing/cparser.mly b/src/kernel_internals/parsing/cparser.mly index eaab7b613122613846c138c4f6ed4c2f732fa4fd..73fd674857b387bb4f0fa09b9d93481387805020 100644 --- a/src/kernel_internals/parsing/cparser.mly +++ b/src/kernel_internals/parsing/cparser.mly @@ -882,10 +882,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/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly index 9c25360b415d9900542d993ef3d7bbae21e36639..cc86b0d9c1da06ba1beb012a70be1036e51dfff4 100644 --- a/src/kernel_internals/parsing/logic_parser.mly +++ b/src/kernel_internals/parsing/logic_parser.mly @@ -722,9 +722,12 @@ cv: ; type_spec_cv: - type_spec { $1 } + type_spec cv_after { $2 $1 } | cv type_spec_cv { LTattribute ($2, $1) } -| type_spec_cv cv { LTattribute ($1, $2) } + +cv_after: + /* empty */ { fun t -> t } +| cv cv_after { fun t -> $2 (LTattribute (t,$1)) } cast_logic_type: | type_spec_cv abs_spec_cv_option { $2 $1 } diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c index c65e13840a6b613def9b85585b6a25b8e05c076b..15c916efa382d7875e227e39535ef8d6b8201d4d 100644 --- a/tests/cil/ghost_cfg.c +++ b/tests/cil/ghost_cfg.c @@ -89,7 +89,7 @@ int ghost_goto_ghost(){ //@ ghost goto X ; // reaches return without executing "x = 2" x = 2; - //@ ghost X: + //@ ghost X:; return 0; } @@ -154,7 +154,7 @@ int main(){ int x = 4 ; - //@ ghost X: + //@ ghost X:; x = 2 ; } diff --git a/tests/syntax/ghost_lexing.i b/tests/syntax/ghost_lexing.i index b2a74f89f75ed392eb6f41baf27124a69d4d40e0..03dc066c147e411ec30fa5f0bc87f7aa3c5c4696 100644 --- a/tests/syntax/ghost_lexing.i +++ b/tests/syntax/ghost_lexing.i @@ -16,7 +16,7 @@ void test2(int x) { } void f() { - /*@ ghost L: */ G++; + /*@ ghost L:; */ G++; /*@ assert \at(G,L) + 1 == G; */ L1: /*@ ghost H=G; */ G++; if (G < 30) goto L1; 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/unroll_labels.i b/tests/syntax/unroll_labels.i index 4807505a70050da90d949df89003324420c7c7ff..4ccad645f15c61425fcf07b5c25f80d4d7bc3108 100644 --- a/tests/syntax/unroll_labels.i +++ b/tests/syntax/unroll_labels.i @@ -62,7 +62,7 @@ void main2 () { i += 1; goto foo; i += 1; - foo: + foo:; } } } @@ -76,7 +76,7 @@ void main2_done () { i += 1; goto foo; i += 1; - foo: + foo:; } } } @@ -99,7 +99,7 @@ void main3 (int c) { foo: i += 1; } - up: + up:; } } 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. +} diff --git a/tests/value/loop_array.i b/tests/value/loop_array.i index 9a279023fb65135b0907c6b0b0fbfd10e1ca3cb1..5d644af2bb682ddbfae9659eb35fc5f6e00b38e2 100644 --- a/tests/value/loop_array.i +++ b/tests/value/loop_array.i @@ -19,5 +19,5 @@ void main () { if (i == 400) goto l_end_loop; } - l_end_loop: + l_end_loop:; } diff --git a/tests/value/loop_join.i b/tests/value/loop_join.i index 2abaeb65fcccff5c539622d0d9c12c7e5d30b087..19bcb4fc323b60b14d555336a8235f0124170db8 100644 --- a/tests/value/loop_join.i +++ b/tests/value/loop_join.i @@ -12,5 +12,5 @@ void main () { if (i == 400) goto l_end_loop; } - l_end_loop: + l_end_loop:; }