diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config index ea6b5a9baba37bad36183027957b04a4ec702360..5c86b86909aa52ceb5c4981128a8c6ea9defc2b0 100644 --- a/src/plugins/wp/tests/ptests_config +++ b/src/plugins/wp/tests/ptests_config @@ -2,7 +2,7 @@ DEFAULT_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip # todo: to fixes -IGNORE= DEFAULT_SUITES= wp_region +DEFAULT_SUITES= wp_region IGNORE= qualif_SUITES= wp wp_plugin wp_acsl wp_bts wp_store wp_hoare IGNORE= qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip wp_region diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config index d2802e471188bf3bc9465d31d93e170cba8a687b..cc353c1a3769ff673c1dad9a0e92ad473d5e41b5 100644 --- a/src/plugins/wp/tests/wp_region/test_config +++ b/src/plugins/wp/tests/wp_region/test_config @@ -1,13 +1,3 @@ -<<<<<<< HEAD CMD: @frama-c@ @OPTIONS@ #LOG: @PTEST_NAME@/region/job.dot OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_NAME@ -wp-fct job -||||||| ac7807782d -CMD: @frama-c@ -no-autoload-plugins -load-module wp -LOG: @PTEST_NAME@/region/job.dot -OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job -======= -CMD: @frama-c@ -no-autoload-plugins -load-module wp -LOG: @PTEST_NAME@/region/job.dot -OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job ->>>>>>> origin/master diff --git a/tests/pdg/globals.c b/tests/pdg/globals.c index 390e3f947b760072a8ac520c6c617e20483410eb..295b43bb0a0f846d276d872bad508ef5d4ff3f20 100644 --- a/tests/pdg/globals.c +++ b/tests/pdg/globals.c @@ -1,8 +1,8 @@ /* run.config - - STDOPT: #"-load-module pdg -eva -out -input -deps -main g" - STDOPT: #"-load-module pdg -eva -out -input -deps -main h" - STDOPT: #"-load-module pdg -eva -out -input -deps -main f" + + STDOPT: #"-eva -out -input -deps -main g" + STDOPT: #"-eva -out -input -deps -main h" + STDOPT: #"-eva -out -input -deps -main f" */ struct Tstr; extern int X; diff --git a/tests/pdg/top_pdg_input.c b/tests/pdg/top_pdg_input.c index 1fa9bc5856422277ce593946c82f6b026885afe5..f0414696dc945a899e01bacc2b1a7e6368ba928e 100644 --- a/tests/pdg/top_pdg_input.c +++ b/tests/pdg/top_pdg_input.c @@ -1,5 +1,5 @@ /* run.config - STDOPT: +"-eva -pdg -out -input -deps -eva-no-results-function no_results -eva-no-builtins-auto -load-module pdg -pdg -then -main main_asm" + STDOPT: +"-eva -pdg -out -input -deps -eva-no-results-function no_results -eva-no-builtins-auto -pdg -then -main main_asm" */ volatile int nondet; int no_results() {return 1;}