From b51847a44bcae22e28081a64f4805276c6745d11 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Wed, 21 Aug 2019 10:32:30 +0200 Subject: [PATCH] [wp/region] fix test config - do not generate annotations (yet, but keep oracles in repo) - don't ask for any prover (for OCI) --- src/plugins/wp/tests/wp_region/oracle/array1.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array2.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array3.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array4.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array5.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array6.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array7.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/array8.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/index.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle | 2 -- src/plugins/wp/tests/wp_region/oracle/swap.res.oracle | 2 -- src/plugins/wp/tests/wp_region/test_config | 2 +- src/plugins/wp/tests/wp_region/test_config_qualif | 3 +++ 20 files changed, 4 insertions(+), 37 deletions(-) create mode 100644 src/plugins/wp/tests/wp_region/test_config_qualif 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 bc98fdb557e..4987dd9ae45 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 702b2b8d789..b724073ea5e 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 6d77c231beb..fa7682e2118 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 034940b5670..f39da987941 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 7bb376d9c70..5a0a75703bf 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 6ae597193b1..da6ccf4e0f1 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 7b9b959a2f9..cb757d81d87 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 f2f3f888c9f..83dd9d42382 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 1bd2257db58..2331b4aae96 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 61b99441d80..ec1a0b83feb 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 1efa44fbed9..13973473a67 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 f6f6d2b7ee1..834049467cb 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 6220dc1c238..fe737f1db75 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 b5bc831819b..eac3247d2ca 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 6afa63b87f6..178fe6a8980 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 2047a44db18..1d4865e408e 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 38f66682b6a..2bc45be7e59 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 32bd81a4e9f..d7076d6dbc8 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 a6597292345..36003c91eef 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 00000000000..b9325b65263 --- /dev/null +++ b/src/plugins/wp/tests/wp_region/test_config_qualif @@ -0,0 +1,3 @@ +DONTRUN: + +//OPT: -wp-region -- GitLab