diff --git a/src/plugins/aorai/tests/ya/metavariables-incompatible.i b/src/plugins/aorai/tests/ya/metavariables-incompatible.i index a32cefe9e95a077a549e747e0231200ad48c4a5b..ac025ee303230685e01374351f91c3365307ff76 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 a0542d200213bae00dd447ca74e59ef7a0c15f08..febfd16cb34647a707de1a733cc9e0e9afd9fd5b 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 4a88230c1c71bc1958ba3a68ca1a473d28633b66..baa7b42e03eacd67ca4225cae17413023786a2e0 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 3ee8df0b80ad14afc530a3013f7067df128c4ec8..59d10572d66174086765df608e8473c6ad2c2f62 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 975369e8966a949daaa79f906923989730a7e8ce..4c1e7b1b838700580f438bdcd4ca35bc4db693d9 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..1a0a6550cd22661cdae17a41fdd59cc8e2709201 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 ae11c2ab9c3e6b443d5982de2d3828014b67032d..d91685eee5b954a2e5b5f49d2e9005bc13041805 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 cd27daffa3812428ce9caffd34acbbd85452dce8..324731fc34133cbf5870e6560c82ad6540973f8f 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 26a22e680ed203ec41a36414d3d05ef7031727b0..160fba1f823fe062c4a7c82eac125cb52f8ca4ab 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 23dd4015e0ad6e92796e03727e1584afa5ba4c95..3d6a5d4db64c3f03744f1665e98cd16512063052 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 9309a4ad71c5e73869a74c107b3a3a10a8f5a220..a524540296fcd5e051e3a7bfea1d16a943a622ea 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 49a5668900890b3f57d4fb6bd3511ab5fa468efc..80551c782227b4a090236e58b1af57092dc93739 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 bf3c37795c39da683ba40f21b9901346cb16cba4..8b92eb451c8e6380cb8a26406ceb6d024a81e8b1 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 6da1b3de795fc4d046e4b209a8e8375622c3fcf2..a4a656fc9af4cb1e935ddf18a0d208f5f0520534 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 15c916efa382d7875e227e39535ef8d6b8201d4d..13b1504560e361161668c1012b0a1e29c9398b43 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 8e02226c49c93c5010f6f1c46dfd32bcd981f8a5..bd261320029fac9ba2668b8f966066eb7b783dd4 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 02c2288f0d43870369ee3879649645b9ee781831..4ba9f9768c54c472c2c59c31e045094ca301cdf9 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 5edc84415b34d37ecf5d58eede9944337ac64876..84c8e1f479d6e530dff7066196fd1050826ae880 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 f7a377dc16250f21911dbc5f014d7a50b33bac3f..87979f0608b990d948997b250a3862bf51d98c48 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 5646776c8be6e08df7545b9b872b067995932fa5..6b4a7dbc2c393c816be2d930b7eb81d6d0deb33a 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 a8892bc2d2feb203e5bef30c636a78b7d481c254..40748281b882ec47152214f8f72222330294a30b 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 4a8970e7f7be6739539dea5ab91c2166b8058df0..1f4b218d0bfd2f02b8e5d3e152eb1177fb4ddf75 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 723aa9d837ec43a7084c4d68f4d3e6842b113bad..b48ddbd09f7be85d24a13b2f581addd5a8a8fbae 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 0ce6903f296b3baeab13bcbe57a70ff5941cb20b..333304c449f7728babafb3871439aa92bae480a3 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 1a71bc26d2059a21a33ba7763b97a2f58d686020..36558b8808f5835948fe3bbe775dda0db517ad39 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 08fe31aa7b67c33420527175fdcfeeedce5ac8b6..348015c7c228d43d8c167ed1572f48c9ebd7e94b 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 f65505058bbf38d898556e25d04c0ff4d7b3ee35..e7a647f6e453e88b9a63b844539f12d718e9cfbe 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 e4f063807c12972b188952fa735a10024d17c844..fca1b6e7e6ef953b698c6d2fa04bee2193bd889c 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 473facee9adb8ed5679c1669cb885f9bd3ac60b0..942e22769090299b995e4dc7faa2d941d907a4f3 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 2638caa2c263c98c9f1218f475940b126c46bad9..7d67b5393d7c32fe09ed205556f754cc1d35aba6 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 d0e4e03c2d8a867f6b47d5ca5cb8ae06d7200c1e..7f17b62b70041b3ef24187b91e6bb1b421f8ee47 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 636b1969432ac2f2e9e91c3c402047ebaaeca97e..39ae9a0e8decaaf47eb20c98f3542432824304fb 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 11f210ed5687266e77d9d1496047271aa504a1cb..e8d46d0178a748a46145d63601c3f5ba9b1711af 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 fce725aabdbdcd8123cc175649b0a1ba8085dda8..217425c9ef46a3cd5259ed0cf5011ea6dc6ddc16 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 6265f34c06d9d846a05443143d0b3224467616b0..9ccba084dc28c5ffad18f5fc9271e085d78a2637 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 9c1713103718b6783fb7201693001013f1d0dccb..41a8ff2c7bbca2cf5a34cd9f1f58f2b574f0c04c 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 fe5fdb97b7baeb77a61c6b1f96f9ea6daa657e50..78b17597c868f218ae7b413305444a3fdac3d225 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 d15f0eaccacb1abdb6bf90ce063efe293b1e0c01..ad9f60245808fff6c5f62bb12d0641e44e962a7b 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 b823ffdf4a1ca5ad657d491848a0aa9a2a5f43fe..57cf567357e69d0515392300318d6da13f8476d0 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 a04efd9d97b8ad4e04976731daa7f67790e212f4..745a67aa56aac5491708a37f4d6e282f1f5c2723 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 4d87d6db6e95dc75524c12825ba789a1a460b7a4..0182c652f28ae765761c09b543d026b4d8825046 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 b91d73a95809d3becec6f93f547aa8d10d45f0b8..c7239abee35c9bf1ec8290756d59550555d78307 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 62ebdab3e24b225226ed31ca6ca17e0cdd50b33f..5db7343892aa72873391759ae652ae7741757bbd 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 eab5dccd0c3e11ce97ad2511ab92beaeb96bc405..9cda9f447e30a8954c162a855682b6f1438989b7 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 4baf088c14f4a8baeba250ad8f2abe33a2b79766..59fca4bf3473d5dfbbfd5f25f12bfa1d6407330f 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 e84cce94b9891a77d85135a75691d9f9b7ad1b87..99e25916b20d422ff84b622d9d269d91f865d671 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 a0339194afe9def80ec7aeba80647ec0e8084981..35dbe5c3064ecbaa0312c532641dab5c25148b19 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 0de775a8e056e17559429eedc7ef5d26feb12bab..e75186e231c116379b922093101c28ba321fbdfa 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 a4e082cc80821e0c384ace856b36df57d72fd94c..f2729c2ea244c8b64e324d2f56252acc9a3394ad 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 55637c2cad56e520c48cb7c9f151a040bab5df24..08ecf3c1bc55182919c315baf9de600eb8af743b 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 6a8f1922b9870d826dfcddb54638ba9386401f1d..180192d7e258b1efa56107d775a19ae042dfee5b 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 0fad3b59986a0a65ad22b21b9f9b170ed348b49e..151b38dcf8e709e60526bc0007a7ff27084f603b 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 d78f5e54a4db97deda334fa64c48c5f8ca5fa827..a7cd33e3341ee64f40642879d1024d7faccabd32 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 d3d786b2880f1a69d94a0826f3379c43ea25f692..5492f24a3afd0b94de7c5eacddbece339a2f51c2 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 2d7d07969208ef53f72ba186c349da56847da008..efa2a0566c5c0ff718cb6c4b321f7823f6871131 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 b1caed2316819fca7f5298378248efc7d71dc111..db9dce1ccf5d5c0cef88ace49215b5aaef7bfdfc 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 66371e18b3a593d348c816860bcb5fa6487964ce..1eed4134ecaf36c365f8eb6a93e6f4fa6324949d 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 b2e82193a255f81a5cb5d92fca3505e85c2a25c5..3ec41da4ee6c62d1b52963e484ae50dc5de8dcb0 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 c9e20e50f123c38e78e82a8951d888ae938d5a43..ed81a5d3f691655f19f5e75ef1518848163c597c 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 0c7901651cf0b9ef6d4ea0310ed368298920c203..c4cb37aa00a73bc53063c83f98aee526abe69a9e 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 8a3aa44011c7c8c8bfa1693b57631cdc8f5b5f1a..231b0c1123f057a3607a57915af9f32a59427d46 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 afe1a02aade80108befaf96b1ec51da84f58a0d5..ddfa14d70527313d30b9148bd25e9b50fcf14a99 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 5f429de862630c8597a556e77917bc234a7caee0..5db196f78807bd979ee203250189ffe2c5b03154 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 97e763362e2dc653cce9d347c2db419585668762..c3535c628d2dd9e33f5e1d853bd3f262d1e4cc0c 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 39840bd6cf94033d0872192b63d32252fce8de53..a0de92104f81c6049e600ee4534200742c76b21c 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 71d62ce185b07cede4befcbde1fd0c358cb75e7a..ef3528b0d15513a1ec11b866e6a4bd481b0fb74f 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 b7233c675d0c28cc82f633f8403f6b7040571f2e..d8a15d22f663965e8bdd03effb49ed31d5b71b1d 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 d20a1dfcda46f0720ce70523677b4472dd709f80..1d1d9d7eb516dc6444cf9a41f12ac23d8081b774 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 6a0a25687f9e2960e533cbec4ac5dbc0dc21e286..fb2cf140850349af5468b540e848f847d4d1852c 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 7d4f460b375b9de4e54c977d4dd8496d64097f2b..2aed6a096ca712545ed09256856a533a7b9d0b14 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 47d289de12e57a13d96629b6affb868a2fa886e3..a0185f6bcfcd32ca452e2f2de948dc8ef42cf24f 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 d100d64669cd8bb838c46411582829eba7e52ee6..1dde8a89eb9d16db31800408f4643807af985f35 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 df437409f8d4e9370eb5c5b95ae9c8238a608e5c..c95988c278fdcb8bc7a99a76e66c264b087859bb 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 64b91652f8cd9ffac41956083b3af7fdb4bb2b8a..371b1c0c91df2d568cf7b6fb90488f58c86d1d8e 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 25e660061ae915c6ea0f0fc095cd272b99ead99b..6c3f823224025594551a55c475f73592c09651a7 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 b532103ecd1513b5c73fb7ebc7e1fd347616cf4b..c522453305f94cfd11edab28d158226619f875f7 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 d887e89667ec5464d71f2d68e749dfe68465f196..0b5e7a8bf6a82be6b854c63f410644568489c687 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 31f1929c13f1f1de53c75f430f3b242bb998bd06..2e1f1903a2ebfd90b8831ec66ddd44f8c93caedf 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 28d719f063809920a5154b132e156ec2b7a78f05..2c56c35150bac395c2cbd72c1479e474c39ce1d8 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 60dd7dd9effbef4de3743659d39d20ecfe4d40c5..9e7dd5eb589611b6a55ac8c44db1f858db12f9a7 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 302e682dfe5f90c52b8bfb4c69fc8b3a60f36250..5286293ce2cf41e971a087e1f083f3b43c6e6fee 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 7f760f860d66bb3e85c187ec6dd38a411b5d412f..f7e7f87cd91ad794f3ac60402aef329f982b4206 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 53ffedf53814469ef1c76dcd7caeffdbce744189..28949ee17ff379336649b432fddadcbfc0300f9d 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 3e163f3bb8227dafc50fa189d2842831938ebf39..58b86079ef72bd6ce70d2a359285b8b69fcbd42b 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 afa7dd0affc9fe027771ce5e87ad5bd0a44a3ed6..7d8222ecd80f8ee059c53be214476bf99df83db5 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 f4a14535232ca14a6f0ea5fb00d4009aa6d75018..d5eb9df2e066dd1f16b6877b64e5327680811e9a 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 da2a59b86aef70d1ce5cf3732635f24f7f810883..04dd59e8d9812164134e645abb46363357c37526 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 90e1020b409d79ace1a1904892f8cba0dee9e883..bbde72ccbddd89b0d5731b2b7652d5e59960d18b 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 f84a4ebf84a90dfca79e584bfc02975497a704cf..98d5d3527c9c68817323dbc5cd45ac47a16e355a 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 1a5baf64c3b8456b030aee0bebc15c0b9cf9ca9f..d51b1b0f4864495a7393dea6ceebd86b3cd0d178 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 2b916a17354f17b3e39f216477a7343128c08a36..c3670163290ec5e0d912bff2106bc72a63fc1466 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 8cfc8a21a7528455accae9f91f3678fc12e51767..df9fbcbdada17c3366d1da87a6b948f454b8129e 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 f3a1c3c0c65e3ed31968b58d4531746eba71b228..94e88f03ca2aaa60f0b99312ef0a1c2dbc9868b0 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 b22673b3052ae0dc65f6d85e38de74b386760165..3097dcc25cb54367cd22fe2bc77aa23d5cfea43c 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 431e9a600ed7bc3239e368efaf8b8df29cc628b3..374d236b163780ee612f7d470a45e6c351f6a8b1 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;