[tests] test for issue #375

8ca0c1b3 · Virgile Prevosto · Andre Maroneze · 9de8b25b · 8ca0c1b3 · 8ca0c1b3
Commit 8ca0c1b3 authored 1 year ago by Virgile Prevosto Committed by Andre Maroneze 1 year ago
--- a/tests/syntax/localisation_error.i
+++ b/tests/syntax/localisation_error.i
+/* run.config*
+EXIT: 1
+STDOPT:
+*/
 int main() {
  int b = 0;
  //@ ghost int a = 2; /*@ assert a == 3; */ /* test */ */

--- a/tests/syntax/oracle/localisation_error.res.oracle
+++ b/tests/syntax/oracle/localisation_error.res.oracle
+[kernel] Parsing localisation_error.i (no preprocessing)
+[kernel] localisation_error.i:7: 
+  syntax error:
+  Location: line 7, between columns 57 and 58, before or at token: /
+  5     int main() {
+  6       int b = 0;
+  7       //@ ghost int a = 2; /*@ assert a == 3; */ /* test */ */
+                                                                 ^
+  8     }
+[kernel] Frama-C aborted: invalid user input.