diff --git a/tests/syntax/error_end_decl.i b/tests/syntax/error_end_decl.i new file mode 100644 index 0000000000000000000000000000000000000000..8fba5808d557f51da3eabbd664511175c1405fdd --- /dev/null +++ b/tests/syntax/error_end_decl.i @@ -0,0 +1,13 @@ +/* run.config +EXIT: 1 +STDOPT: +*/ + +/*@ assigns *p \from \nothing; */ +void f(char *p) + +/*@ + assigns \result \from \nothing; + ensures \result == 0; +*/ +char g(char *p); diff --git a/tests/syntax/oracle/error_end_decl.res.oracle b/tests/syntax/oracle/error_end_decl.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391 diff --git a/tests/syntax/oracle/static_assert_wrong.res.oracle b/tests/syntax/oracle/static_assert_wrong.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..d2e83bab9e6ee0bdc2ab1f40b164d1f5e2617354 --- /dev/null +++ b/tests/syntax/oracle/static_assert_wrong.res.oracle @@ -0,0 +1,9 @@ +[kernel] Parsing static_assert_wrong.i (no preprocessing) +[kernel] static_assert_wrong.i:8: + syntax error: + Location: line 8, between columns 0 and 3, before or at token: int + 6 _Static_assert(1,"assert succeeds") + 7 + 8 int x = 0; + ^^^ +[kernel] Frama-C aborted: invalid user input. diff --git a/tests/syntax/static_assert_wrong.i b/tests/syntax/static_assert_wrong.i new file mode 100644 index 0000000000000000000000000000000000000000..fd27a5c70f7046819343f242140208e72f0692a8 --- /dev/null +++ b/tests/syntax/static_assert_wrong.i @@ -0,0 +1,8 @@ +/* run.config* + EXIT: 1 + STDOPT: +*/ + +_Static_assert(1,"assert succeeds") + +int x = 0;