diff --git a/tests/misc/oracle/pragma-pack.0.res.oracle b/tests/misc/oracle/pragma-pack.0.res.oracle index 54c851ec7707c8feeb46ac865037b0081924c601..496ab33d0b3a9a832384820acac75e32ffa57341 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 177a24a98458ddbea40ce3fb9ce2c855712a12bc..743cdf3cdb3c454aae8cd5bd9ef9bee2ec6d96b1 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 6664996b0f909d093330a7b0984499f8053f65bf..5bf78d1d17d803aff751627e061c065d913c110c 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 51ba9929f8136b5cb1cc74d0c293a6aca4f25e4c..4cfa52c3e8ef347cf27b3eef902756e4d2f5a02f 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 3d1e0550a28df50bbbfdbfe592a846c7fc658a3a..fbb313828d4826ad54d21734248b953f19747e72 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 9f9d451cca4d7a3cb7ba454de014cce162e20a84..6fc15e643c37c4bd05d5d8caa37f168a77748d4e 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 095cbbd26b45e686cc725c04319438085c845161..da3a4a8fca7024415abf47d88324746fed939d09 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 d94f2aee4c876a243e9e5420d33fa3611a921a75..e94e03ed7c012c2ac70e38763d953bd255f253e9 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 dae1c5e043d6ea0136c04c3a735b63efe7690ae2..8185ec1f58cfd27fcb1077ae8c83bb8006ebc7c9 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 30443d6f1138945a5113952ee3796e16f6f18afd..c4b8f43294782b437e6ca7cfee8a7fbd8e5964ec 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 ba34ee79c97c3cfffa2603e84dcea6d13a54b0e3..a27afa11a3c598d28b7450d04aa51672ce10b874 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 f2fe46a7218f4e48596c2a96c4773d15971234f6..75a737c68a9be04685c441563916e714b3d155da 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.