Commit 0240a6db authored by Andre Maroneze's avatar Andre Maroneze 💬
Browse files

Merge branch 'fix/syntax/reject-label-end-of-block' into 'master'

small parser fixes

Closes #637

See merge request frama-c/frama-c!2601
parents bb79c595 0f047e66
......@@ -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:
......
......@@ -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 }
......
......@@ -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 ;
}
......
......@@ -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;
......
[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.
......@@ -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:;
}
}
void f() {
/*@ assert \true; */
}
void main() {
{_LOR:} // KO: labels can't be at the end of a block.
}
......@@ -19,5 +19,5 @@ void main () {
if (i == 400)
goto l_end_loop;
}
l_end_loop:
l_end_loop:;
}
......@@ -12,5 +12,5 @@ void main () {
if (i == 400)
goto l_end_loop;
}
l_end_loop:
l_end_loop:;
}
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment