From f39d80372a3de213542d2d0a8b9f82d3f812343b Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Thu, 9 Sep 2021 15:31:35 +0200
Subject: [PATCH] [kernel] prevent label removal in for continue - continues
label was dropped when placed on an unspecified sequence associated to the
increment part of a for loop
---
src/kernel_internals/typing/cabs2cil.ml | 13 +++---
tests/syntax/for_unspecified_seq_in_inc.i | 17 +++++++
.../for_unspecified_seq_in_inc.res.oracle | 44 +++++++++++++++++++
3 files changed, 68 insertions(+), 6 deletions(-)
create mode 100644 tests/syntax/for_unspecified_seq_in_inc.i
create mode 100644 tests/syntax/oracle/for_unspecified_seq_in_inc.res.oracle
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index 71cc190bbc9..00bc6672df8 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 00000000000..2b9813d581a
--- /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 00000000000..9393d2f83bf
--- /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;
+}
+
+
--
GitLab