diff --git a/tests/syntax/ghost-else-bad-oneline.i b/tests/syntax/ghost-else-bad-oneline.i
new file mode 100644
index 0000000000000000000000000000000000000000..990b2e21ea623e3b62852f3d58750d550691d74d
--- /dev/null
+++ b/tests/syntax/ghost-else-bad-oneline.i
@@ -0,0 +1,10 @@
+/* run.config
+ OPT: -no-autoload-plugins -print
+*/
+
+void if_ghost_else_one_line_bad(int x, int y) {
+ if (x) {
+ x++;
+ } //@ ghost else
+ y++;
+}
\ No newline at end of file
diff --git a/tests/syntax/ghost-else-bad.c b/tests/syntax/ghost-else-bad.c
new file mode 100644
index 0000000000000000000000000000000000000000..8f6bf609bffa284e52b5d0c3a89622b3d47c568a
--- /dev/null
+++ b/tests/syntax/ghost-else-bad.c
@@ -0,0 +1,55 @@
+/* run.config
+ OPT: -no-autoload-plugins -cpp-extra-args="-DERROR_LOC_WITH_COMMENTS"
+ OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print
+ OPT: -no-autoload-plugins -cpp-extra-args="-DBAD_ANNOT_POSITION"
+*/
+
+
+#ifdef ERROR_LOC_WITH_COMMENTS // Must check that the line indicated for undeclared "z" is correct
+
+void if_ghost_else_block_comments_then_error(int x, int y) {
+ if (x) {
+ x++;
+ } /*@ ghost
+ // comment 1
+ // comment 2
+ else {
+ y ++ ;
+ } */
+
+ z = 42;
+}
+
+#endif
+
+#ifdef ALREADY_HAS_ELSE
+// Must warn that the ghost else cannot appear since there is already a else
+// Thus the ghost else is ignored and the resulting code does not comprise it
+
+void if_ghost_else_block_bad(int x, int y) {
+ if (x) {
+ x++;
+ } /*@ ghost else {
+ y ++ ;
+ } */
+ else {
+ y = 42;
+ }
+}
+
+#endif
+
+#ifdef BAD_ANNOT_POSITION // Syntax error because of the bad position of the annotation
+
+void test(int x, int y){
+ if(x){
+ x++ ;
+ } /*@ ghost
+ //@ ensures \true ;
+ else {
+ y++ ;
+ }
+ */
+}
+
+#endif
\ No newline at end of file
diff --git a/tests/syntax/ghost-else.c b/tests/syntax/ghost-else.c
deleted file mode 100644
index 0fc9a2a715d3b72bdd673d5c4cfc3f2fafbafdf6..0000000000000000000000000000000000000000
--- a/tests/syntax/ghost-else.c
+++ /dev/null
@@ -1,140 +0,0 @@
-/* run.config
- OPT: -no-autoload-plugins -print
- OPT: -cpp-extra-args="-DERROR_LOC_WITH_COMMENTS"
- OPT: -cpp-extra-args="-DALREADY_HAS_ELSE" -print
- OPT: -cpp-extra-args="-DBAD_ANNOT_POSITION"
- OPT: -cpp-extra-args="-DBAD_ONELINE_GHOST_ELSE"
-*/
-
-void normal_only_if(int x, int y) {
- if (x) {
- x++;
- }
-}
-
-void normal_if_else(int x, int y) {
- if (x) {
- x++;
- } else {
- y++;
- }
-}
-
-void normal_if_else_intricated(int x, int y) {
- if (x)
- if (y)
- y++;
- else
- x++;
-}
-
-void if_ghost_else_one_line(int x, int y) {
- if (x) {
- x++;
- } //@ ghost else y ++ ;
-}
-
-void if_ghost_else_block(int x, int y) {
- if (x) {
- x++;
- } /*@ ghost else {
- y ++ ;
- } */
-}
-
-void if_ghost_else_multi_line_block(int x, int y) {
- if (x) {
- x++;
- } /*@ ghost else {
- y ++ ;
- y += x;
- -- y ;
- } */
-}
-
-void if_ghost_else_block_comments(int x, int y) {
- if (x) {
- x++;
- } /*@ ghost
- // comment 1
- // comment 2
- else {
- y ++ ;
- } */
-}
-
-void normal_if_ghost_else_intricated(int x, int y) {
- if (x)
- if (x)
- x++;
- //@ ghost else y++;
-}
-
-void ghost_else_plus_else_association(int x, int y){
- // we must take care to keep the "if" bloc when pretty-printing
- // as removing the brackets changes the program.
- if (x){
- if (x) x++ ;
- //@ ghost else y-- ;
- } else x ++ ;
-}
-
-#ifdef ERROR_LOC_WITH_COMMENTS // Must check that the line indicated for undeclared "z" is correct
-
-void if_ghost_else_block_comments_then_error(int x, int y) {
- if (x) {
- x++;
- } /*@ ghost
- // comment 1
- // comment 2
- else {
- y ++ ;
- } */
-
- z = 42;
-}
-
-#endif
-
-#ifdef ALREADY_HAS_ELSE
-// Must warn that the ghost else cannot appear since there is already a else
-// Thus the ghost else is ignored and the resulting code does not comprise it
-
-void if_ghost_else_block_bad(int x, int y) {
- if (x) {
- x++;
- } /*@ ghost else {
- y ++ ;
- } */
- else {
- y = 42;
- }
-}
-
-#endif
-
-#ifdef BAD_ANNOT_POSITION // Syntax error because of the bad position of the annotation
-
-void test(int x, int y){
- if(x){
- x++ ;
- } /*@ ghost
- //@ ensures \true ;
- else {
- y++ ;
- }
- */
-}
-
-#endif
-
-#ifdef BAD_ONELINE_GHOST_ELSE // Syntax error because of unterminated ghost one liner
-
-void if_ghost_else_one_line_bad(int x, int y) {
- if (x) {
- x++;
- } //@ ghost else
- y++;
-}
-
-#endif
diff --git a/tests/syntax/ghost-else.i b/tests/syntax/ghost-else.i
new file mode 100644
index 0000000000000000000000000000000000000000..edca2ad9cc813eac29b41dc50c94269ee954de0a
--- /dev/null
+++ b/tests/syntax/ghost-else.i
@@ -0,0 +1,76 @@
+/* run.config
+ OPT: -no-autoload-plugins -print
+*/
+
+void normal_only_if(int x, int y) {
+ if (x) {
+ x++;
+ }
+}
+
+void normal_if_else(int x, int y) {
+ if (x) {
+ x++;
+ } else {
+ y++;
+ }
+}
+
+void normal_if_else_intricated(int x, int y) {
+ if (x)
+ if (y)
+ y++;
+ else
+ x++;
+}
+
+void if_ghost_else_one_line(int x, int y) {
+ if (x) {
+ x++;
+ } //@ ghost else y ++ ;
+}
+
+void if_ghost_else_block(int x, int y) {
+ if (x) {
+ x++;
+ } /*@ ghost else {
+ y ++ ;
+ } */
+}
+
+void if_ghost_else_multi_line_block(int x, int y) {
+ if (x) {
+ x++;
+ } /*@ ghost else {
+ y ++ ;
+ y += x;
+ -- y ;
+ } */
+}
+
+void if_ghost_else_block_comments(int x, int y) {
+ if (x) {
+ x++;
+ } /*@ ghost
+ // comment 1
+ // comment 2
+ else {
+ y ++ ;
+ } */
+}
+
+void normal_if_ghost_else_intricated(int x, int y) {
+ if (x)
+ if (x)
+ x++;
+ //@ ghost else y++;
+}
+
+void ghost_else_plus_else_association(int x, int y){
+ // we must take care to keep the "if" bloc when pretty-printing
+ // as removing the brackets changes the program.
+ if (x){
+ if (x) x++ ;
+ //@ ghost else y-- ;
+ } else x ++ ;
+}
\ No newline at end of file
diff --git a/tests/syntax/oracle/ghost-else-bad-oneline.res.oracle b/tests/syntax/oracle/ghost-else-bad-oneline.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..df16567ef5ded917da8a68560edf2039e5a26e4e
--- /dev/null
+++ b/tests/syntax/oracle/ghost-else-bad-oneline.res.oracle
@@ -0,0 +1,15 @@
+[kernel] Parsing tests/syntax/ghost-else-bad-oneline.i (no preprocessing)
+[kernel] tests/syntax/ghost-else-bad-oneline.i:6:
+ syntax error:
+ Location: between lines 6 and 8, before or at token:
+
+ 4
+ 5 void if_ghost_else_one_line_bad(int x, int y) {
+
+ 6 if (x) {
+ 7 x++;
+ 8 } //@ ghost else
+
+ 9 y++;
+ 10 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost-else-bad.0.res.oracle b/tests/syntax/oracle/ghost-else-bad.0.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..73aca960de292814921ff41c2a63223640c56362
--- /dev/null
+++ b/tests/syntax/oracle/ghost-else-bad.0.res.oracle
@@ -0,0 +1,5 @@
+[kernel] Parsing tests/syntax/ghost-else-bad.c (with preprocessing)
+[kernel] tests/syntax/ghost-else-bad.c:20: Failure: Cannot resolve variable z
+[kernel] User Error: stopping on file "tests/syntax/ghost-else-bad.c" that has errors. Add
+ '-kernel-msg-key pp' for preprocessing command.
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost-else-bad.1.err.oracle b/tests/syntax/oracle/ghost-else-bad.1.err.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..a462608f4fbd5cf7c65dbe989be079cd1601e57d
--- /dev/null
+++ b/tests/syntax/oracle/ghost-else-bad.1.err.oracle
@@ -0,0 +1 @@
+Warning: tests/syntax/ghost-else-bad.c:32: Invalid ghost else ignored
diff --git a/tests/syntax/oracle/ghost-else-bad.1.res.oracle b/tests/syntax/oracle/ghost-else-bad.1.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3a7ccc5655e32894b3939a956c80dbf011fe7e3e
--- /dev/null
+++ b/tests/syntax/oracle/ghost-else-bad.1.res.oracle
@@ -0,0 +1,9 @@
+[kernel] Parsing tests/syntax/ghost-else-bad.c (with preprocessing)
+/* Generated by Frama-C */
+void if_ghost_else_block_bad(int x, int y)
+{
+ if (x) x ++; else y = 42;
+ return;
+}
+
+
diff --git a/tests/syntax/oracle/ghost-else-bad.2.res.oracle b/tests/syntax/oracle/ghost-else-bad.2.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..0fb6dc879ca32d041f42d358de3964d59a30769d
--- /dev/null
+++ b/tests/syntax/oracle/ghost-else-bad.2.res.oracle
@@ -0,0 +1,14 @@
+[kernel] Parsing tests/syntax/ghost-else-bad.c (with preprocessing)
+[kernel] tests/syntax/ghost-else-bad.c:47:
+ syntax error:
+ Location: between lines 47 and 49, before or at token: else
+ 45 if(x){
+ 46 x++ ;
+
+ 47 } /*@ ghost
+ 48 //@ ensures \true ;
+ 49 else {
+
+ 50 y++ ;
+ 51 }
+[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost-else.1.res.oracle b/tests/syntax/oracle/ghost-else.1.res.oracle
deleted file mode 100644
index 9b7e8807048ecf36a3741d5eb9cb7c1d83616d26..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/ghost-else.1.res.oracle
+++ /dev/null
@@ -1,5 +0,0 @@
-[kernel] Parsing tests/syntax/ghost-else.c (with preprocessing)
-[kernel] tests/syntax/ghost-else.c:94: Failure: Cannot resolve variable z
-[kernel] User Error: stopping on file "tests/syntax/ghost-else.c" that has errors. Add
- '-kernel-msg-key pp' for preprocessing command.
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost-else.2.err.oracle b/tests/syntax/oracle/ghost-else.2.err.oracle
deleted file mode 100644
index bba7ee84ac82145570f2afcfda2984420f0495ca..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/ghost-else.2.err.oracle
+++ /dev/null
@@ -1 +0,0 @@
-Warning: tests/syntax/ghost-else.c:106: Invalid ghost else ignored
diff --git a/tests/syntax/oracle/ghost-else.2.res.oracle b/tests/syntax/oracle/ghost-else.2.res.oracle
deleted file mode 100644
index c0f7e60325f2056efc5e5cacf8cfbe32e908724c..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/ghost-else.2.res.oracle
+++ /dev/null
@@ -1,78 +0,0 @@
-[kernel] Parsing tests/syntax/ghost-else.c (with preprocessing)
-/* Generated by Frama-C */
-void normal_only_if(int x, int y)
-{
- if (x) x ++;
- return;
-}
-
-void normal_if_else(int x, int y)
-{
- if (x) x ++; else y ++;
- return;
-}
-
-void normal_if_else_intricated(int x, int y)
-{
- if (x)
- if (y) y ++; else x ++;
- return;
-}
-
-void if_ghost_else_one_line(int x, int y)
-{
- if (x) x ++;
- /*@ ghost else y ++;*/
- return;
-}
-
-void if_ghost_else_block(int x, int y)
-{
- if (x) x ++;
- /*@ ghost else y ++;*/
- return;
-}
-
-void if_ghost_else_multi_line_block(int x, int y)
-{
- if (x) x ++;
- /*@ ghost else {
- y ++;
- y += x;
- y --;
- }*/
- return;
-}
-
-void if_ghost_else_block_comments(int x, int y)
-{
- if (x) x ++;
- /*@ ghost else y ++;*/
- return;
-}
-
-void normal_if_ghost_else_intricated(int x, int y)
-{
- if (x)
- if (x) x ++;
- /*@ ghost else y ++;*/
- return;
-}
-
-void ghost_else_plus_else_association(int x, int y)
-{
- if (x) {
- if (x) x ++;
- /*@ ghost else y --;*/
- }
- else x ++;
- return;
-}
-
-void if_ghost_else_block_bad(int x, int y)
-{
- if (x) x ++; else y = 42;
- return;
-}
-
-
diff --git a/tests/syntax/oracle/ghost-else.3.res.oracle b/tests/syntax/oracle/ghost-else.3.res.oracle
deleted file mode 100644
index ef0d0730513f8360f091d21d94553497250ecf82..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/ghost-else.3.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-[kernel] Parsing tests/syntax/ghost-else.c (with preprocessing)
-[kernel] tests/syntax/ghost-else.c:121:
- syntax error:
- Location: between lines 121 and 123, before or at token: else
- 119 if(x){
- 120 x++ ;
-
- 121 } /*@ ghost
- 122 //@ ensures \true ;
- 123 else {
-
- 124 y++ ;
- 125 }
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost-else.4.res.oracle b/tests/syntax/oracle/ghost-else.4.res.oracle
deleted file mode 100644
index fbc63424f9150f2d7dfedbacdc386c3e4b0b683c..0000000000000000000000000000000000000000
--- a/tests/syntax/oracle/ghost-else.4.res.oracle
+++ /dev/null
@@ -1,14 +0,0 @@
-[kernel] Parsing tests/syntax/ghost-else.c (with preprocessing)
-[kernel] tests/syntax/ghost-else.c:134:
- syntax error:
- Location: between lines 134 and 136, before or at token: /
- 132
- 133 void if_ghost_else_one_line_bad(int x, int y) {
-
- 134 if (x) {
- 135 x++;
- 136 } //@ ghost else
-
- 137 y++;
- 138 }
-[kernel] Frama-C aborted: invalid user input.
diff --git a/tests/syntax/oracle/ghost-else.0.res.oracle b/tests/syntax/oracle/ghost-else.res.oracle
similarity index 93%
rename from tests/syntax/oracle/ghost-else.0.res.oracle
rename to tests/syntax/oracle/ghost-else.res.oracle
index b25cd9760cc34e1bdee1366bf7085d6e043f2346..7d21709e861dc709563ac2b47c6e02497ddbb524 100644
--- a/tests/syntax/oracle/ghost-else.0.res.oracle
+++ b/tests/syntax/oracle/ghost-else.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/syntax/ghost-else.c (with preprocessing)
+[kernel] Parsing tests/syntax/ghost-else.i (no preprocessing)
/* Generated by Frama-C */
void normal_only_if(int x, int y)
{