diff --git a/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle index bc98fdb557e3a350c7a4802c79ed6debedbbce59..4987dd9ae45263a17a6338e3a4cb844be4876e93 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array1/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle index 702b2b8d789d09dc59149976a92a8f98b97bb6d8..b724073ea5e6c6a7fac7738b6d831e6fc1e177ca 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array2/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle index 6d77c231beb2341e3a09658085070704e21c235a..fa7682e21183bf98f749787a3ecde94f7c1b3ce3 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array3/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle index 034940b56709622e5fc09109abbbeea465d4c742..f39da987941e0ffab9390a9e6e5329dcc2a9dde6 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array4/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle index 7bb376d9c70b63b6e95ec9ea92d68bcefe821012..5a0a75703bf70121d5cebd897d7699c9d6a6ac96 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array5/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle index 6ae597193b16031bdf51bee9d44d3f2961c365c0..da6ccf4e0f1e820a4d240e64df242b33930b7278 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array6/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle index 7b9b959a2f989ece7374f0d5d9de4101bedac3c5..cb757d81d87267e4a38812b6cb8762f8489e6848 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array7/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle index f2f3f888c9fb149d92730fed2f0418c3a69aa933..83dd9d4238255784aba7772b3e57fb754865ad16 100644 --- a/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/array8/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle b/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle index 1bd2257db5862630de3c20f120d5ccfd093c4702..2331b4aae9657c583924d185d3f0c3fb0a9b0bc8 100644 --- a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/fb_ADD/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle b/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle index 61b99441d804a52a4ec1cf4ddad2c28c2dc412f0..ec1a0b83feb62c26278e26829c9a50d83687ef97 100644 --- a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/fb_SORT/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle index 1efa44fbed950e4c5a4f484670bc6e47929a9681..13973473a6739603448758d6940000363173431e 100644 --- a/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle @@ -5,5 +5,3 @@ [wp] Region Graph: tests/wp_region/result/garbled/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle/index.res.oracle index f6f6d2b7ee11c9b0059f09574af6ceae37dc70f3..834049467cbde15d83aba42c883878baaa71ed0f 100644 --- a/src/plugins/wp/tests/wp_region/oracle/index.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/index.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/index/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle index 6220dc1c2384dd82dcf11d464fb873558362c2cd..fe737f1db75548cc56518bebf54a18bc070f442f 100644 --- a/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/matrix/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle index b5bc831819bf35c116e82e1e674160b9e3b1c050..eac3247d2ca75c18f6bdb8de8851ca83750f7ac4 100644 --- a/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/structarray1/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle index 6afa63b87f63c482865b3b7dd77214fa338bab35..178fe6a89808245f88bbd916e648129d57347505 100644 --- a/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/structarray2/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle index 2047a44db1815c1b96b847f0d3409f2ad847f39e..1d4865e408e6511794022d8846142fd16724b46e 100644 --- a/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/structarray3/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle index 38f66682b6a5561322b3d0209f82de21ae6205ca..2bc45be7e59d5d04cc65b58b30e9b86dea76af19 100644 --- a/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/structarray4/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle index 32bd81a4e9f616afa36e651981809122e864e55a..d7076d6dbc8cb0e241490c9707bd7bc5470ba1e7 100644 --- a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle +++ b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle @@ -2,5 +2,3 @@ [wp] Region Graph: tests/wp_region/result/swap/region/job.dot [wp] Running WP plugin... [wp] Warning: Missing RTE guards -[wp] 0 goal scheduled -[wp] Proved goals: 0 / 0 diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config index a6597292345aad67d889bbc6c2f8b095e0c5f247..36003c91eeff9b752b08515c756f5e0268465e56 100644 --- a/src/plugins/wp/tests/wp_region/test_config +++ b/src/plugins/wp/tests/wp_region/test_config @@ -1,3 +1,3 @@ CMD: @frama-c@ -no-autoload-plugins -load-module wp LOG: @PTEST_NAME@/region/job.dot -OPT: -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job +OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-out @PTEST_DIR@/result/@PTEST_NAME@ -wp-fct job diff --git a/src/plugins/wp/tests/wp_region/test_config_qualif b/src/plugins/wp/tests/wp_region/test_config_qualif new file mode 100644 index 0000000000000000000000000000000000000000..b9325b65263f57a6624419148942cbf23bc78a2b --- /dev/null +++ b/src/plugins/wp/tests/wp_region/test_config_qualif @@ -0,0 +1,3 @@ +DONTRUN: + +//OPT: -wp-region