diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 71cc190bbc9f1e001a4ca8e231d52803b3c01de2..00bc6672df896bea3be51255c917c13a58500cc2 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -9954,13 +9954,14 @@ and doStatement local_env (s : Cabs.statement) : chunk = let res = match e2.expr_node with | Cabs.NOTHING -> (* This means true *) - se1 @@ (loopChunk ~sattr:[Attr("for",[])] ~ghost a (s' @@ (s'', ghost)), ghost) + let c = (s' @@ (s'', ghost)) in + se1 @@ (loopChunk ~sattr:[Attr("for",[])] ~ghost a c, ghost) | _ -> - se1 @@ - (loopChunk ~sattr:[Attr("for",[])] ~ghost a - (((doCondition - local_env CNoConst e2 skipChunk break_cond) - @@ (s', ghost)) @@ (s'', ghost)), ghost) + let c = (s' @@ (s'', ghost)) in + let c = + doCondition local_env CNoConst e2 skipChunk break_cond @@ (c, ghost) + in + se1 @@ (loopChunk ~sattr:[Attr("for",[])] ~ghost a c, ghost) in exitScope (); if has_decl then begin diff --git a/tests/syntax/for_unspecified_seq_in_inc.i b/tests/syntax/for_unspecified_seq_in_inc.i new file mode 100644 index 0000000000000000000000000000000000000000..2b9813d581acd4f9383a5e9a9335990441e7afe4 --- /dev/null +++ b/tests/syntax/for_unspecified_seq_in_inc.i @@ -0,0 +1,17 @@ +extern int f(void); + +int main(void) { + for (; 1; (void)(4 > f())) + continue; + + for (int a; 1; (void)(a > f())) + continue; + + for (; 1; (void)(f() > f())) + continue; + + for (int a; 1; a++) + continue; + + return 0; +} diff --git a/tests/syntax/oracle/for_unspecified_seq_in_inc.res.oracle b/tests/syntax/oracle/for_unspecified_seq_in_inc.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..9393d2f83bf32c6bee1de538399e877c7f59284b --- /dev/null +++ b/tests/syntax/oracle/for_unspecified_seq_in_inc.res.oracle @@ -0,0 +1,44 @@ +[kernel] Parsing tests/syntax/for_unspecified_seq_in_inc.i (no preprocessing) +/* Generated by Frama-C */ +extern int f(void); + +int main(void) +{ + int __retres; + while (1) { + int tmp; + goto __Cont; + __Cont: tmp = f(); + } + { + int a; + while (1) { + int tmp_0; + goto __Cont_0; + __Cont_0: { /* sequence */ + tmp_0 = f(); + ; + } + } + } + while (1) { + int tmp_1; + int tmp_2; + goto __Cont_1; + __Cont_1: { /* sequence */ + tmp_1 = f(); + tmp_2 = f(); + } + } + { + int a_0; + while (1) { + goto __Cont_2; + __Cont_2: a_0 ++; + } + } + __retres = 0; + return __retres; +} + +