From 43f68a8855479244e902ad711cddbf3c5e78510c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 23 Feb 2024 17:34:34 +0100
Subject: [PATCH] update some oracles
---
tests/misc/oracle/pragma-pack.0.res.oracle | 46 +++++++++----------
.../ghost_cv_parsing_errors.2.res.oracle | 2 +-
.../syntax/oracle/ghost_else_bad.2.res.oracle | 2 +-
.../oracle/ghost_parameters.10.res.oracle | 2 +-
.../oracle/ghost_parameters.3.res.oracle | 2 +-
.../oracle/ghost_parameters.4.res.oracle | 2 +-
.../oracle/ghost_parameters.5.res.oracle | 2 +-
.../oracle/ghost_parameters.6.res.oracle | 2 +-
.../oracle/ghost_parameters.7.res.oracle | 2 +-
.../oracle/ghost_parameters.8.res.oracle | 2 +-
.../oracle/ghost_parameters.9.res.oracle | 2 +-
.../oracle/incomplete_struct_field.res.oracle | 12 ++---
12 files changed, 39 insertions(+), 39 deletions(-)
diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle
index 54c851ec770..496ab33d0b3 100644
--- a/tests/misc/oracle/pragma-pack.0.res.oracle
+++ b/tests/misc/oracle/pragma-pack.0.res.oracle
@@ -83,26 +83,26 @@
packing pragma: restoring alignment to default (16)
[kernel:typing:pragma] pragma-pack.c:135:
packing pragma: pushing alignment 16, setting alignment to 4
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:137:
adding aligned(1) attribute to field '__anonstruct_test1_1.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:138:
setting aligned(2) attribute to field '__anonstruct_test1_1.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:139:
adding aligned(4) attribute to field '__anonstruct_test1_1.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:136:
+[kernel:typing:pragma] pragma-pack.c:140:
adding aligned(1) attribute to field '__anonstruct_test1_1.l' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:136:
adding aligned(4) attribute to comp '__anonstruct_test1_1' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:142: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:152:
packing pragma: pushing alignment 16, setting alignment to 1
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:154:
adding aligned(1) attribute to field '__anonstruct_test2_3.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:155:
setting aligned(1) attribute to field '__anonstruct_test2_3.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:156:
adding aligned(1) attribute to field '__anonstruct_test2_3.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:153:
+[kernel:typing:pragma] pragma-pack.c:157:
adding aligned(1) attribute to field '__anonstruct_test2_3.l' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:153:
adding aligned(1) attribute to comp '__anonstruct_test2_3' due to packing pragma
@@ -112,51 +112,51 @@
[kernel:typing:pragma] pragma-pack.c:176: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:186:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:187:
+[kernel:typing:pragma] pragma-pack.c:189:
setting aligned(2) attribute to field '__anonstruct_test4_7.j' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:193: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:203:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:204:
+[kernel:typing:pragma] pragma-pack.c:206:
setting aligned(2) attribute to field '__anonstruct_test5_9.j' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:210: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:220:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:221:
+[kernel:typing:pragma] pragma-pack.c:223:
setting aligned(2) attribute to field '__anonstruct_test6_11.j' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:227: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:237:
packing pragma: pushing alignment 16, setting alignment to 2
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:239:
adding aligned(1) attribute to field '__anonstruct_test7_13.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:240:
setting aligned(2) attribute to field '__anonstruct_test7_13.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:241:
adding aligned(1) attribute to field '__anonstruct_test7_13.q' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:242:
adding aligned(2) attribute to field '__anonstruct_test7_13.p' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:243:
adding aligned(2) attribute to field '__anonstruct_test7_13.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:238:
+[kernel:typing:pragma] pragma-pack.c:244:
adding aligned(1) attribute to field '__anonstruct_test7_13.l' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:238:
adding aligned(2) attribute to comp '__anonstruct_test7_13' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:247:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.i' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:248:
adding aligned(1) attribute to field '__anonstruct_test7_2_14.j' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:249:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.k' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:246:
+[kernel:typing:pragma] pragma-pack.c:250:
adding aligned(2) attribute to field '__anonstruct_test7_2_14.l' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:246:
adding aligned(2) attribute to comp '__anonstruct_test7_2_14' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:252: packing pragma: popped alignment 16
[kernel:typing:pragma] pragma-pack.c:336:
packing pragma: pushing alignment 16, setting alignment to 1
-[kernel:typing:pragma] pragma-pack.c:337:
+[kernel:typing:pragma] pragma-pack.c:338:
adding aligned(1) attribute to field '__anonstruct_barcode_bmp_t_18.len' due to packing pragma
-[kernel:typing:pragma] pragma-pack.c:337:
+[kernel:typing:pragma] pragma-pack.c:339:
adding aligned(1) attribute to field '__anonstruct_barcode_bmp_t_18.data' due to packing pragma
[kernel:typing:pragma] pragma-pack.c:337:
adding aligned(1) attribute to comp '__anonstruct_barcode_bmp_t_18' due to packing pragma
diff --git a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
index 177a24a9845..743cdf3cdb3 100644
--- a/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
+++ b/tests/syntax/oracle/ghost_cv_parsing_errors.2.res.oracle
@@ -5,7 +5,7 @@
24 #ifdef IN_GHOST_ATTR
25
26 int /*@ \ghost */ global ;
- ^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^
27
28 #endif
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_else_bad.2.res.oracle b/tests/syntax/oracle/ghost_else_bad.2.res.oracle
index 6664996b0f9..5bf78d1d17d 100644
--- a/tests/syntax/oracle/ghost_else_bad.2.res.oracle
+++ b/tests/syntax/oracle/ghost_else_bad.2.res.oracle
@@ -5,7 +5,7 @@
47 } /*@ ghost
48 //@ ensures \true ;
49 else {
- ^^^^^^^^^^
+ ^^^^
50 y++ ;
51 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.10.res.oracle b/tests/syntax/oracle/ghost_parameters.10.res.oracle
index 51ba9929f81..4cfa52c3e8e 100644
--- a/tests/syntax/oracle/ghost_parameters.10.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.10.res.oracle
@@ -6,7 +6,7 @@
185 }
186
187 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
188
189 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.3.res.oracle b/tests/syntax/oracle/ghost_parameters.3.res.oracle
index 3d1e0550a28..fbb313828d4 100644
--- a/tests/syntax/oracle/ghost_parameters.3.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.3.res.oracle
@@ -6,7 +6,7 @@
90 }
91
92 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
93
94 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.4.res.oracle b/tests/syntax/oracle/ghost_parameters.4.res.oracle
index 9f9d451cca4..6fc15e643c3 100644
--- a/tests/syntax/oracle/ghost_parameters.4.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.4.res.oracle
@@ -6,7 +6,7 @@
104 }
105
106 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
107
108 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.5.res.oracle b/tests/syntax/oracle/ghost_parameters.5.res.oracle
index 095cbbd26b4..da3a4a8fca7 100644
--- a/tests/syntax/oracle/ghost_parameters.5.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.5.res.oracle
@@ -6,7 +6,7 @@
117 }
118
119 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
120
121 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.6.res.oracle b/tests/syntax/oracle/ghost_parameters.6.res.oracle
index d94f2aee4c8..e94e03ed7c0 100644
--- a/tests/syntax/oracle/ghost_parameters.6.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.6.res.oracle
@@ -6,7 +6,7 @@
131 }
132
133 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
134
135 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.7.res.oracle b/tests/syntax/oracle/ghost_parameters.7.res.oracle
index dae1c5e043d..8185ec1f58c 100644
--- a/tests/syntax/oracle/ghost_parameters.7.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.7.res.oracle
@@ -6,7 +6,7 @@
144 }
145
146 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
147
148 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.8.res.oracle b/tests/syntax/oracle/ghost_parameters.8.res.oracle
index 30443d6f113..c4b8f432947 100644
--- a/tests/syntax/oracle/ghost_parameters.8.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.8.res.oracle
@@ -6,7 +6,7 @@
158 }
159
160 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
161
162 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost_parameters.9.res.oracle b/tests/syntax/oracle/ghost_parameters.9.res.oracle
index ba34ee79c97..a27afa11a3c 100644
--- a/tests/syntax/oracle/ghost_parameters.9.res.oracle
+++ b/tests/syntax/oracle/ghost_parameters.9.res.oracle
@@ -6,7 +6,7 @@
171 }
172
173 void function(int a, int b) /*@ ghost(int c, int d) */ {
- ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+ ^^^^^^^^
174
175 }
[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/incomplete_struct_field.res.oracle b/tests/syntax/oracle/incomplete_struct_field.res.oracle
index f2fe46a7218..75a737c68a9 100644
--- a/tests/syntax/oracle/incomplete_struct_field.res.oracle
+++ b/tests/syntax/oracle/incomplete_struct_field.res.oracle
@@ -1,14 +1,14 @@
[kernel] Parsing incomplete_struct_field.i (no preprocessing)
-[kernel] incomplete_struct_field.i:5: User Error:
+[kernel] incomplete_struct_field.i:7: User Error:
declaration of array of incomplete type 'struct _s`
[kernel] incomplete_struct_field.i:7: User Error:
field `v' is declared with incomplete type struct _s [12]
-[kernel] incomplete_struct_field.i:5: User Error:
- type struct _s is circular
- 3 STDOPT:
- 4 */
+[kernel] incomplete_struct_field.i:7: User Error:
+ field v declaration contains a circular reference to type struct _s
5 typedef struct _s {
- ^^^^^^^^^^^^^^^^^^^
6 int i;
7 struct _s v[12];
+ ^
+ 8 } ts;
+ 9
[kernel] Frama-C aborted: invalid user input.
--
GitLab