From 36939fbd9d88bc5ba97e486669b03550700f5980 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Mon, 22 Mar 2021 15:55:13 +0100
Subject: [PATCH] [Tests] adds EXIT directives into test files
---
.../tests/ya/metavariables-incompatible.i | 3 +-
.../aorai/tests/ya/metavariables-wrong.i | 2 +-
.../aorai/tests/ya/singleassignment-wrong.i | 2 +-
src/plugins/report/tests/report/classify.c | 1 +
src/plugins/server/tests/batch/ast_services.i | 6 +++
src/plugins/server/tests/batch/wrong.i | 4 ++
.../variadic/tests/erroneous/no-param.i | 5 ++-
.../variadic/tests/erroneous/not-enough-par.i | 4 ++
.../tests/erroneous/variadic-builtin.i | 4 ++
.../wp/tests/wp_plugin/unsafe-arrays.i | 10 ++---
src/plugins/wp/tests/wp_usage/issue-189.i | 4 +-
tests/builtins/watch.c | 5 +++
tests/cil/acsl-comments.i | 5 +++
tests/cil/bts892.i | 6 +++
tests/cil/ghost_cfg.c | 1 +
tests/metrics/locals_size.i | 2 +-
tests/misc/bts0451.i | 1 +
tests/misc/bts0990_link.i | 4 +-
tests/misc/custom_machdep.c | 9 ++--
tests/misc/debug_category.i | 43 +++++++++++--------
tests/misc/filepath.i | 3 +-
tests/misc/function_ptr_alignof.i | 5 ++-
tests/misc/function_ptr_lvalue_1.i | 6 +++
tests/misc/function_ptr_lvalue_2.i | 5 +++
tests/misc/function_ptr_sizeof.i | 5 ++-
tests/misc/global_decl_loc2.i | 4 +-
tests/misc/log_selfrec.i | 4 +-
tests/misc/widen_hints.c | 2 +
tests/spec/multiple_include_2.c | 3 ++
tests/syntax/alloc_order.i | 5 +++
tests/syntax/arg_type.i | 6 +--
tests/syntax/array_cast_bts1099.i | 5 +++
tests/syntax/array_size.i | 6 +++
tests/syntax/axiomatic_nested.i | 4 ++
tests/syntax/bad_return_bts_599.i | 5 ++-
tests/syntax/bts0519.c | 1 +
tests/syntax/cert-dcl-36.c | 5 +++
tests/syntax/cert_msc_38.c | 17 ++++----
tests/syntax/composite-tags.i | 5 +++
tests/syntax/const-assignments.c | 6 +--
tests/syntax/duplicate_field.i | 5 +++
tests/syntax/fam.i | 6 +++
tests/syntax/flexible_array_member_invalid1.i | 5 +++
tests/syntax/flexible_array_member_invalid2.i | 5 +++
tests/syntax/flexible_array_member_invalid3.i | 6 +++
tests/syntax/flexible_array_member_invalid4.i | 5 +++
tests/syntax/flexible_array_member_invalid5.i | 6 +++
tests/syntax/ghost_cv_incompat.i | 5 +++
tests/syntax/ghost_cv_invalid_use.i | 4 ++
tests/syntax/ghost_cv_parsing_errors.c | 1 +
tests/syntax/ghost_cv_var_decl.c | 3 ++
tests/syntax/ghost_else_bad.c | 6 +--
tests/syntax/ghost_else_bad_oneline.i | 2 +-
tests/syntax/ghost_local_ill_formed.i | 4 ++
tests/syntax/ghost_multiline_annot.c | 6 +--
tests/syntax/ghost_parameters.c | 3 ++
tests/syntax/incompatible_qualifiers.c | 8 ++--
tests/syntax/incomplete_array.i | 4 ++
tests/syntax/incomplete_struct_field.i | 4 ++
tests/syntax/inconsistent_decl.c | 5 ++-
tests/syntax/inconsistent_global_ghost_spec.c | 10 ++---
tests/syntax/init_bts1352.i | 6 +++
tests/syntax/invalid_constant.i | 4 ++
tests/syntax/line_number.c | 5 +++
tests/syntax/lvalvoid.i | 4 ++
tests/syntax/merge_attrs_align.c | 3 ++
tests/syntax/merge_unused.c | 7 +--
tests/syntax/multiple_assigns.i | 4 ++
tests/syntax/multiple_froms.i | 6 +++
tests/syntax/mutually_recursive_struct.i | 5 +++
tests/syntax/no_prototype.i | 5 +++
.../syntax/reject_use_decl_mismatch_bts728.c | 6 +--
tests/syntax/rettype.i | 4 ++
tests/syntax/sizeof_incomplete_type.c | 5 +++
tests/syntax/spurious_brace_bts_1273.i | 5 +++
.../struct_with_function_field_invalid.i | 5 +++
tests/syntax/syntactic_hook.i | 3 ++
tests/syntax/type_branch_bts_1081.i | 5 +++
tests/syntax/type_redef.i | 2 +-
tests/syntax/typedef_namespace_bts1500.c | 9 ++--
tests/syntax/va.c | 5 +++
tests/syntax/vla_goto.i | 6 +++
tests/syntax/vla_goto3.i | 4 ++
tests/syntax/vla_goto_same_block_below.i | 5 +++
tests/syntax/vla_switch.i | 5 +++
tests/syntax/void_parameter.i | 7 ++-
tests/syntax/wrong-assignment.i | 6 +++
tests/syntax/wrong_label.i | 5 +++
tests/value/array_zero_length.i | 1 +
tests/value/empty_base.c | 1 +
tests/value/recursion.i | 3 +-
tests/value/split_return.i | 3 ++
tests/value/unknown_sizeof.i | 2 +-
tests/value/use_spec.i | 6 +--
tests/value/va_list.c | 7 +--
95 files changed, 388 insertions(+), 97 deletions(-)
diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
index a32cefe9e95..ac025ee3032 100644
--- a/src/plugins/aorai/tests/ya/metavariables-incompatible.i
+++ b/src/plugins/aorai/tests/ya/metavariables-incompatible.i
@@ -1,6 +1,5 @@
/* run.config*
+ EXIT: 1
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
-
void main(void) {}
-
diff --git a/src/plugins/aorai/tests/ya/metavariables-wrong.i b/src/plugins/aorai/tests/ya/metavariables-wrong.i
index a0542d20021..febfd16cb34 100644
--- a/src/plugins/aorai/tests/ya/metavariables-wrong.i
+++ b/src/plugins/aorai/tests/ya/metavariables-wrong.i
@@ -1,7 +1,7 @@
/* run.config*
+ EXIT: 1
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
-
void f(int x) {}
void g(void) {}
void h(void) {}
diff --git a/src/plugins/aorai/tests/ya/singleassignment-wrong.i b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
index 4a88230c1c7..baa7b42e03e 100644
--- a/src/plugins/aorai/tests/ya/singleassignment-wrong.i
+++ b/src/plugins/aorai/tests/ya/singleassignment-wrong.i
@@ -1,7 +1,7 @@
/* run.config*
+ EXIT: 1
OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
-
int main(int x)
{
return x;
diff --git a/src/plugins/report/tests/report/classify.c b/src/plugins/report/tests/report/classify.c
index 3ee8df0b80a..59d10572d66 100644
--- a/src/plugins/report/tests/report/classify.c
+++ b/src/plugins/report/tests/report/classify.c
@@ -2,6 +2,7 @@
CMD: @frama-c@ -kernel-warn-key=annot-error=active -no-autoload-plugins -load-module wp,report -report-output @PTEST_RESULT@/classified.@PTEST_NUMBER@.json -wp -wp-msg-key shell
LOG: classified.@PTEST_NUMBER@.json
OPT: -wp-prover qed -report-unclassified-untried REVIEW -then -report-classify
+EXIT: 1
LOG: classified.@PTEST_NUMBER@.json
OPT: -wp-prover qed -report-unclassified-warning ERROR -then -report-classify
LOG: classified.@PTEST_NUMBER@.json
diff --git a/src/plugins/server/tests/batch/ast_services.i b/src/plugins/server/tests/batch/ast_services.i
index 975369e8966..4c1e7b1b838 100644
--- a/src/plugins/server/tests/batch/ast_services.i
+++ b/src/plugins/server/tests/batch/ast_services.i
@@ -1,2 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
int f(int x) { return x++; }
int g(int y) { return y++; }
diff --git a/src/plugins/server/tests/batch/wrong.i b/src/plugins/server/tests/batch/wrong.i
index e69de29bb2d..1a0a6550cd2 100644
--- a/src/plugins/server/tests/batch/wrong.i
+++ b/src/plugins/server/tests/batch/wrong.i
@@ -0,0 +1,4 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
diff --git a/src/plugins/variadic/tests/erroneous/no-param.i b/src/plugins/variadic/tests/erroneous/no-param.i
index ae11c2ab9c3..d91685eee5b 100644
--- a/src/plugins/variadic/tests/erroneous/no-param.i
+++ b/src/plugins/variadic/tests/erroneous/no-param.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
void f(...) // f must have at least one argument
{
return;
@@ -7,4 +11,3 @@ int main()
{
f(0);
}
-
diff --git a/src/plugins/variadic/tests/erroneous/not-enough-par.i b/src/plugins/variadic/tests/erroneous/not-enough-par.i
index cd27daffa38..324731fc341 100644
--- a/src/plugins/variadic/tests/erroneous/not-enough-par.i
+++ b/src/plugins/variadic/tests/erroneous/not-enough-par.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
int f(int a, int, int c,...);
int main(){
diff --git a/src/plugins/variadic/tests/erroneous/variadic-builtin.i b/src/plugins/variadic/tests/erroneous/variadic-builtin.i
index 26a22e680ed..160fba1f823 100644
--- a/src/plugins/variadic/tests/erroneous/variadic-builtin.i
+++ b/src/plugins/variadic/tests/erroneous/variadic-builtin.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 3
+ STDOPT:
+*/
extern void Frama_C_show_each_warning(char const * , ...);
void main(void)
diff --git a/src/plugins/wp/tests/wp_plugin/unsafe-arrays.i b/src/plugins/wp/tests/wp_plugin/unsafe-arrays.i
index 23dd4015e0a..3d6a5d4db64 100644
--- a/src/plugins/wp/tests/wp_plugin/unsafe-arrays.i
+++ b/src/plugins/wp/tests/wp_plugin/unsafe-arrays.i
@@ -1,15 +1,15 @@
/* run.config
OPT: -safe-arrays
+ EXIT: 1
OPT: -unsafe-arrays
*/
struct { int f[10]; } s,*p;
int a[10];
-/*@
- requires \valid(p);
- ensures ARRAYS: \valid(&a[..]);
- ensures STRUCT: \valid(&s.f[..]);
- ensures INDIRP: \valid(&p->f[..]);
+/*@ requires \valid(p);
+ ensures ARRAYS: \valid(&a[..]);
+ ensures STRUCT: \valid(&s.f[..]);
+ ensures INDIRP: \valid(&p->f[..]);
*/
void f(void) { }
diff --git a/src/plugins/wp/tests/wp_usage/issue-189.i b/src/plugins/wp/tests/wp_usage/issue-189.i
index 9309a4ad71c..a524540296f 100644
--- a/src/plugins/wp/tests/wp_usage/issue-189.i
+++ b/src/plugins/wp/tests/wp_usage/issue-189.i
@@ -1,13 +1,13 @@
/* run.config
OPT:
+ EXIT: 1
OPT: -wp-msg-key refusage -wp-model Caveat
+ EXIT: 0
OPT: -wp-msg-key refusage -wp-model Caveat -wp-unalias-vars src
*/
-
/* run.config_qualif
DONTRUN:
*/
-
/*@ requires v1: \valid( ptr );
@ requires v2: \valid_read( src + idx );
@ requires s1: \separated( ptr, src + idx );
diff --git a/tests/builtins/watch.c b/tests/builtins/watch.c
index 49a56689008..80551c78222 100644
--- a/tests/builtins/watch.c
+++ b/tests/builtins/watch.c
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
int x,y,z;
int main(int c){
diff --git a/tests/cil/acsl-comments.i b/tests/cil/acsl-comments.i
index bf3c37795c3..8b92eb451c8 100644
--- a/tests/cil/acsl-comments.i
+++ b/tests/cil/acsl-comments.i
@@ -1,2 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
/*@ ensures /* FOO */ \false; */
void job(void) { }
diff --git a/tests/cil/bts892.i b/tests/cil/bts892.i
index 6da1b3de795..a4a656fc9af 100644
--- a/tests/cil/bts892.i
+++ b/tests/cil/bts892.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
int tab[16];
void* main(void)
diff --git a/tests/cil/ghost_cfg.c b/tests/cil/ghost_cfg.c
index 15c916efa38..13b1504560e 100644
--- a/tests/cil/ghost_cfg.c
+++ b/tests/cil/ghost_cfg.c
@@ -1,4 +1,5 @@
/* run.config
+ EXIT: 1
OPT:-no-autoload-plugins -cpp-extra-args="-DCAN_CHECK"
OPT:-no-autoload-plugins -cpp-extra-args="-DCANT_CHECK"
*/
diff --git a/tests/metrics/locals_size.i b/tests/metrics/locals_size.i
index 8e02226c49c..bd261320029 100644
--- a/tests/metrics/locals_size.i
+++ b/tests/metrics/locals_size.i
@@ -1,8 +1,8 @@
/* run.config
+ EXIT: 1
OPT: -metrics-locals-size f,g,level3,level2,level1,main
OPT: -metrics-locals-size recurse2
*/
-
// locals size without temps: 0
int f() {
static int count = 0; // not a local
diff --git a/tests/misc/bts0451.i b/tests/misc/bts0451.i
index 02c2288f0d4..4ba9f9768c5 100644
--- a/tests/misc/bts0451.i
+++ b/tests/misc/bts0451.i
@@ -1,5 +1,6 @@
/* run.config
COMMENT: running this test fails on purpose
+ EXIT: 1
OPT: -simplify-cfg -typecheck
*/
diff --git a/tests/misc/bts0990_link.i b/tests/misc/bts0990_link.i
index 5edc84415b3..84c8e1f479d 100644
--- a/tests/misc/bts0990_link.i
+++ b/tests/misc/bts0990_link.i
@@ -1,7 +1,7 @@
-/* run.config
+/* run.config*
+ EXIT: 1
OPT: tests/misc/bts0990_link_1.i
*/
-
// NB: This test is meant to return an error, as s is declared as an array in
// tests/misc/bts0990_link_1.i
diff --git a/tests/misc/custom_machdep.c b/tests/misc/custom_machdep.c
index f7a377dc162..87979f0608b 100644
--- a/tests/misc/custom_machdep.c
+++ b/tests/misc/custom_machdep.c
@@ -1,9 +1,10 @@
/* run.config*
-EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.cmxs
-OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-module @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@ -machdep custom -print -then -print
-COMMENT: we need a -then to test double registering of a machdep
-*/
+ EXIT: 1
+ EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@.cmxs
+ OPT: -cpp-extra-args="-I@PTEST_DIR@/@PTEST_NAME@ -D__FC_MACHDEP_CUSTOM" -load-module @PTEST_DIR@/@PTEST_NAME@/@PTEST_NAME@ -machdep custom -print -then -print
+ COMMENT: we need a -then to test double registering of a machdep
+*/
#include "__fc_machdep_custom.h"
// most of the following includes are not directly used, but they test if
// the custom machdep has defined the necessary constants
diff --git a/tests/misc/debug_category.i b/tests/misc/debug_category.i
index 5646776c8be..6b4a7dbc2c3 100644
--- a/tests/misc/debug_category.i
+++ b/tests/misc/debug_category.i
@@ -1,21 +1,28 @@
-/* run.config
+/* run.config*
MODULE: tests/misc/Debug_category.cmxs
-OPT: -test-msg-key help -test-warn-key="a=inactive"
-OPT: -test-msg-key a -test-warn-key="a=inactive"
-OPT: -test-msg-key a -test-msg-key="-a:b" -test-warn-key="a=inactive"
-OPT: -test-msg-key a -test-msg-key="-a:b" -test-msg-key a:b:c -test-warn-key="a=inactive"
-OPT: -test-msg-key "a:b:c,d" -test-warn-key="a=inactive"
-OPT: -test-msg-key "*" -test-warn-key="a=inactive"
-OPT:
-OPT: -test-warn-key a=error
-OPT: -test-warn-key a=abort
-OPT: -test-warn-key a=feedback
-OPT: -test-warn-key="*=abort"
-OPT: -test-warn-key=a=once
-OPT: -test-warn-key a=feedback-once
-OPT: -test-warn-key a=err-once
-OPT: -test-warn-key test-vis-err
-OPT: -test-warn-key test-inv-err
-OPT: -test-warn-key test-failure
+EXIT: 0
+ OPT: -test-msg-key help -test-warn-key="a=inactive"
+ OPT: -test-msg-key a -test-warn-key="a=inactive"
+ OPT: -test-msg-key a -test-msg-key="-a:b" -test-warn-key="a=inactive"
+ OPT: -test-msg-key a -test-msg-key="-a:b" -test-msg-key a:b:c -test-warn-key="a=inactive"
+ OPT: -test-msg-key "a:b:c,d" -test-warn-key="a=inactive"
+ OPT: -test-msg-key "*" -test-warn-key="a=inactive"
+ OPT:
+EXIT: 1
+ OPT: -test-warn-key a=error
+ OPT: -test-warn-key a=abort
+EXIT: 0
+ OPT: -test-warn-key a=feedback
+EXIT: 1
+ OPT: -test-warn-key="*=abort"
+EXIT: 0
+ OPT: -test-warn-key=a=once
+ OPT: -test-warn-key a=feedback-once
+EXIT: 1
+ OPT: -test-warn-key a=err-once
+ OPT: -test-warn-key test-vis-err
+ OPT: -test-warn-key test-inv-err
+EXIT: 4
+ OPT: -test-warn-key test-failure
FILTER: sed 's|Your Frama-C version is.*|Your Frama-C version is VERSION|'
*/
diff --git a/tests/misc/filepath.i b/tests/misc/filepath.i
index a8892bc2d2f..40748281b88 100644
--- a/tests/misc/filepath.i
+++ b/tests/misc/filepath.i
@@ -1,5 +1,6 @@
-/* run.config
+/* run.config*
MODULE: tests/misc/filepath_test.cmxs
COMMENT: the '-load' option below intentionally contains an error
+ EXIT: 1
OPT: -no-autoload-plugins -load nonexistent_file.sav
*/
diff --git a/tests/misc/function_ptr_alignof.i b/tests/misc/function_ptr_alignof.i
index 4a8970e7f7b..1f4b218d0bf 100644
--- a/tests/misc/function_ptr_alignof.i
+++ b/tests/misc/function_ptr_alignof.i
@@ -1,6 +1,9 @@
-/* run.config
+/* run.config*
+ EXIT: 1
+ STDOPT:
*/
+
void f(void) { }
int main(void)
diff --git a/tests/misc/function_ptr_lvalue_1.i b/tests/misc/function_ptr_lvalue_1.i
index 723aa9d837e..b48ddbd09f7 100644
--- a/tests/misc/function_ptr_lvalue_1.i
+++ b/tests/misc/function_ptr_lvalue_1.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
void f(void) {}
int main()
diff --git a/tests/misc/function_ptr_lvalue_2.i b/tests/misc/function_ptr_lvalue_2.i
index 0ce6903f296..333304c449f 100644
--- a/tests/misc/function_ptr_lvalue_2.i
+++ b/tests/misc/function_ptr_lvalue_2.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
void f(void) {}
int main()
diff --git a/tests/misc/function_ptr_sizeof.i b/tests/misc/function_ptr_sizeof.i
index 1a71bc26d20..36558b8808f 100644
--- a/tests/misc/function_ptr_sizeof.i
+++ b/tests/misc/function_ptr_sizeof.i
@@ -1,6 +1,9 @@
-/* run.config
+/* run.config*
+ EXIT: 1
+ STDOPT:
*/
+
void f(void) { }
int main(void)
diff --git a/tests/misc/global_decl_loc2.i b/tests/misc/global_decl_loc2.i
index 08fe31aa7b6..348015c7c22 100644
--- a/tests/misc/global_decl_loc2.i
+++ b/tests/misc/global_decl_loc2.i
@@ -1,4 +1,6 @@
-/* run.config
+/* run.config*
+ EXIT: 0
+
OPT: @PTEST_DIR@/global_decl_loc.i -load-module @PTEST_DIR@/global_decl_loc.cmxs
*/
diff --git a/tests/misc/log_selfrec.i b/tests/misc/log_selfrec.i
index f65505058bb..e7a647f6e45 100644
--- a/tests/misc/log_selfrec.i
+++ b/tests/misc/log_selfrec.i
@@ -1,3 +1,5 @@
-/* run.config
+/* run.config*
+
+ EXIT: 1
OPT: -foobar -report-unclassified-error jazz
*/
diff --git a/tests/misc/widen_hints.c b/tests/misc/widen_hints.c
index e4f063807c1..fca1b6e7e6e 100644
--- a/tests/misc/widen_hints.c
+++ b/tests/misc/widen_hints.c
@@ -1,6 +1,8 @@
/* run.config
+ EXIT:1
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DSYNTAX_ERRORS -kernel-warn-key=annot-error=active
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DNONCONST
+ EXIT:0
OPT: -eva @EVA_CONFIG@ -eva-slevel 1 -eva-msg-key widen-hints
OPT: -eva @EVA_CONFIG@ -cpp-extra-args=-DALLGLOBAL -eva-msg-key widen-hints
*/
diff --git a/tests/spec/multiple_include_2.c b/tests/spec/multiple_include_2.c
index 473facee9ad..942e2276909 100644
--- a/tests/spec/multiple_include_2.c
+++ b/tests/spec/multiple_include_2.c
@@ -1,6 +1,9 @@
/* run.config
+ EXIT: 1
+
OPT: -kernel-warn-key=annot-error=active -print tests/spec/multiple_include_1.c -journal-disable
*/
+
#include "multiple_include.h"
/*@ requires p(x); */
diff --git a/tests/syntax/alloc_order.i b/tests/syntax/alloc_order.i
index 2638caa2c26..7d67b5393d7 100644
--- a/tests/syntax/alloc_order.i
+++ b/tests/syntax/alloc_order.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
/*@
allocates \result;
requires i > 0;
diff --git a/tests/syntax/arg_type.i b/tests/syntax/arg_type.i
index d0e4e03c2d8..7f17b62b700 100644
--- a/tests/syntax/arg_type.i
+++ b/tests/syntax/arg_type.i
@@ -1,9 +1,9 @@
-/* run.config
-STDOPT: +"-machdep gcc_x86_32"
+/* run.config*
+ EXIT: 1
+ STDOPT: +"-machdep gcc_x86_32"
*/
// GCC allows such things
-
int f(int);
int f(x) short x; { return x; }
diff --git a/tests/syntax/array_cast_bts1099.i b/tests/syntax/array_cast_bts1099.i
index 636b1969432..39ae9a0e8de 100644
--- a/tests/syntax/array_cast_bts1099.i
+++ b/tests/syntax/array_cast_bts1099.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
typedef int t[10];
typedef int u[4];
diff --git a/tests/syntax/array_size.i b/tests/syntax/array_size.i
index 11f210ed568..e8d46d0178a 100644
--- a/tests/syntax/array_size.i
+++ b/tests/syntax/array_size.i
@@ -1 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
int f(int t[-1]) { return t[0]; } // should raise an error
diff --git a/tests/syntax/axiomatic_nested.i b/tests/syntax/axiomatic_nested.i
index fce725aabdb..217425c9ef4 100644
--- a/tests/syntax/axiomatic_nested.i
+++ b/tests/syntax/axiomatic_nested.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
/*@
axiomatic bla1 {
// nested axiomatics are not allowed
diff --git a/tests/syntax/bad_return_bts_599.i b/tests/syntax/bad_return_bts_599.i
index 6265f34c06d..9ccba084dc2 100644
--- a/tests/syntax/bad_return_bts_599.i
+++ b/tests/syntax/bad_return_bts_599.i
@@ -1,4 +1,7 @@
-
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
int BadReturn1(int* p) {
*p++;
return;
diff --git a/tests/syntax/bts0519.c b/tests/syntax/bts0519.c
index 9c171310371..41a8ff2c7bb 100644
--- a/tests/syntax/bts0519.c
+++ b/tests/syntax/bts0519.c
@@ -1,5 +1,6 @@
/* run.config
STDOPT: +"-cpp-command='gcc -C -E -I.'" +"-cpp-frama-c-compliant"
+ EXIT: 1
STDOPT: +"-cpp-command='gcc -C -E -I. -DERR'" +"-cpp-frama-c-compliant"
*/
diff --git a/tests/syntax/cert-dcl-36.c b/tests/syntax/cert-dcl-36.c
index fe5fdb97b7b..78b17597c86 100644
--- a/tests/syntax/cert-dcl-36.c
+++ b/tests/syntax/cert-dcl-36.c
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
int i1 = 10; /* Definition, external linkage */
static int i2 = 20; /* Definition, internal linkage */
extern int i3 = 30; /* Definition, external linkage */
diff --git a/tests/syntax/cert_msc_38.c b/tests/syntax/cert_msc_38.c
index d15f0eaccac..ad9f6024580 100644
--- a/tests/syntax/cert_msc_38.c
+++ b/tests/syntax/cert_msc_38.c
@@ -1,12 +1,13 @@
/* run.config
-STDOPT: +"-cpp-extra-args='-DTEST_ASSERT'"
-STDOPT: +"-cpp-extra-args='-DTEST_ERRNO'"
-STDOPT: +"-cpp-extra-args='-DTEST_MATHERRHANDLING'"
-STDOPT: +"-cpp-extra-args='-DTEST_VASTART'"
-STDOPT: +"-cpp-extra-args='-DTEST_VACOPY'"
-STDOPT: +"-cpp-extra-args='-DTEST_VAARG'"
-STDOPT: +"-cpp-extra-args='-DTEST_VAEND'"
-STDOPT: +"-cpp-extra-args='-DTEST_SETJMP'"
+ EXIT: 1
+ STDOPT: +"-cpp-extra-args='-DTEST_ASSERT'"
+ STDOPT: +"-cpp-extra-args='-DTEST_ERRNO'"
+ STDOPT: +"-cpp-extra-args='-DTEST_MATHERRHANDLING'"
+ STDOPT: +"-cpp-extra-args='-DTEST_VASTART'"
+ STDOPT: +"-cpp-extra-args='-DTEST_VACOPY'"
+ STDOPT: +"-cpp-extra-args='-DTEST_VAARG'"
+ STDOPT: +"-cpp-extra-args='-DTEST_VAEND'"
+ STDOPT: +"-cpp-extra-args='-DTEST_SETJMP'"
*/
#include <assert.h>
#include <stdarg.h>
diff --git a/tests/syntax/composite-tags.i b/tests/syntax/composite-tags.i
index b823ffdf4a1..57cf567357e 100644
--- a/tests/syntax/composite-tags.i
+++ b/tests/syntax/composite-tags.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
struct s1 { int a; };
struct s2 { int a; };
diff --git a/tests/syntax/const-assignments.c b/tests/syntax/const-assignments.c
index a04efd9d97b..745a67aa56a 100644
--- a/tests/syntax/const-assignments.c
+++ b/tests/syntax/const-assignments.c
@@ -1,21 +1,21 @@
/* run.config
STDOPT:
+ EXIT:1
STDOPT: +" -cpp-extra-args=-DT0"
STDOPT: +" -cpp-extra-args=-DT1"
STDOPT: +" -cpp-extra-args=-DT2"
STDOPT: +" -cpp-extra-args=-DT3"
STDOPT: +" -cpp-extra-args=-DT4"
STDOPT: +" -cpp-extra-args=-DT5"
+ EXIT:0
STDOPT: +" -cpp-extra-args=-DT6"
STDOPT: +" -cpp-extra-args=-DT7"
+ EXIT:1
STDOPT: +" -cpp-extra-args=-DT8"
*/
-
/* The first run is correct. The others should fail, as they include invalid
assignments to const lvalues. */
const int x = 1;
-
-
#ifdef T0
void f() {
x = 42;
diff --git a/tests/syntax/duplicate_field.i b/tests/syntax/duplicate_field.i
index 4d87d6db6e9..0182c652f28 100644
--- a/tests/syntax/duplicate_field.i
+++ b/tests/syntax/duplicate_field.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
struct test{
int x;
int x;
diff --git a/tests/syntax/fam.i b/tests/syntax/fam.i
index b91d73a9580..c7239abee35 100644
--- a/tests/syntax/fam.i
+++ b/tests/syntax/fam.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
// Tests related to flexible array members
// FAM declaration OK
diff --git a/tests/syntax/flexible_array_member_invalid1.i b/tests/syntax/flexible_array_member_invalid1.i
index 62ebdab3e24..5db7343892a 100644
--- a/tests/syntax/flexible_array_member_invalid1.i
+++ b/tests/syntax/flexible_array_member_invalid1.i
@@ -1,3 +1,8 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
+
// invalid flexible array member (empty struct otherwise)
struct s1 {
char data[];
diff --git a/tests/syntax/flexible_array_member_invalid2.i b/tests/syntax/flexible_array_member_invalid2.i
index eab5dccd0c3..9cda9f447e3 100644
--- a/tests/syntax/flexible_array_member_invalid2.i
+++ b/tests/syntax/flexible_array_member_invalid2.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
// invalid flexible array member (two incomplete fields)
struct s {
int len;
diff --git a/tests/syntax/flexible_array_member_invalid3.i b/tests/syntax/flexible_array_member_invalid3.i
index 4baf088c14f..59fca4bf347 100644
--- a/tests/syntax/flexible_array_member_invalid3.i
+++ b/tests/syntax/flexible_array_member_invalid3.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
// invalid flexible array member (two incomplete fields in same field group)
struct s {
int len;
diff --git a/tests/syntax/flexible_array_member_invalid4.i b/tests/syntax/flexible_array_member_invalid4.i
index e84cce94b98..99e25916b20 100644
--- a/tests/syntax/flexible_array_member_invalid4.i
+++ b/tests/syntax/flexible_array_member_invalid4.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
// invalid flexible array member (incomplete field is not last)
struct s {
int len;
diff --git a/tests/syntax/flexible_array_member_invalid5.i b/tests/syntax/flexible_array_member_invalid5.i
index a0339194afe..35dbe5c3064 100644
--- a/tests/syntax/flexible_array_member_invalid5.i
+++ b/tests/syntax/flexible_array_member_invalid5.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
// In C99, flexible array members cannot be nested inside other structs
typedef struct {
int a;
diff --git a/tests/syntax/ghost_cv_incompat.i b/tests/syntax/ghost_cv_incompat.i
index 0de775a8e05..e75186e231c 100644
--- a/tests/syntax/ghost_cv_incompat.i
+++ b/tests/syntax/ghost_cv_incompat.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
typedef int int_array [10] ;
struct Type { int field ; } ;
diff --git a/tests/syntax/ghost_cv_invalid_use.i b/tests/syntax/ghost_cv_invalid_use.i
index a4e082cc808..f2729c2ea24 100644
--- a/tests/syntax/ghost_cv_invalid_use.i
+++ b/tests/syntax/ghost_cv_invalid_use.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
// In this file, each write raises an error: writing non-ghost memory location
// from ghost code, except if a comment says the opposite.
diff --git a/tests/syntax/ghost_cv_parsing_errors.c b/tests/syntax/ghost_cv_parsing_errors.c
index 55637c2cad5..08ecf3c1bc5 100644
--- a/tests/syntax/ghost_cv_parsing_errors.c
+++ b/tests/syntax/ghost_cv_parsing_errors.c
@@ -1,4 +1,5 @@
/* run.config
+ EXIT: 1
OPT:-cpp-extra-args="-DIN_TYPE"
OPT:-cpp-extra-args="-DIN_DECL"
OPT:-cpp-extra-args="-DIN_GHOST_ATTR"
diff --git a/tests/syntax/ghost_cv_var_decl.c b/tests/syntax/ghost_cv_var_decl.c
index 6a8f1922b98..180192d7e25 100644
--- a/tests/syntax/ghost_cv_var_decl.c
+++ b/tests/syntax/ghost_cv_var_decl.c
@@ -1,5 +1,8 @@
/* run.config
+
+ EXIT: 1
OPT:-cpp-extra-args="-DFAIL_DECL_TYPE"
+ EXIT: 0
OPT:-load-script @PTEST_DIR@/@PTEST_NAME@.ml
*/
diff --git a/tests/syntax/ghost_else_bad.c b/tests/syntax/ghost_else_bad.c
index 0fad3b59986..151b38dcf8e 100644
--- a/tests/syntax/ghost_else_bad.c
+++ b/tests/syntax/ghost_else_bad.c
@@ -1,12 +1,12 @@
/* run.config
+ EXIT: 1
OPT: -no-autoload-plugins -cpp-extra-args="-DERROR_LOC_WITH_COMMENTS"
+ EXIT: 0
OPT: -no-autoload-plugins -cpp-extra-args="-DALREADY_HAS_ELSE" -print -kernel-warn-key ghost:bad-use=feedback
+ EXIT: 1
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++;
diff --git a/tests/syntax/ghost_else_bad_oneline.i b/tests/syntax/ghost_else_bad_oneline.i
index d78f5e54a4d..a7cd33e3341 100644
--- a/tests/syntax/ghost_else_bad_oneline.i
+++ b/tests/syntax/ghost_else_bad_oneline.i
@@ -1,7 +1,7 @@
/* run.config
+ EXIT: 1
OPT: -no-autoload-plugins -print
*/
-
void if_ghost_else_one_line_bad(int x, int y) {
if (x) {
x++;
diff --git a/tests/syntax/ghost_local_ill_formed.i b/tests/syntax/ghost_local_ill_formed.i
index d3d786b2880..5492f24a3af 100644
--- a/tests/syntax/ghost_local_ill_formed.i
+++ b/tests/syntax/ghost_local_ill_formed.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
void titi() {
int c = 0;
L0: ;
diff --git a/tests/syntax/ghost_multiline_annot.c b/tests/syntax/ghost_multiline_annot.c
index 2d7d0796920..efa2a0566c5 100644
--- a/tests/syntax/ghost_multiline_annot.c
+++ b/tests/syntax/ghost_multiline_annot.c
@@ -1,18 +1,18 @@
/* run.config
STDOPT: +" -cpp-extra-args=-DP0"
+ EXIT: 1
STDOPT: +" -cpp-extra-args=-DP1"
STDOPT: +" -cpp-extra-args=-DP2"
STDOPT: +" -cpp-extra-args=-DP3"
STDOPT: +" -cpp-extra-args=-DP4"
STDOPT: +" -cpp-extra-args=-DP5"
+ EXIT: 0
STDOPT: +" -cpp-extra-args=-DP6"
STDOPT: +" -cpp-extra-args=-DP7"
STDOPT: +" -cpp-extra-args=-DP8"
*/
-
#ifdef P0
-int main(int c)
-{
+int main(int c) {
/*@ ghost //@ requires c >= 0;
int x = c;
/@ loop invariant x >= 0;
diff --git a/tests/syntax/ghost_parameters.c b/tests/syntax/ghost_parameters.c
index b1caed23168..db9dce1ccf5 100644
--- a/tests/syntax/ghost_parameters.c
+++ b/tests/syntax/ghost_parameters.c
@@ -1,7 +1,10 @@
/* run.config
+ EXIT: 1
STDOPT: +" -cpp-extra-args=-DARGS_NOT_VOID"
STDOPT: +" -cpp-extra-args=-DARGS_VOID"
+ EXIT: 0
STDOPT: +" -cpp-extra-args=-DCOHERENT_DECL"
+ EXIT: 1
STDOPT: +" -cpp-extra-args=-DINCOHERENT_LOCAL_DECL_NON_GHOST"
STDOPT: +" -cpp-extra-args=-DINCOHERENT_GLOBAL_DECL_NON_GHOST"
STDOPT: +" -cpp-extra-args=-DINCOHERENT_LOCAL_DECL_GHOST"
diff --git a/tests/syntax/incompatible_qualifiers.c b/tests/syntax/incompatible_qualifiers.c
index 66371e18b3a..1eed4134eca 100644
--- a/tests/syntax/incompatible_qualifiers.c
+++ b/tests/syntax/incompatible_qualifiers.c
@@ -1,6 +1,8 @@
-/*run.config
- STDOPT:
- STDOPT: #"-cpp-extra-args='-DNOERROR'"
+/* run.config
+ EXIT: 1
+ STDOPT:
+ EXIT: 0
+ STDOPT: #"-cpp-extra-args='-DNOERROR'"
*/
// Note: some of the declarations below are accepted by GCC 7.1.1 with -std=c11
// (but not -std=c99), mainly due to this warning (use -Wextra to see it):
diff --git a/tests/syntax/incomplete_array.i b/tests/syntax/incomplete_array.i
index b2e82193a25..3ec41da4ee6 100644
--- a/tests/syntax/incomplete_array.i
+++ b/tests/syntax/incomplete_array.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
/* variation around issue #2091 */
struct S;
diff --git a/tests/syntax/incomplete_struct_field.i b/tests/syntax/incomplete_struct_field.i
index c9e20e50f12..ed81a5d3f69 100644
--- a/tests/syntax/incomplete_struct_field.i
+++ b/tests/syntax/incomplete_struct_field.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
typedef struct _s {
int i;
struct _s v[12];
diff --git a/tests/syntax/inconsistent_decl.c b/tests/syntax/inconsistent_decl.c
index 0c7901651cf..c4cb37aa00a 100644
--- a/tests/syntax/inconsistent_decl.c
+++ b/tests/syntax/inconsistent_decl.c
@@ -1,6 +1,7 @@
/* run.config
-STDOPT: +"tests/syntax/inconsistent_decl_2.i"
-STDOPT: +"tests/syntax/inconsistent_decl_2.i"+"-cpp-extra-args='-DWITH_PROTO'"
+EXIT: 1
+ STDOPT: +"tests/syntax/inconsistent_decl_2.i"
+ STDOPT: +"tests/syntax/inconsistent_decl_2.i"+"-cpp-extra-args='-DWITH_PROTO'"
*/
#ifdef WITH_PROTO
diff --git a/tests/syntax/inconsistent_global_ghost_spec.c b/tests/syntax/inconsistent_global_ghost_spec.c
index 8a3aa44011c..231b0c1123f 100644
--- a/tests/syntax/inconsistent_global_ghost_spec.c
+++ b/tests/syntax/inconsistent_global_ghost_spec.c
@@ -1,10 +1,10 @@
/* run.config
-OPT: -cpp-extra-args="-DNON_GHOST_DECL_GHOST_DEF"
-OPT: -cpp-extra-args="-DGHOST_DECL_NON_GHOST_DEF"
-OPT: -cpp-extra-args="-DGHOST_DEF_NON_GHOST_DECL"
-OPT: -cpp-extra-args="-DNON_GHOST_DEF_GHOST_DECL"
+EXIT: 1
+ OPT: -cpp-extra-args="-DNON_GHOST_DECL_GHOST_DEF"
+ OPT: -cpp-extra-args="-DGHOST_DECL_NON_GHOST_DEF"
+ OPT: -cpp-extra-args="-DGHOST_DEF_NON_GHOST_DECL"
+ OPT: -cpp-extra-args="-DNON_GHOST_DEF_GHOST_DECL"
*/
-
#ifdef NON_GHOST_DECL_GHOST_DEF
void function(void) ;
diff --git a/tests/syntax/init_bts1352.i b/tests/syntax/init_bts1352.i
index afe1a02aade..ddfa14d7052 100644
--- a/tests/syntax/init_bts1352.i
+++ b/tests/syntax/init_bts1352.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
int main(void) {
int t /* [5] missing */ = { 1, 2, 3, 4, 5 };
}
diff --git a/tests/syntax/invalid_constant.i b/tests/syntax/invalid_constant.i
index 5f429de8626..5db196f7880 100644
--- a/tests/syntax/invalid_constant.i
+++ b/tests/syntax/invalid_constant.i
@@ -1,2 +1,6 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
/* Invalid octal constant */
int i = 0123456789;
diff --git a/tests/syntax/line_number.c b/tests/syntax/line_number.c
index 97e763362e2..c3535c628d2 100644
--- a/tests/syntax/line_number.c
+++ b/tests/syntax/line_number.c
@@ -1,2 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
//@ assert \result == 0;
extern int p(void void);
diff --git a/tests/syntax/lvalvoid.i b/tests/syntax/lvalvoid.i
index 39840bd6cf9..a0de92104f8 100644
--- a/tests/syntax/lvalvoid.i
+++ b/tests/syntax/lvalvoid.i
@@ -1,3 +1,7 @@
+/* run.config
+ EXIT: 1
+ STDOPT:
+*/
void* memcpy1(void* dst, const void *src,long n) {
char* d=dst; char* s=src;
for (int i=0;i<n;i++)
diff --git a/tests/syntax/merge_attrs_align.c b/tests/syntax/merge_attrs_align.c
index 71d62ce185b..ef3528b0d15 100644
--- a/tests/syntax/merge_attrs_align.c
+++ b/tests/syntax/merge_attrs_align.c
@@ -1,8 +1,11 @@
/*run.config
+ EXIT: 1
STDOPT: +"-machdep x86_64" +"tests/syntax/merge_attrs_align1.c" +"tests/syntax/merge_attrs_align2.c"
STDOPT: +"-machdep x86_64" +"tests/syntax/merge_attrs_align1.c" +"tests/syntax/merge_attrs_align3.c"
+ EXIT: 0
STDOPT: +"-machdep x86_64" +"tests/syntax/merge_attrs_align1.c" +"tests/syntax/merge_attrs_align4.c"
STDOPT: +"-machdep x86_64" +"tests/syntax/merge_attrs_align2.c" +"tests/syntax/merge_attrs_align3.c"
+ EXIT: 1
STDOPT: +"-machdep x86_64" +"tests/syntax/merge_attrs_align2.c" +"tests/syntax/merge_attrs_align4.c"
STDOPT: +"-machdep x86_64" +"tests/syntax/merge_attrs_align3.c" +"tests/syntax/merge_attrs_align4.c"
*/
diff --git a/tests/syntax/merge_unused.c b/tests/syntax/merge_unused.c
index b7233c675d0..d8a15d22f66 100644
--- a/tests/syntax/merge_unused.c
+++ b/tests/syntax/merge_unused.c
@@ -1,7 +1,8 @@
-/* run.config
-OPT: -cpp-extra-args="-I@PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c -print
-*/
+/* run.config*
+EXIT: 1
+ OPT: -cpp-extra-args="-I@PTEST_DIR@" @PTEST_DIR@/@PTEST_NAME@_2.c -print
+*/
#pragma pack(1)
#include "merge_unused.h"
diff --git a/tests/syntax/multiple_assigns.i b/tests/syntax/multiple_assigns.i
index d20a1dfcda4..1d1d9d7eb51 100644
--- a/tests/syntax/multiple_assigns.i
+++ b/tests/syntax/multiple_assigns.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 0
+ STDOPT:
+*/
int z;
/*@ assigns z, z;
diff --git a/tests/syntax/multiple_froms.i b/tests/syntax/multiple_froms.i
index 6a0a25687f9..fb2cf140850 100644
--- a/tests/syntax/multiple_froms.i
+++ b/tests/syntax/multiple_froms.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 0
+ STDOPT:
+*/
+
+
int a, b, c, d, e;
// Reminder: assigns are visited in reverse
diff --git a/tests/syntax/mutually_recursive_struct.i b/tests/syntax/mutually_recursive_struct.i
index 7d4f460b375..2aed6a096ca 100644
--- a/tests/syntax/mutually_recursive_struct.i
+++ b/tests/syntax/mutually_recursive_struct.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
struct S1;
struct S2;
diff --git a/tests/syntax/no_prototype.i b/tests/syntax/no_prototype.i
index 47d289de12e..a0185f6bcfc 100644
--- a/tests/syntax/no_prototype.i
+++ b/tests/syntax/no_prototype.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
void foo();
int main(void) {
diff --git a/tests/syntax/reject_use_decl_mismatch_bts728.c b/tests/syntax/reject_use_decl_mismatch_bts728.c
index d100d64669c..1dde8a89eb9 100644
--- a/tests/syntax/reject_use_decl_mismatch_bts728.c
+++ b/tests/syntax/reject_use_decl_mismatch_bts728.c
@@ -1,8 +1,8 @@
/* run.config
-STDOPT: +"-cpp-extra-args='-DHAS_PROTO'"
-STDOPT: +"-cpp-extra-args='-DNO_PROTO'"
+EXIT: 1
+ STDOPT: +"-cpp-extra-args='-DHAS_PROTO'"
+ STDOPT: +"-cpp-extra-args='-DNO_PROTO'"
*/
-
#ifdef HAS_PROTO
int f();
#endif
diff --git a/tests/syntax/rettype.i b/tests/syntax/rettype.i
index df437409f8d..c95988c278f 100644
--- a/tests/syntax/rettype.i
+++ b/tests/syntax/rettype.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
// This test must be rejected: return type of foo is not
// compatible between decl and def.
diff --git a/tests/syntax/sizeof_incomplete_type.c b/tests/syntax/sizeof_incomplete_type.c
index 64b91652f8c..371b1c0c91d 100644
--- a/tests/syntax/sizeof_incomplete_type.c
+++ b/tests/syntax/sizeof_incomplete_type.c
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
#include <stdlib.h>
typedef char *sds;
diff --git a/tests/syntax/spurious_brace_bts_1273.i b/tests/syntax/spurious_brace_bts_1273.i
index 25e660061ae..6c3f8232240 100644
--- a/tests/syntax/spurious_brace_bts_1273.i
+++ b/tests/syntax/spurious_brace_bts_1273.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
void foo() {
}
}
diff --git a/tests/syntax/struct_with_function_field_invalid.i b/tests/syntax/struct_with_function_field_invalid.i
index b532103ecd1..c522453305f 100644
--- a/tests/syntax/struct_with_function_field_invalid.i
+++ b/tests/syntax/struct_with_function_field_invalid.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
// invalid field with function type, parsing should fail
struct {
void f(int);
diff --git a/tests/syntax/syntactic_hook.i b/tests/syntax/syntactic_hook.i
index d887e89667e..0b5e7a8bf6a 100644
--- a/tests/syntax/syntactic_hook.i
+++ b/tests/syntax/syntactic_hook.i
@@ -1,7 +1,10 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
+ EXIT: 1
STDOPT: +"-no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs"
*/
+
+
int f(void);
int k(int *);
diff --git a/tests/syntax/type_branch_bts_1081.i b/tests/syntax/type_branch_bts_1081.i
index 31f1929c13f..2e1f1903a2e 100644
--- a/tests/syntax/type_branch_bts_1081.i
+++ b/tests/syntax/type_branch_bts_1081.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
int main(){
int foo, x, y;
foo ? (void)x : (signed char)y;
diff --git a/tests/syntax/type_redef.i b/tests/syntax/type_redef.i
index 28d719f0638..2c56c35150b 100644
--- a/tests/syntax/type_redef.i
+++ b/tests/syntax/type_redef.i
@@ -1,8 +1,8 @@
/* run.config
+ EXIT: 1
STDOPT:
STDOPT: #"-c11"
*/ // Note: redefinition of local typedefs is currently unsupported
-
typedef int myint;
typedef int myint; //valid in C11 only
diff --git a/tests/syntax/typedef_namespace_bts1500.c b/tests/syntax/typedef_namespace_bts1500.c
index 60dd7dd9eff..9e7dd5eb589 100644
--- a/tests/syntax/typedef_namespace_bts1500.c
+++ b/tests/syntax/typedef_namespace_bts1500.c
@@ -1,7 +1,8 @@
-/* run.config
-STDOPT:
-STDOPT: +"-cpp-extra-args='-DHIDING_TYPEDEF'"
-STDOPT: +"-cpp-extra-args='-DREDEFINITION'"
+/* run.config*
+ STDOPT:
+ EXIT: 1
+ STDOPT: +"-cpp-extra-args='-DHIDING_TYPEDEF'"
+ STDOPT: +"-cpp-extra-args='-DREDEFINITION'"
*/
typedef int digit;
diff --git a/tests/syntax/va.c b/tests/syntax/va.c
index 302e682dfe5..5286293ce2c 100644
--- a/tests/syntax/va.c
+++ b/tests/syntax/va.c
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
#include "stdarg.h"
#include "stdio.h"
diff --git a/tests/syntax/vla_goto.i b/tests/syntax/vla_goto.i
index 7f760f860d6..f7e7f87cd91 100644
--- a/tests/syntax/vla_goto.i
+++ b/tests/syntax/vla_goto.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
int case2(int arg) {
{
int a2[arg];
diff --git a/tests/syntax/vla_goto3.i b/tests/syntax/vla_goto3.i
index 53ffedf5381..28949ee17ff 100644
--- a/tests/syntax/vla_goto3.i
+++ b/tests/syntax/vla_goto3.i
@@ -1,3 +1,7 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
volatile int nondet;
int main () {
diff --git a/tests/syntax/vla_goto_same_block_below.i b/tests/syntax/vla_goto_same_block_below.i
index 3e163f3bb82..58b86079ef7 100644
--- a/tests/syntax/vla_goto_same_block_below.i
+++ b/tests/syntax/vla_goto_same_block_below.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
volatile int nondet ;
int main() {
diff --git a/tests/syntax/vla_switch.i b/tests/syntax/vla_switch.i
index afa7dd0affc..7d8222ecd80 100644
--- a/tests/syntax/vla_switch.i
+++ b/tests/syntax/vla_switch.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
int case3(int arg) {
switch(arg) {
// Illegal according to 6.8.4.2§2
diff --git a/tests/syntax/void_parameter.i b/tests/syntax/void_parameter.i
index f4a14535232..d5eb9df2e06 100644
--- a/tests/syntax/void_parameter.i
+++ b/tests/syntax/void_parameter.i
@@ -1,7 +1,7 @@
-/* run.config
-
+/* run.config*
+ EXIT: 1
+ STDOPT:
*/
-
// GCC warning, Clang/CompCert error
void f1(void);
void f2(void parameter);
@@ -13,4 +13,3 @@ void f1(void){}
void f2(void parameter){}
void f3(void, int x){}
void f4(void parameter, int x){}
-
diff --git a/tests/syntax/wrong-assignment.i b/tests/syntax/wrong-assignment.i
index da2a59b86ae..04dd59e8d98 100644
--- a/tests/syntax/wrong-assignment.i
+++ b/tests/syntax/wrong-assignment.i
@@ -1,3 +1,9 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
+
typedef struct { _Bool a; } ebool;
ebool b, c;
diff --git a/tests/syntax/wrong_label.i b/tests/syntax/wrong_label.i
index 90e1020b409..bbde72ccbdd 100644
--- a/tests/syntax/wrong_label.i
+++ b/tests/syntax/wrong_label.i
@@ -1,3 +1,8 @@
+/* run.config*
+ EXIT: 1
+ STDOPT:
+*/
+
void f() {
/*@ assert \true; */
}
diff --git a/tests/value/array_zero_length.i b/tests/value/array_zero_length.i
index f84a4ebf84a..98d5d3527c9 100644
--- a/tests/value/array_zero_length.i
+++ b/tests/value/array_zero_length.i
@@ -1,6 +1,7 @@
/* run.config*
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -journal-disable -machdep gcc_x86_32
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable -machdep gcc_x86_32
+ EXIT: 1
OPT: -no-autoload-plugins -load-module inout,eva -eva @EVA_CONFIG@ -lib-entry -journal-disable
*/
diff --git a/tests/value/empty_base.c b/tests/value/empty_base.c
index 1a5baf64c3b..d51b1b0f486 100644
--- a/tests/value/empty_base.c
+++ b/tests/value/empty_base.c
@@ -1,4 +1,5 @@
/* run.config*
+ EXIT: 1
STDOPT: +"-machdep gcc_x86_32"
STDOPT:
*/
diff --git a/tests/value/recursion.i b/tests/value/recursion.i
index 2b916a17354..c3670163290 100644
--- a/tests/value/recursion.i
+++ b/tests/value/recursion.i
@@ -1,4 +1,5 @@
-/*run.config*
+/* run.config*
+ EXIT: 1
OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -journal-disable
OPT: -no-autoload-plugins -load-module from,inout,eva -lib-entry -main main -eva @EVA_CONFIG@ -eva-ignore-recursive-calls -journal-disable
*/
diff --git a/tests/value/split_return.i b/tests/value/split_return.i
index 8cfc8a21a75..df9fbcbdada 100644
--- a/tests/value/split_return.i
+++ b/tests/value/split_return.i
@@ -1,12 +1,15 @@
/* run.config*
STDOPT: +"-deterministic -eva-no-memexec -eva-slevel-function init:3,main1:3,f2:4,main2:4,f4:3,main5:3,uninit:2,main9:2 -eva-split-return-function f2:0,f3:-2:-4,f4:4,f5:-2,NON_EXISTING:4,uninit:0,escaping:0 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -permissive -then -load-module report -report"
STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return auto -eva-split-return-function f7:0:3 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -load-module report -report"
+ EXIT:1
COMMENT: below command must fail, as -permissive is not set
STDOPT: +"-deterministic -eva-no-memexec -eva -eva-slevel-function NON_EXISTING:4 -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
+ EXIT:0
STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9"
STDOPT: +"-deterministic -eva-no-memexec -eva -journal-disable -out -input -deps -eva-slevel 6 -eva-split-return full -eva-split-return-function f7:0:3 -eva-split-return-function f2:full -eva-warn-copy-indeterminate=-uninit,-escaping,-main9 -then -eva-split-return-function f2:auto"
*/
+
/*@ assigns \result \from \nothing;
assigns *p \from \nothing;
ensures \result == 0 && \initialized(p) || \result == 1; */
diff --git a/tests/value/unknown_sizeof.i b/tests/value/unknown_sizeof.i
index f3a1c3c0c65..94e88f03ca2 100644
--- a/tests/value/unknown_sizeof.i
+++ b/tests/value/unknown_sizeof.i
@@ -1,8 +1,8 @@
/* run.config*
+ EXIT: 1
OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main1
OPT: -no-autoload-plugins -load-module eva -eva @EVA_CONFIG@ -main main2
*/
-
struct s;
struct s s;
diff --git a/tests/value/use_spec.i b/tests/value/use_spec.i
index b22673b3052..3097dcc25cb 100644
--- a/tests/value/use_spec.i
+++ b/tests/value/use_spec.i
@@ -1,9 +1,9 @@
/* run.config*
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
- OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
+ EXIT: 1
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps
+ OPT: -no-autoload-plugins -load-module from,inout,eva -eva-use-spec f,h -eva @EVA_CONFIG@ -inout -calldeps -show-indirect-deps
*/
-
void f(int *x) {
}
diff --git a/tests/value/va_list.c b/tests/value/va_list.c
index 431e9a600ed..374d236b163 100644
--- a/tests/value/va_list.c
+++ b/tests/value/va_list.c
@@ -1,6 +1,7 @@
-/*run.config*
- STDOPT:
- STDOPT: #"-variadic-no-translation"
+/* run.config*
+ STDOPT:
+ EXIT: 1
+ STDOPT: #"-variadic-no-translation"
*/
typedef void *va_list;
--
GitLab