From fb7ababa80187e36222cdb6563ca21e6f3d91f5c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr> Date: Thu, 22 Aug 2024 09:22:19 +0200 Subject: [PATCH] [wp] remove memRegion testing --- src/plugins/wp/tests/wp_region/README.md | 13 -- src/plugins/wp/tests/wp_region/annot.i | 66 ------ src/plugins/wp/tests/wp_region/annot/a.i | 58 ----- src/plugins/wp/tests/wp_region/annot/b.i | 58 ----- src/plugins/wp/tests/wp_region/array1.i | 8 - src/plugins/wp/tests/wp_region/array2.i | 8 - src/plugins/wp/tests/wp_region/array3.i | 6 - src/plugins/wp/tests/wp_region/array4.i | 7 - src/plugins/wp/tests/wp_region/array5.i | 7 - src/plugins/wp/tests/wp_region/array6.i | 9 - src/plugins/wp/tests/wp_region/array7.i | 10 - src/plugins/wp/tests/wp_region/array8.i | 10 - src/plugins/wp/tests/wp_region/fb_ADD.i | 25 --- src/plugins/wp/tests/wp_region/fb_SORT.i | 44 ---- src/plugins/wp/tests/wp_region/fc.sh | 109 ---------- src/plugins/wp/tests/wp_region/garbled.i | 6 - src/plugins/wp/tests/wp_region/index.i | 6 - src/plugins/wp/tests/wp_region/matrix.i | 8 - .../tests/wp_region/oracle/annot.res.oracle | 59 ----- .../wp/tests/wp_region/oracle/array1.0.dot | 57 ----- .../tests/wp_region/oracle/array1.res.oracle | 4 - .../wp/tests/wp_region/oracle/array2.0.dot | 63 ------ .../tests/wp_region/oracle/array2.res.oracle | 4 - .../wp/tests/wp_region/oracle/array3.0.dot | 33 --- .../tests/wp_region/oracle/array3.res.oracle | 4 - .../wp/tests/wp_region/oracle/array4.0.dot | 41 ---- .../tests/wp_region/oracle/array4.res.oracle | 4 - .../wp/tests/wp_region/oracle/array5.0.dot | 49 ----- .../tests/wp_region/oracle/array5.res.oracle | 4 - .../wp/tests/wp_region/oracle/array6.0.dot | 41 ---- .../tests/wp_region/oracle/array6.res.oracle | 4 - .../wp/tests/wp_region/oracle/array7.0.dot | 47 ---- .../tests/wp_region/oracle/array7.res.oracle | 4 - .../wp/tests/wp_region/oracle/array8.0.dot | 58 ----- .../tests/wp_region/oracle/array8.res.oracle | 4 - .../wp/tests/wp_region/oracle/diff_annot.txt | 0 .../wp/tests/wp_region/oracle/fb_ADD.0.dot | 95 -------- .../tests/wp_region/oracle/fb_ADD.res.oracle | 4 - .../wp/tests/wp_region/oracle/fb_SORT.0.dot | 204 ------------------ .../tests/wp_region/oracle/fb_SORT.res.oracle | 4 - .../wp/tests/wp_region/oracle/garbled.0.dot | 48 ----- .../tests/wp_region/oracle/garbled.res.oracle | 7 - .../wp/tests/wp_region/oracle/index.0.dot | 57 ----- .../tests/wp_region/oracle/index.res.oracle | 4 - .../wp/tests/wp_region/oracle/matrix.0.dot | 93 -------- .../tests/wp_region/oracle/matrix.res.oracle | 4 - .../tests/wp_region/oracle/structarray1.0.dot | 70 ------ .../wp_region/oracle/structarray1.res.oracle | 4 - .../tests/wp_region/oracle/structarray2.0.dot | 97 --------- .../wp_region/oracle/structarray2.res.oracle | 4 - .../tests/wp_region/oracle/structarray3.0.dot | 114 ---------- .../wp_region/oracle/structarray3.res.oracle | 4 - .../tests/wp_region/oracle/structarray4.0.dot | 110 ---------- .../wp_region/oracle/structarray4.res.oracle | 4 - .../wp/tests/wp_region/oracle/swap.0.dot | 40 ---- .../wp/tests/wp_region/oracle/swap.res.oracle | 4 - .../wp_region/oracle_qualif/array1.res.oracle | 6 - .../wp_region/oracle_qualif/array2.res.oracle | 6 - .../wp_region/oracle_qualif/array3.res.oracle | 6 - .../wp_region/oracle_qualif/array4.res.oracle | 6 - .../wp_region/oracle_qualif/array5.res.oracle | 6 - .../wp_region/oracle_qualif/array6.res.oracle | 6 - .../wp_region/oracle_qualif/array7.res.oracle | 6 - .../wp_region/oracle_qualif/array8.res.oracle | 6 - .../wp_region/oracle_qualif/fb_ADD.res.oracle | 6 - .../oracle_qualif/fb_SORT.res.oracle | 6 - .../oracle_qualif/garbled.res.oracle | 6 - .../wp_region/oracle_qualif/index.res.oracle | 6 - .../wp_region/oracle_qualif/matrix.res.oracle | 6 - .../oracle_qualif/structarray1.res.oracle | 6 - .../oracle_qualif/structarray2.res.oracle | 6 - .../oracle_qualif/structarray3.res.oracle | 6 - .../oracle_qualif/structarray4.res.oracle | 6 - .../wp_region/oracle_qualif/swap.res.oracle | 6 - src/plugins/wp/tests/wp_region/structarray1.i | 18 -- src/plugins/wp/tests/wp_region/structarray2.i | 18 -- src/plugins/wp/tests/wp_region/structarray3.i | 18 -- src/plugins/wp/tests/wp_region/structarray4.i | 20 -- src/plugins/wp/tests/wp_region/swap.i | 8 - src/plugins/wp/tests/wp_region/test_config | 4 - .../wp/tests/wp_region/test_config_qualif | 1 - 81 files changed, 2104 deletions(-) delete mode 100644 src/plugins/wp/tests/wp_region/README.md delete mode 100644 src/plugins/wp/tests/wp_region/annot.i delete mode 100644 src/plugins/wp/tests/wp_region/annot/a.i delete mode 100644 src/plugins/wp/tests/wp_region/annot/b.i delete mode 100644 src/plugins/wp/tests/wp_region/array1.i delete mode 100644 src/plugins/wp/tests/wp_region/array2.i delete mode 100644 src/plugins/wp/tests/wp_region/array3.i delete mode 100644 src/plugins/wp/tests/wp_region/array4.i delete mode 100644 src/plugins/wp/tests/wp_region/array5.i delete mode 100644 src/plugins/wp/tests/wp_region/array6.i delete mode 100644 src/plugins/wp/tests/wp_region/array7.i delete mode 100644 src/plugins/wp/tests/wp_region/array8.i delete mode 100644 src/plugins/wp/tests/wp_region/fb_ADD.i delete mode 100644 src/plugins/wp/tests/wp_region/fb_SORT.i delete mode 100755 src/plugins/wp/tests/wp_region/fc.sh delete mode 100644 src/plugins/wp/tests/wp_region/garbled.i delete mode 100644 src/plugins/wp/tests/wp_region/index.i delete mode 100644 src/plugins/wp/tests/wp_region/matrix.i delete mode 100644 src/plugins/wp/tests/wp_region/oracle/annot.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array1.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array1.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array2.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array2.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array3.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array3.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array4.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array4.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array5.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array5.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array6.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array6.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array7.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array7.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array8.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/array8.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/diff_annot.txt delete mode 100644 src/plugins/wp/tests/wp_region/oracle/fb_ADD.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/fb_SORT.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/garbled.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/index.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/index.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/matrix.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray1.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray2.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray3.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray4.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle/swap.0.dot delete mode 100644 src/plugins/wp/tests/wp_region/oracle/swap.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle delete mode 100644 src/plugins/wp/tests/wp_region/structarray1.i delete mode 100644 src/plugins/wp/tests/wp_region/structarray2.i delete mode 100644 src/plugins/wp/tests/wp_region/structarray3.i delete mode 100644 src/plugins/wp/tests/wp_region/structarray4.i delete mode 100644 src/plugins/wp/tests/wp_region/swap.i delete mode 100644 src/plugins/wp/tests/wp_region/test_config delete mode 100644 src/plugins/wp/tests/wp_region/test_config_qualif diff --git a/src/plugins/wp/tests/wp_region/README.md b/src/plugins/wp/tests/wp_region/README.md deleted file mode 100644 index 54aa9413764..00000000000 --- a/src/plugins/wp/tests/wp_region/README.md +++ /dev/null @@ -1,13 +0,0 @@ -# Testing WP/Region - -Use `./fc.sh -h|--help` to visualize the output before commiting changes. - -# Recommanded workflow - -With default configuration, put a single 'job' function in each test file. -Then: - -1. Run `./fc.sh test.i -r` to visualize the region graph and check the proofs -2. Run `./fc.sh test.i -u` to update the region-graph oracle (creates also the oracle directories) -3. Run `./fc.sh test.i -t` to check test is OK (eventually use `-t -show` or `-t -update`) -4. Run `./fc.sh test.i -q` to check qualif test is OK diff --git a/src/plugins/wp/tests/wp_region/annot.i b/src/plugins/wp/tests/wp_region/annot.i deleted file mode 100644 index 2312dafd8a4..00000000000 --- a/src/plugins/wp/tests/wp_region/annot.i +++ /dev/null @@ -1,66 +0,0 @@ -/* run.config - PLUGIN: wp - OPT: -region-annot -print -generated-spec-mode skip - EXECNOW: BIN ocode_@PTEST_NAME@_1.i @frama-c@ %{dep:@PTEST_DIR@/@PTEST_NAME@.i} -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_1.i > @DEV_NULL@ 2> @DEV_NULL@ - EXECNOW: BIN ocode_@PTEST_NAME@_2.i @frama-c@ %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} -region-annot -print -ocode @PTEST_RESULT@/ocode_@PTEST_NAME@_2.i > @DEV_NULL@ 2> @DEV_NULL@ - EXECNOW: LOG diff_@PTEST_NAME@.txt diff %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_1.i} %{dep:@PTEST_RESULT@/ocode_@PTEST_NAME@_2.i} &> @PTEST_RESULT@/diff_@PTEST_NAME@.txt -COMMENT: The file diff_@PTEST_NAME@.txt must be empty. -COMMENT: So, that file has not to be present into the oracle directory since absent files are considered such as empty files. - */ - -/* run.config_qualif - DONTRUN: -*/ - -// This test only checks that annotation are correctly parsed & printed - -typedef struct N { double v ; int s ; } *SN ; -typedef struct L { int v ; int s ; } *SL ; - -typedef struct Block { - SN prm ; - SN inp1 ; - SN inp2 ; - SN inp3 ; - SN out1 ; - SN out2 ; - SN out3 ; - SL idx1 ; - SL idx2 ; - SL idx3 ; - SN sum ; -} FB ; - -//@ \wp::wpregion *fb ; -void fb_ADD(FB *fb) -{ - fb->out1->v = fb->out1->v + fb->out2->v ; - fb->out1->s = fb->out1->s | fb->out2->s ; -} - -/*@ - \wp::wpregion IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ; - \wp::wpregion OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ; - \wp::wpregion IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ; - */ -void fb_SORT(FB *fb) -{ - SN *inp = &(fb->inp1) ; - SN *out = &(fb->out1) ; - SL *idx = &(fb->idx1) ; - - for (int i = 0; i < 3; i++) { - out[i]->v = inp[i]->v + fb->prm->v ; - out[i]->s = 0 ; - idx[i]->v = inp[i]->s ; - idx[i]->s = 0 ; - } - - fb->sum->v = - fb->out1->v + - fb->out2->v + - fb->out3->v ; - - fb->sum->s = 0 ; - -} diff --git a/src/plugins/wp/tests/wp_region/annot/a.i b/src/plugins/wp/tests/wp_region/annot/a.i deleted file mode 100644 index fb6d84c2cb8..00000000000 --- a/src/plugins/wp/tests/wp_region/annot/a.i +++ /dev/null @@ -1,58 +0,0 @@ -/* Generated by Frama-C */ -struct N { - double v ; - int s ; -}; -typedef struct N *SN; -struct L { - int v ; - int s ; -}; -typedef struct L *SL; -struct Block { - SN prm ; - SN inp1 ; - SN inp2 ; - SN inp3 ; - SN out1 ; - SN out2 ; - SN out3 ; - SL idx1 ; - SL idx2 ; - SL idx3 ; - SN sum ; -}; -typedef struct Block FB; -/*@ terminates \true; - \wp::wpregion *fb; */ -void fb_ADD(FB *fb) -{ - (fb->out1)->v += (fb->out2)->v; - (fb->out1)->s |= (fb->out2)->s; - return; -} - -/*@ terminates \true; - \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3); - \wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3); - \wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3); - */ -void fb_SORT(FB *fb) -{ - SN *inp = & fb->inp1; - SN *out = & fb->out1; - SL *idx = & fb->idx1; - { - int i = 0; - while (i < 3) { - (*(out + i))->v = (*(inp + i))->v + (fb->prm)->v; - (*(out + i))->s = 0; - (*(idx + i))->v = (*(inp + i))->s; - (*(idx + i))->s = 0; - i ++; - } - } - (fb->sum)->v = ((fb->out1)->v + (fb->out2)->v) + (fb->out3)->v; - (fb->sum)->s = 0; - return; -} diff --git a/src/plugins/wp/tests/wp_region/annot/b.i b/src/plugins/wp/tests/wp_region/annot/b.i deleted file mode 100644 index fb6d84c2cb8..00000000000 --- a/src/plugins/wp/tests/wp_region/annot/b.i +++ /dev/null @@ -1,58 +0,0 @@ -/* Generated by Frama-C */ -struct N { - double v ; - int s ; -}; -typedef struct N *SN; -struct L { - int v ; - int s ; -}; -typedef struct L *SL; -struct Block { - SN prm ; - SN inp1 ; - SN inp2 ; - SN inp3 ; - SN out1 ; - SN out2 ; - SN out3 ; - SL idx1 ; - SL idx2 ; - SL idx3 ; - SN sum ; -}; -typedef struct Block FB; -/*@ terminates \true; - \wp::wpregion *fb; */ -void fb_ADD(FB *fb) -{ - (fb->out1)->v += (fb->out2)->v; - (fb->out1)->s |= (fb->out2)->s; - return; -} - -/*@ terminates \true; - \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3); - \wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3); - \wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3); - */ -void fb_SORT(FB *fb) -{ - SN *inp = & fb->inp1; - SN *out = & fb->out1; - SL *idx = & fb->idx1; - { - int i = 0; - while (i < 3) { - (*(out + i))->v = (*(inp + i))->v + (fb->prm)->v; - (*(out + i))->s = 0; - (*(idx + i))->v = (*(inp + i))->s; - (*(idx + i))->s = 0; - i ++; - } - } - (fb->sum)->v = ((fb->out1)->v + (fb->out2)->v) + (fb->out3)->v; - (fb->sum)->s = 0; - return; -} diff --git a/src/plugins/wp/tests/wp_region/array1.i b/src/plugins/wp/tests/wp_region/array1.i deleted file mode 100644 index bf3da7a503c..00000000000 --- a/src/plugins/wp/tests/wp_region/array1.i +++ /dev/null @@ -1,8 +0,0 @@ -//@ \wp::wpregion *p, *q ; -int job( int n, int * p , int * q ) -{ - int s = 0 ; - for (int k = 0; k < n; k++) - s += p[k] * q[k] ; - return s ; -} diff --git a/src/plugins/wp/tests/wp_region/array2.i b/src/plugins/wp/tests/wp_region/array2.i deleted file mode 100644 index be59f8c030d..00000000000 --- a/src/plugins/wp/tests/wp_region/array2.i +++ /dev/null @@ -1,8 +0,0 @@ -//@ \wp::wpregion *p; \wp::wpregion *q ; -int job( int n, int * p , int * q ) -{ - int s = 0 ; - for (int k = 0; k < n; k++) - s += p[k] * q[k] ; - return s ; -} diff --git a/src/plugins/wp/tests/wp_region/array3.i b/src/plugins/wp/tests/wp_region/array3.i deleted file mode 100644 index 5035254bf8a..00000000000 --- a/src/plugins/wp/tests/wp_region/array3.i +++ /dev/null @@ -1,6 +0,0 @@ -int job( int * p ) -{ - int s = 0 ; - while (!*p) { s+=*p ; p++; } - return s; -} diff --git a/src/plugins/wp/tests/wp_region/array4.i b/src/plugins/wp/tests/wp_region/array4.i deleted file mode 100644 index bc3b3b68375..00000000000 --- a/src/plugins/wp/tests/wp_region/array4.i +++ /dev/null @@ -1,7 +0,0 @@ -int job( int * p ) -{ - int s = 0 ; - int *q = p ; - while (!*q) { s+=*q ; q++; } - return s; -} diff --git a/src/plugins/wp/tests/wp_region/array5.i b/src/plugins/wp/tests/wp_region/array5.i deleted file mode 100644 index 9fd9f2aa9f6..00000000000 --- a/src/plugins/wp/tests/wp_region/array5.i +++ /dev/null @@ -1,7 +0,0 @@ -int job( int * p , int * q ) -{ - int s = 0 ; - q = p ; - while (!*q) { s+=*p ; p[s]; q++; } - return s; -} diff --git a/src/plugins/wp/tests/wp_region/array6.i b/src/plugins/wp/tests/wp_region/array6.i deleted file mode 100644 index 8136a3c37b0..00000000000 --- a/src/plugins/wp/tests/wp_region/array6.i +++ /dev/null @@ -1,9 +0,0 @@ -int A[10] ; -int B[20] ; - -int job(int k) -{ - int s = 0 ; - while (!A[k]) { s += A[k]; k++; } - return s ; -} diff --git a/src/plugins/wp/tests/wp_region/array7.i b/src/plugins/wp/tests/wp_region/array7.i deleted file mode 100644 index 8178ba26808..00000000000 --- a/src/plugins/wp/tests/wp_region/array7.i +++ /dev/null @@ -1,10 +0,0 @@ -int A[10] ; -int B[20] ; - -int job(int k) -{ - int s = 0 ; - int * p = A+k ; - while (!*p) { s += *p; p++; } - return s ; -} diff --git a/src/plugins/wp/tests/wp_region/array8.i b/src/plugins/wp/tests/wp_region/array8.i deleted file mode 100644 index 2ded4d8661d..00000000000 --- a/src/plugins/wp/tests/wp_region/array8.i +++ /dev/null @@ -1,10 +0,0 @@ -int A[10] ; -int B[20] ; - -int job(int c,int k) -{ - int s = 0 ; - int * p = (c?A:B)+k ; - while (!*p) { s += *p; p++; } - return s ; -} diff --git a/src/plugins/wp/tests/wp_region/fb_ADD.i b/src/plugins/wp/tests/wp_region/fb_ADD.i deleted file mode 100644 index dc378f6d5e6..00000000000 --- a/src/plugins/wp/tests/wp_region/fb_ADD.i +++ /dev/null @@ -1,25 +0,0 @@ -typedef struct N { double v ; int s ; } *SN ; -typedef struct L { int v ; int s ; } *SL ; - -typedef struct Block { - SN prm ; - SN inp1 ; - SN inp2 ; - SN inp3 ; - SN out1 ; - SN out2 ; - SN out3 ; - SL idx1 ; - SL idx2 ; - SL idx3 ; - SN sum ; -} FB ; - -/*@ - \wp::wpregion A: fb ; -*/ -void job(FB *fb) -{ - fb->out1->v = fb->out1->v + fb->out2->v ; - fb->out1->s = fb->out1->s | fb->out2->s ; -} diff --git a/src/plugins/wp/tests/wp_region/fb_SORT.i b/src/plugins/wp/tests/wp_region/fb_SORT.i deleted file mode 100644 index 72629334e8a..00000000000 --- a/src/plugins/wp/tests/wp_region/fb_SORT.i +++ /dev/null @@ -1,44 +0,0 @@ -typedef struct N { double v ; int s ; } *SN ; -typedef struct L { int v ; int s ; } *SL ; - -typedef struct Block { - SN prm ; - SN inp1 ; - SN inp2 ; - SN inp3 ; - SN out1 ; - SN out2 ; - SN out3 ; - SL idx1 ; - SL idx2 ; - SL idx3 ; - SN sum ; -} FB ; - -/*@ - \wp::wpregion Shared: *(fb->inp1 .. fb->inp3); - \wp::wpregion IN: (fb->inp1 .. fb->inp3); - \wp::wpregion OUT: (fb->out1 .. fb->out3); - \wp::wpregion IDX: (fb->idx1 .. fb->idx3); - */ -void job(FB *fb) -{ - SN *inp = &(fb->inp1) ; - SN *out = &(fb->out1) ; - SL *idx = &(fb->idx1) ; - - for (int i = 0; i < 3; i++) { - out[i]->v = inp[i]->v + fb->prm->v ; - out[i]->s = 0 ; - idx[i]->v = inp[i]->s ; - idx[i]->s = 0 ; - } - - fb->sum->v = - fb->out1->v + - fb->out2->v + - fb->out3->v ; - - fb->sum->s = 0 ; - -} diff --git a/src/plugins/wp/tests/wp_region/fc.sh b/src/plugins/wp/tests/wp_region/fc.sh deleted file mode 100755 index f070fd5bb55..00000000000 --- a/src/plugins/wp/tests/wp_region/fc.sh +++ /dev/null @@ -1,109 +0,0 @@ -# Visualize output of WP/Region tests - -OPT= -CMD=fc -TEST="<none>" -NAME="none" -OPEN="none" -DEFAULT="-wp-msg-key dot,chunk,roots,garbled" - -if type open &> /dev/null ; then - OPEN=open -elif type xpdf &> /dev/null ; then - OPEN=xpdf -elif type evince &> /dev/null ; then - OPEN=evince -fi - -while [ "$1" != "" ]; -do - case $1 in - "-h"|"--help") - echo "fc.sh [options...] <test.[ic]>" ; - echo " -h,--help help and exit" ; - echo " -D,--delete clean output directory and exit" ; - echo " -g,--gui run in Frama-C Gui" ; - echo " -r,--region visualize region graph" ; - echo " -u,--update commit region graph in oracle" ; - echo " -t,--test run ptests.opt on test file (or all files)" ; - echo " -q,--qualif run ptests.opt with test-config qualif" ; - echo " --open <cmd> opens pdf with '<cmd>'" ; - echo " -k <keys> set message keys" ; - echo " * any other Frama-C options" ; - exit 0 ; - ;; - *.i) TEST=${1}; NAME=${TEST/.i/} ;; - *.c) TEST=${1}; NAME=${TEST/.c/} ;; - "-D"|"--delete") CMD=delete ;; - "-u"|"--update") CMD=update ;; - "-t"|"--test") CMD=test ;; - "-q"|"--qualif") CMD=qualif ;; - "-g"|"--gui") CMD=gui ;; - "-r"|"--region") CMD=region ; OPT="${OPT} -wp-msg-key pdf" ;; - "--open") shift ; CMD=region ; OPEN=${1} ;; - "-k") shift ; CMD=region ; DEFAULT="" ; OPT="${OPT} -wp-msg-key $1" ;; - *) - OPT="${OPT} $1" - ;; - esac - shift -done - -BIN=../../../../../bin -WP="-wp-region -wp-model Region -wp-fct job -wp-out result/${NAME}" - -case $CMD in - "fc"|"region") - echo "Running frama-c $TEST" - $BIN/frama-c $WP $TEST $DEFAULT $OPT - PDF="./result/${NAME}/region/job.pdf" - if [ $CMD = region ] && [ -f $PDF ] - then - if [ $OPEN != none ] ; then - echo "Source File:" - cat $TEST - $OPEN $PDF - else - echo "No command found for opening $PDF" - echo "Use --open <cmd> option" - fi - fi - ;; - "gui") - echo "Running frama-c $TEST (Gui)" - $BIN/frama-c-gui $WP $TEST $OPT - ;; - "test") - if [ $TEST == "<none>" ] - then - echo "Testing directory..." - ( cd ../.. ; ../../../bin/ptests.opt tests/wp_region > /dev/null ) - for test in *.i - do - name=${test/.i/} - oracle=oracle/$name/region/job.dot - result=result/$name/region/job.dot - if [ -f $oracle ] && !( diff -q $oracle $result > /dev/null ) - then - echo "Diff: ./fc.sh $test -r" - fi - done - else - echo "Testing $TEST$OPT" - ( cd ../.. ; ../../../bin/ptests.opt tests/wp_region/$TEST $OPT ) - fi - ;; - "qualif") - echo "Testing $TEST -config qualif$OPT" - ( cd ../.. ; ../../../bin/ptests.opt tests/wp_region/$TEST -config qualif $OPT ) - ;; - "update") - echo "Update './oracle/$NAME/region/job.dot" - mkdir -p ./oracle/$NAME/region - cp -f ./result/$NAME/region/job.dot ./oracle/$NAME/region/ - ;; - "delete") - echo "Cleaning './result/$NAME'" - rm -fr result/$NAME/* - ;; -esac diff --git a/src/plugins/wp/tests/wp_region/garbled.i b/src/plugins/wp/tests/wp_region/garbled.i deleted file mode 100644 index 6b703ba4245..00000000000 --- a/src/plugins/wp/tests/wp_region/garbled.i +++ /dev/null @@ -1,6 +0,0 @@ - - -float job(int *p,int *q) -{ - return *q + *(float*)p + *p ; -} diff --git a/src/plugins/wp/tests/wp_region/index.i b/src/plugins/wp/tests/wp_region/index.i deleted file mode 100644 index 6151de509bc..00000000000 --- a/src/plugins/wp/tests/wp_region/index.i +++ /dev/null @@ -1,6 +0,0 @@ -int A[3][4][5] ; - -int job(int i,int j,int k) -{ - return A[i][j][k]; -} diff --git a/src/plugins/wp/tests/wp_region/matrix.i b/src/plugins/wp/tests/wp_region/matrix.i deleted file mode 100644 index f5133222090..00000000000 --- a/src/plugins/wp/tests/wp_region/matrix.i +++ /dev/null @@ -1,8 +0,0 @@ -void job( int cols , int rows , int ** m , int * v , int * r ) -{ - for (int i = 0; i < rows; i++) { - r[i] = 0 ; - for (int j = 0; j < cols; j++) - r[i] += m[i][j] * v[j] ; - } -} diff --git a/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle b/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle deleted file mode 100644 index 11a2a154085..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle +++ /dev/null @@ -1,59 +0,0 @@ -[kernel] Parsing annot.i (no preprocessing) -/* Generated by Frama-C */ -struct N { - double v ; - int s ; -}; -typedef struct N *SN; -struct L { - int v ; - int s ; -}; -typedef struct L *SL; -struct Block { - SN prm ; - SN inp1 ; - SN inp2 ; - SN inp3 ; - SN out1 ; - SN out2 ; - SN out3 ; - SL idx1 ; - SL idx2 ; - SL idx3 ; - SN sum ; -}; -typedef struct Block FB; -/*@ \wp::wpregion *fb; */ -void fb_ADD(FB *fb) -{ - (fb->out1)->v += (fb->out2)->v; - (fb->out1)->s |= (fb->out2)->s; - return; -} - -/*@ \wp::wpregion IN: \pattern{PMEM}, (fb->inp1..fb->inp3); - \wp::wpregion OUT: \pattern{PVECTOR}, (fb->out1..fb->out3); - \wp::wpregion IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3); - */ -void fb_SORT(FB *fb) -{ - SN *inp = & fb->inp1; - SN *out = & fb->out1; - SL *idx = & fb->idx1; - { - int i = 0; - while (i < 3) { - (*(out + i))->v = (*(inp + i))->v + (fb->prm)->v; - (*(out + i))->s = 0; - (*(idx + i))->v = (*(inp + i))->s; - (*(idx + i))->s = 0; - i ++; - } - } - (fb->sum)->v = ((fb->out1)->v + (fb->out2)->v) + (fb->out3)->v; - (fb->sum)->s = 0; - return; -} - - diff --git a/src/plugins/wp/tests/wp_region/oracle/array1.0.dot b/src/plugins/wp/tests/wp_region/oracle/array1.0.dot deleted file mode 100644 index 8061a50b2de..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array1.0.dot +++ /dev/null @@ -1,57 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="n", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="q", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="k", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - A000 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _005 [ label="roots:&n", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _005; } - _005 -> A000 [ arrowhead="tee" ]; - _006 [ shape="record", label="Var sint32" ]; - A000 -> _006:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _007 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _007; } - _007 -> A001 [ arrowhead="tee" ]; - _008 [ shape="record", label="<_p1> Ref" ]; - _008:_p1 -> A005:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A001 -> _008:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _009 [ label="roots:&q", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _009; } - _009 -> A002 [ arrowhead="tee" ]; - _010 [ shape="record", label="<_p1> Ref" ]; - _010:_p1 -> A005:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A002 -> _010:w [ arrowhead="tee" ]; - A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _011 [ shape="record", label="Var sint32" ]; - A003 -> _011:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _012 [ shape="record", label="Var sint32" ]; - A004 -> _012:w [ arrowhead="tee" ]; - A005 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ]; - _013 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A005; _013; } - _013 -> A005 [ arrowhead="tee" ]; - _014 [ shape="record", label="Mem sint32" ]; - A005 -> _014:w [ arrowhead="tee" ]; - R015 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R015; A006; } - R015 -> A006 ; - A006 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _016 [ shape="record", label="Var sint32" ]; - A006 -> _016:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle deleted file mode 100644 index f594dcb8a6c..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array1.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array1.i (no preprocessing) -[wp] Region Graph: array1.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array2.0.dot b/src/plugins/wp/tests/wp_region/oracle/array2.0.dot deleted file mode 100644 index 4e9b35936cb..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array2.0.dot +++ /dev/null @@ -1,63 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="n", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="q", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="k", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - A000 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _005 [ label="roots:&n", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _005; } - _005 -> A000 [ arrowhead="tee" ]; - _006 [ shape="record", label="Var sint32" ]; - A000 -> _006:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _007 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _007; } - _007 -> A001 [ arrowhead="tee" ]; - _008 [ shape="record", label="<_p1> Ref" ]; - _008:_p1 -> A005:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A001 -> _008:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _009 [ label="roots:&q", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _009; } - _009 -> A002 [ arrowhead="tee" ]; - _010 [ shape="record", label="<_p1> Ref" ]; - _010:_p1 -> A006:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A002 -> _010:w [ arrowhead="tee" ]; - A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _011 [ shape="record", label="Var sint32" ]; - A003 -> _011:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _012 [ shape="record", label="Var sint32" ]; - A004 -> _012:w [ arrowhead="tee" ]; - A005 [ label="R[]", shape="oval", fillcolor="green", style="filled" ]; - _013 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A005; _013; } - _013 -> A005 [ arrowhead="tee" ]; - _014 [ shape="record", label="Mem sint32" ]; - A005 -> _014:w [ arrowhead="tee" ]; - A006 [ label="R[]", shape="oval", fillcolor="green", style="filled" ]; - _015 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A006; _015; } - _015 -> A006 [ arrowhead="tee" ]; - _016 [ shape="record", label="Mem sint32" ]; - A006 -> _016:w [ arrowhead="tee" ]; - R017 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R017; A007; } - R017 -> A007 ; - A007 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _018 [ shape="record", label="Var sint32" ]; - A007 -> _018:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle deleted file mode 100644 index 493acb0f321..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array2.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array2.i (no preprocessing) -[wp] Region Graph: array2.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array3.0.dot b/src/plugins/wp/tests/wp_region/oracle/array3.0.dot deleted file mode 100644 index 02d81fff4e3..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array3.0.dot +++ /dev/null @@ -1,33 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - A000 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _002 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _002; } - _002 -> A000 [ arrowhead="tee" ]; - _003 [ shape="record", label="<_p1> Var ptr" ]; - _003:_p1 -> A002:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A000 -> _003:w [ arrowhead="tee" ]; - A001 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _004 [ shape="record", label="Var sint32" ]; - A001 -> _004:w [ arrowhead="tee" ]; - A002 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ]; - _005 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _005; } - _005 -> A002 [ arrowhead="tee" ]; - _006 [ shape="record", label="Mem sint32" ]; - A002 -> _006:w [ arrowhead="tee" ]; - R007 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R007; A003; } - R007 -> A003 ; - A003 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _008 [ shape="record", label="Var sint32" ]; - A003 -> _008:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle deleted file mode 100644 index ff1d6ff8c47..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array3.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array3.i (no preprocessing) -[wp] Region Graph: array3.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array4.0.dot b/src/plugins/wp/tests/wp_region/oracle/array4.0.dot deleted file mode 100644 index e885c887b4e..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array4.0.dot +++ /dev/null @@ -1,41 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="q", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - A000 [ label="D", shape="oval" ]; - _003 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _003; } - _003 -> A000 [ arrowhead="tee" ]; - _004 [ shape="record", label="<_p1> Ref" ]; - _004:_p1 -> A003:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A000 -> _004:w [ arrowhead="tee" ]; - A001 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _005 [ shape="record", label="Var sint32" ]; - A001 -> _005:w [ arrowhead="tee" ]; - A002 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _006 [ shape="record", label="<_p1> Var ptr" ]; - _006:_p1 -> A003:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A002 -> _006:w [ arrowhead="tee" ]; - A003 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ]; - _007 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A003; _007; } - _007 -> A003 [ arrowhead="tee" ]; - _008 [ shape="record", label="Mem sint32" ]; - A003 -> _008:w [ arrowhead="tee" ]; - R009 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R009; A004; } - R009 -> A004 ; - A004 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _010 [ shape="record", label="Var sint32" ]; - A004 -> _010:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle deleted file mode 100644 index a98da77e19c..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array4.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array4.i (no preprocessing) -[wp] Region Graph: array4.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array5.0.dot b/src/plugins/wp/tests/wp_region/oracle/array5.0.dot deleted file mode 100644 index f017daa76b5..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array5.0.dot +++ /dev/null @@ -1,49 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="q", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="tmp", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - A000 [ label="D", shape="oval" ]; - _004 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _004; } - _004 -> A000 [ arrowhead="tee" ]; - _005 [ shape="record", label="<_p1> Ref" ]; - _005:_p1 -> A004:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A000 -> _005:w [ arrowhead="tee" ]; - A001 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _006 [ label="roots:&q", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _006; } - _006 -> A001 [ arrowhead="tee" ]; - _007 [ shape="record", label="<_p1> Var ptr" ]; - _007:_p1 -> A004:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A001 -> _007:w [ arrowhead="tee" ]; - A002 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _008 [ shape="record", label="Var sint32" ]; - A002 -> _008:w [ arrowhead="tee" ]; - A003 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _009 [ shape="record", label="Var sint32" ]; - A003 -> _009:w [ arrowhead="tee" ]; - A004 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ]; - _010 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A004; _010; } - _010 -> A004 [ arrowhead="tee" ]; - _011 [ shape="record", label="Mem sint32" ]; - A004 -> _011:w [ arrowhead="tee" ]; - R012 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R012; A005; } - R012 -> A005 ; - A005 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="Var sint32" ]; - A005 -> _013:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle deleted file mode 100644 index 49fd11f80bd..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array5.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array5.i (no preprocessing) -[wp] Region Graph: array5.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array6.0.dot b/src/plugins/wp/tests/wp_region/oracle/array6.0.dot deleted file mode 100644 index a55f8bb5e6e..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array6.0.dot +++ /dev/null @@ -1,41 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="A", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="k", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - A000 [ label="", shape="oval" ]; - _003 [ label="roots:&A", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _003; } - _003 -> A000 [ arrowhead="tee" ]; - _004 [ shape="record", label="<_p1> 0..319: D32[10]" ]; - _004:_p1 -> A003 [ style="dotted" ]; - A000 -> _004:w [ arrowhead="tee" ]; - A001 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _005 [ label="roots:&k", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _005; } - _005 -> A001 [ arrowhead="tee" ]; - _006 [ shape="record", label="Var sint32" ]; - A001 -> _006:w [ arrowhead="tee" ]; - A002 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _007 [ shape="record", label="Var sint32" ]; - A002 -> _007:w [ arrowhead="tee" ]; - A003 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _008 [ label="roots:&A+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A003; _008; } - _008 -> A003 [ arrowhead="tee" ]; - _009 [ shape="record", label="Mem sint32" ]; - A003 -> _009:w [ arrowhead="tee" ]; - R010 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R010; A004; } - R010 -> A004 ; - A004 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _011 [ shape="record", label="Var sint32" ]; - A004 -> _011:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle deleted file mode 100644 index 814e494ce84..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array6.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array6.i (no preprocessing) -[wp] Region Graph: array6.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array7.0.dot b/src/plugins/wp/tests/wp_region/oracle/array7.0.dot deleted file mode 100644 index e4b91ca2a02..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array7.0.dot +++ /dev/null @@ -1,47 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="A", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="k", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - A000 [ label="", shape="oval" ]; - _004 [ label="roots:&A", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _004; } - _004 -> A000 [ arrowhead="tee" ]; - _005 [ shape="record", label="<_p1> 0..319: D32[10]" ]; - _005:_p1 -> A004 [ style="dotted" ]; - A000 -> _005:w [ arrowhead="tee" ]; - A001 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _006 [ label="roots:&k", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _006; } - _006 -> A001 [ arrowhead="tee" ]; - _007 [ shape="record", label="Var sint32" ]; - A001 -> _007:w [ arrowhead="tee" ]; - A002 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _008 [ shape="record", label="Var sint32" ]; - A002 -> _008:w [ arrowhead="tee" ]; - A003 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _009 [ shape="record", label="<_p1> Var ptr" ]; - _009:_p1 -> A004:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A003 -> _009:w [ arrowhead="tee" ]; - A004 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ]; - _010 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A004; _010; } - _010 -> A004 [ arrowhead="tee" ]; - _011 [ shape="record", label="Mem sint32" ]; - A004 -> _011:w [ arrowhead="tee" ]; - R012 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R012; A005; } - R012 -> A005 ; - A005 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="Var sint32" ]; - A005 -> _013:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle deleted file mode 100644 index 8bd34f4ece8..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array7.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array7.i (no preprocessing) -[wp] Region Graph: array7.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/array8.0.dot b/src/plugins/wp/tests/wp_region/oracle/array8.0.dot deleted file mode 100644 index f062fa1492f..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array8.0.dot +++ /dev/null @@ -1,58 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="A", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="B", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A000 ; - V002 [ label="c", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A001 ; - V003 [ label="k", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A002 ; - V004 [ label="s", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A003 ; - V005 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V005:e -> A004 ; - V006 [ label="tmp", shape="cds", style="filled", fillcolor="yellow" ]; - V006:e -> A005 ; - A000 [ label="R[]&", shape="oval", fillcolor="orange", style="filled" ]; - _007 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _007; } - _007 -> A000 [ arrowhead="tee" ]; - _008 [ shape="record", label="Mem sint32" ]; - A000 -> _008:w [ arrowhead="tee" ]; - A001 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _009 [ label="roots:&c", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _009; } - _009 -> A001 [ arrowhead="tee" ]; - _010 [ shape="record", label="Var sint32" ]; - A001 -> _010:w [ arrowhead="tee" ]; - A002 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _011 [ label="roots:&k", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _011; } - _011 -> A002 [ arrowhead="tee" ]; - _012 [ shape="record", label="Var sint32" ]; - A002 -> _012:w [ arrowhead="tee" ]; - A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="Var sint32" ]; - A003 -> _013:w [ arrowhead="tee" ]; - A004 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _014 [ shape="record", label="<_p1> Var ptr" ]; - _014:_p1 -> A000:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A004 -> _014:w [ arrowhead="tee" ]; - A005 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _015 [ shape="record", label="<_p1> Var ptr" ]; - _015:_p1 -> A000:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A005 -> _015:w [ arrowhead="tee" ]; - R016 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R016; A006; } - R016 -> A006 ; - A006 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _017 [ shape="record", label="Var sint32" ]; - A006 -> _017:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle deleted file mode 100644 index 045b9aa7539..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/array8.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing array8.i (no preprocessing) -[wp] Region Graph: array8.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/diff_annot.txt b/src/plugins/wp/tests/wp_region/oracle/diff_annot.txt deleted file mode 100644 index e69de29bb2d..00000000000 diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.0.dot b/src/plugins/wp/tests/wp_region/oracle/fb_ADD.0.dot deleted file mode 100644 index c6648e78e8f..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.0.dot +++ /dev/null @@ -1,95 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="fb", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - A000 [ label="D", shape="oval" ]; - _001 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _001; } - _001 -> A000 [ arrowhead="tee" ]; - _002 [ shape="record", label="<_p1> Ref" ]; - _002:_p1 -> A001:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _002:w [ arrowhead="tee" ]; - A001 [ label="", shape="oval" ]; - _003 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _003; } - _003 -> A001 [ arrowhead="tee" ]; - _004 [ shape="record", label="<_p1> 256..319: D64|<_p2> 320..383: D64" ]; - _004:_p2 -> A003 [ style="dotted" ]; - _004:_p1 -> A002 [ style="dotted" ]; - A001 -> _004:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _005 [ label="roots:&fb+256", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A002; _005; } - _005 -> A002 [ arrowhead="tee" ]; - _006 [ shape="record", label="<_p1> Ref" ]; - _006:_p1 -> A004:w [ taillabel="*", labelangle="+30", color="red" ]; - A002 -> _006:w [ arrowhead="tee" ]; - A003 [ label="D", shape="oval" ]; - _007 [ label="roots:&fb+320", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A003; _007; } - _007 -> A003 [ arrowhead="tee" ]; - _008 [ shape="record", label="<_p1> Ref" ]; - _008:_p1 -> A005:w [ taillabel="*", labelangle="+30", color="red" ]; - A003 -> _008:w [ arrowhead="tee" ]; - A004 [ label="", shape="oval" ]; - _009 [ label="roots:&fb+256", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A004; _009; } - _009 -> A004 [ arrowhead="tee" ]; - _010 [ shape="record", label="<_p1> 0..63: D64|<_p2> 64..95: D32" ]; - _010:_p2 -> A007 [ style="dotted" ]; - _010:_p1 -> A006 [ style="dotted" ]; - A004 -> _010:w [ arrowhead="tee" ]; - A005 [ label="", shape="oval" ]; - _011 [ label="roots:&fb+320", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A005; _011; } - _011 -> A005 [ arrowhead="tee" ]; - _012 [ shape="record", label="<_p1> 0..63: D64|<_p2> 64..95: D32" ]; - _012:_p2 -> A009 [ style="dotted" ]; - _012:_p1 -> A008 [ style="dotted" ]; - A005 -> _012:w [ arrowhead="tee" ]; - A006 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _013 [ label="roots:&fb+256", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A006; _013; } - _013 -> A006 [ arrowhead="tee" ]; - _014 [ shape="record", label="Var float64" ]; - A006 -> _014:w [ arrowhead="tee" ]; - A007 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _015 [ label="roots:&fb+320", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A007; _015; } - _015 -> A007 [ arrowhead="tee" ]; - _016 [ shape="record", label="Var sint32" ]; - A007 -> _016:w [ arrowhead="tee" ]; - A008 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _017 [ label="roots:&fb+320", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A008; _017; } - _017 -> A008 [ arrowhead="tee" ]; - _018 [ shape="record", label="Var float64" ]; - A008 -> _018:w [ arrowhead="tee" ]; - A009 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _019 [ label="roots:&fb+384", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A009; _019; } - _019 -> A009 [ arrowhead="tee" ]; - _020 [ shape="record", label="Var sint32" ]; - A009 -> _020:w [ arrowhead="tee" ]; - R021 [ label="A", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R021; A000; } - R021 -> A000 ; -} 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 deleted file mode 100644 index c174f1f4537..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/fb_ADD.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing fb_ADD.i (no preprocessing) -[wp] Region Graph: fb_ADD.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.0.dot b/src/plugins/wp/tests/wp_region/oracle/fb_SORT.0.dot deleted file mode 100644 index c278bffd209..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.0.dot +++ /dev/null @@ -1,204 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="fb", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="inp", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="out", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="idx", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - A000 [ label="D", shape="oval" ]; - _005 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _005; } - _005 -> A000 [ arrowhead="tee" ]; - _006 [ shape="record", label="<_p1> Ref" ]; - _006:_p1 -> A005:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _006:w [ arrowhead="tee" ]; - A001 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _007 [ shape="record", label="<_p1> Var ptr" ]; - _007:_p1 -> A006:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A001 -> _007:w [ arrowhead="tee" ]; - A002 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _008 [ shape="record", label="<_p1> Var ptr" ]; - _008:_p1 -> A007:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A002 -> _008:w [ arrowhead="tee" ]; - A003 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _009 [ shape="record", label="<_p1> Var ptr" ]; - _009:_p1 -> A008:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A003 -> _009:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _010 [ shape="record", label="Var sint32" ]; - A004 -> _010:w [ arrowhead="tee" ]; - A005 [ label="", shape="oval" ]; - _011 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A005; _011; } - _011 -> A005 [ arrowhead="tee" ]; - _012 [ shape="record", - label="<_p1> 0..63: D64|<_p2> 64..255: D64[3]|<_p3> 256..447: D64[3]|<_p4> 448..639: D64[3]|<_p5> 640..703: D64" - ]; - _012:_p5 -> A010 [ style="dotted" ]; - _012:_p4 -> A008 [ style="dotted" ]; - _012:_p3 -> A007 [ style="dotted" ]; - _012:_p2 -> A006 [ style="dotted" ]; - _012:_p1 -> A009 [ style="dotted" ]; - A005 -> _012:w [ arrowhead="tee" ]; - A006 [ label="D[]&", shape="oval", fillcolor="orange", style="filled" ]; - _013 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A006; _013; } - _013 -> A006 [ arrowhead="tee" ]; - _014 [ shape="record", label="<_p1> Ref" ]; - _014:_p1 -> A011:w [ taillabel="*", labelangle="+30", color="red" ]; - A006 -> _014:w [ arrowhead="tee" ]; - A007 [ label="D[]&", shape="oval", fillcolor="orange", style="filled" ]; - _015 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A007; _015; } - _015 -> A007 [ arrowhead="tee" ]; - _016 [ shape="record", label="<_p1> Ref" ]; - _016:_p1 -> A012:w [ taillabel="*", labelangle="+30", color="red" ]; - A007 -> _016:w [ arrowhead="tee" ]; - A008 [ label="D[]&", shape="oval", fillcolor="orange", style="filled" ]; - _017 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A008; _017; } - _017 -> A008 [ arrowhead="tee" ]; - _018 [ shape="record", label="<_p1> Ref" ]; - _018:_p1 -> A013:w [ taillabel="*", labelangle="+30", color="red" ]; - A008 -> _018:w [ arrowhead="tee" ]; - A009 [ label="D", shape="oval" ]; - _019 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A009; _019; } - _019 -> A009 [ arrowhead="tee" ]; - _020 [ shape="record", label="<_p1> Ref" ]; - _020:_p1 -> A014:w [ taillabel="*", labelangle="+30", color="red" ]; - A009 -> _020:w [ arrowhead="tee" ]; - A010 [ label="D", shape="oval" ]; - _021 [ label="roots:&fb+640", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A010; _021; } - _021 -> A010 [ arrowhead="tee" ]; - _022 [ shape="record", label="<_p1> Ref" ]; - _022:_p1 -> A015:w [ taillabel="*", labelangle="+30", color="red" ]; - A010 -> _022:w [ arrowhead="tee" ]; - A011 [ label="&", shape="oval", fillcolor="orange", style="filled" ]; - _023 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A011; _023; } - _023 -> A011 [ arrowhead="tee" ]; - _024 [ shape="record", label="<_p1> 0..63: D64|<_p2> 64..95: D32" ]; - _024:_p2 -> A017 [ style="dotted" ]; - _024:_p1 -> A016 [ style="dotted" ]; - A011 -> _024:w [ arrowhead="tee" ]; - A012 [ label="", shape="oval" ]; - _025 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A012; _025; } - _025 -> A012 [ arrowhead="tee" ]; - _026 [ shape="record", label="<_p1> 0..63: D64|<_p2> 64..95: D32" ]; - _026:_p2 -> A019 [ style="dotted" ]; - _026:_p1 -> A018 [ style="dotted" ]; - A012 -> _026:w [ arrowhead="tee" ]; - A013 [ label="", shape="oval" ]; - _027 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A013; _027; } - _027 -> A013 [ arrowhead="tee" ]; - _028 [ shape="record", label="<_p1> 0..31: D32|<_p2> 32..63: D32" ]; - _028:_p2 -> A021 [ style="dotted" ]; - _028:_p1 -> A020 [ style="dotted" ]; - A013 -> _028:w [ arrowhead="tee" ]; - A014 [ label="", shape="oval" ]; - _029 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A014; _029; } - _029 -> A014 [ arrowhead="tee" ]; - _030 [ shape="record", label="<_p1> 0..63: D64" ]; - _030:_p1 -> A022 [ style="dotted" ]; - A014 -> _030:w [ arrowhead="tee" ]; - A015 [ label="", shape="oval" ]; - _031 [ label="roots:&fb+640", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A015; _031; } - _031 -> A015 [ arrowhead="tee" ]; - _032 [ shape="record", label="<_p1> 0..63: D64|<_p2> 64..95: D32" ]; - _032:_p2 -> A024 [ style="dotted" ]; - _032:_p1 -> A023 [ style="dotted" ]; - A015 -> _032:w [ arrowhead="tee" ]; - A016 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _033 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A016; _033; } - _033 -> A016 [ arrowhead="tee" ]; - _034 [ shape="record", label="Mem float64" ]; - A016 -> _034:w [ arrowhead="tee" ]; - A017 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _035 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A017; _035; } - _035 -> A017 [ arrowhead="tee" ]; - _036 [ shape="record", label="Mem sint32" ]; - A017 -> _036:w [ arrowhead="tee" ]; - A018 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _037 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A018; _037; } - _037 -> A018 [ arrowhead="tee" ]; - _038 [ shape="record", label="Mem float64" ]; - A018 -> _038:w [ arrowhead="tee" ]; - A019 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _039 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A019; _039; } - _039 -> A019 [ arrowhead="tee" ]; - _040 [ shape="record", label="Mem sint32" ]; - A019 -> _040:w [ arrowhead="tee" ]; - A020 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _041 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A020; _041; } - _041 -> A020 [ arrowhead="tee" ]; - _042 [ shape="record", label="Mem sint32" ]; - A020 -> _042:w [ arrowhead="tee" ]; - A021 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _043 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A021; _043; } - _043 -> A021 [ arrowhead="tee" ]; - _044 [ shape="record", label="Mem sint32" ]; - A021 -> _044:w [ arrowhead="tee" ]; - A022 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _045 [ label="roots:&fb", style="filled", color="lightblue", shape="box" ]; - { rank=same; A022; _045; } - _045 -> A022 [ arrowhead="tee" ]; - _046 [ shape="record", label="Var float64" ]; - A022 -> _046:w [ arrowhead="tee" ]; - A023 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _047 [ label="roots:&fb+640", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A023; _047; } - _047 -> A023 [ arrowhead="tee" ]; - _048 [ shape="record", label="Var float64" ]; - A023 -> _048:w [ arrowhead="tee" ]; - A024 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _049 [ label="roots:&fb+704", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A024; _049; } - _049 -> A024 [ arrowhead="tee" ]; - _050 [ shape="record", label="Var sint32" ]; - A024 -> _050:w [ arrowhead="tee" ]; - R051 [ label="IDX", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R051; A008; } - R051 -> A008 ; - R052 [ label="IN", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R052; A006; } - R052 -> A006 ; - R053 [ label="OUT", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R053; A007; } - R053 -> A007 ; - R054 [ label="Shared", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R054; A011; } - R054 -> A011 ; -} 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 deleted file mode 100644 index bfcc8d4d3ca..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/fb_SORT.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing fb_SORT.i (no preprocessing) -[wp] Region Graph: fb_SORT.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/garbled.0.dot b/src/plugins/wp/tests/wp_region/oracle/garbled.0.dot deleted file mode 100644 index 1f13727a1f3..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/garbled.0.dot +++ /dev/null @@ -1,48 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="q", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="__retres", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - A000 [ label="D", shape="oval" ]; - _003 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _003; } - _003 -> A000 [ arrowhead="tee" ]; - _004 [ shape="record", label="<_p1> Ref" ]; - _004:_p1 -> A003:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _004:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _005 [ label="roots:&q", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _005; } - _005 -> A001 [ arrowhead="tee" ]; - _006 [ shape="record", label="<_p1> Ref" ]; - _006:_p1 -> A004:w [ taillabel="*", labelangle="+30", color="red" ]; - A001 -> _006:w [ arrowhead="tee" ]; - A002 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _007 [ shape="record", label="Var float32" ]; - A002 -> _007:w [ arrowhead="tee" ]; - A003 [ label="R", shape="oval", color="red", fillcolor="red", - style="filled" - ]; - _008 [ label="roots:&p", style="filled", color="lightblue", shape="box" ]; - { rank=same; A003; _008; } - _008 -> A003 [ arrowhead="tee" ]; - _009 [ shape="record", label="Raw", fillcolor="red", style="filled" ]; - A003 -> _009:w [ arrowhead="tee" ]; - A004 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _010 [ label="roots:&q", style="filled", color="lightblue", shape="box" ]; - { rank=same; A004; _010; } - _010 -> A004 [ arrowhead="tee" ]; - _011 [ shape="record", label="Var sint32" ]; - A004 -> _011:w [ arrowhead="tee" ]; - R012 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R012; A005; } - R012 -> A005 ; - A005 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="Var float32" ]; - A005 -> _013:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle deleted file mode 100644 index c390ec3e2ad..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/garbled.res.oracle +++ /dev/null @@ -1,7 +0,0 @@ -[kernel] Parsing garbled.i (no preprocessing) -[wp:garbled] Garbled Clusters: A=sint32 B=float32 -[wp:garbled] Garbled Clusters: A=garbled B=sint32 -[wp:garbled] Garbled Clusters: A=garbled B=float32 -[wp] Region Graph: garbled.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/index.0.dot b/src/plugins/wp/tests/wp_region/oracle/index.0.dot deleted file mode 100644 index 5aea05755a4..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/index.0.dot +++ /dev/null @@ -1,57 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="A", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="j", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="k", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="__retres", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - A000 [ label="", shape="oval" ]; - _005 [ label="roots:&A", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _005; } - _005 -> A000 [ arrowhead="tee" ]; - _006 [ shape="record", label="<_p1> 0..1919: D32[5,4,3]" ]; - _006:_p1 -> A005 [ style="dotted" ]; - A000 -> _006:w [ arrowhead="tee" ]; - A001 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _007 [ label="roots:&i", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _007; } - _007 -> A001 [ arrowhead="tee" ]; - _008 [ shape="record", label="Var sint32" ]; - A001 -> _008:w [ arrowhead="tee" ]; - A002 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _009 [ label="roots:&j", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _009; } - _009 -> A002 [ arrowhead="tee" ]; - _010 [ shape="record", label="Var sint32" ]; - A002 -> _010:w [ arrowhead="tee" ]; - A003 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _011 [ label="roots:&k", style="filled", color="lightblue", shape="box" ]; - { rank=same; A003; _011; } - _011 -> A003 [ arrowhead="tee" ]; - _012 [ shape="record", label="Var sint32" ]; - A003 -> _012:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="Var sint32" ]; - A004 -> _013:w [ arrowhead="tee" ]; - A005 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _014 [ label="roots:&A+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A005; _014; } - _014 -> A005 [ arrowhead="tee" ]; - _015 [ shape="record", label="Mem sint32" ]; - A005 -> _015:w [ arrowhead="tee" ]; - R016 [ label="\\result", shape="tab", style="filled", fillcolor="yellow" ]; - { rank=same; R016; A006; } - R016 -> A006 ; - A006 [ label="W", shape="oval", fillcolor="green", style="filled" ]; - _017 [ shape="record", label="Var sint32" ]; - A006 -> _017:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle/index.res.oracle deleted file mode 100644 index 953037c02fa..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/index.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing index.i (no preprocessing) -[wp] Region Graph: index.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/matrix.0.dot b/src/plugins/wp/tests/wp_region/oracle/matrix.0.dot deleted file mode 100644 index fcce73f07e9..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/matrix.0.dot +++ /dev/null @@ -1,93 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="cols", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="rows", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="m", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="v", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="r", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - V005 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V005:e -> A005 ; - V006 [ label="j", shape="cds", style="filled", fillcolor="yellow" ]; - V006:e -> A006 ; - A000 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _007 [ label="roots:&cols", style="filled", color="lightblue", shape="box" - ]; - { rank=same; A000; _007; } - _007 -> A000 [ arrowhead="tee" ]; - _008 [ shape="record", label="Var sint32" ]; - A000 -> _008:w [ arrowhead="tee" ]; - A001 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _009 [ label="roots:&rows", style="filled", color="lightblue", shape="box" - ]; - { rank=same; A001; _009; } - _009 -> A001 [ arrowhead="tee" ]; - _010 [ shape="record", label="Var sint32" ]; - A001 -> _010:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _011 [ label="roots:&m", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _011; } - _011 -> A002 [ arrowhead="tee" ]; - _012 [ shape="record", label="<_p1> Ref" ]; - _012:_p1 -> A007:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A002 -> _012:w [ arrowhead="tee" ]; - A003 [ label="D", shape="oval" ]; - _013 [ label="roots:&v", style="filled", color="lightblue", shape="box" ]; - { rank=same; A003; _013; } - _013 -> A003 [ arrowhead="tee" ]; - _014 [ shape="record", label="<_p1> Ref" ]; - _014:_p1 -> A008:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A003 -> _014:w [ arrowhead="tee" ]; - A004 [ label="D", shape="oval" ]; - _015 [ label="roots:&r", style="filled", color="lightblue", shape="box" ]; - { rank=same; A004; _015; } - _015 -> A004 [ arrowhead="tee" ]; - _016 [ shape="record", label="<_p1> Ref" ]; - _016:_p1 -> A009:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A004 -> _016:w [ arrowhead="tee" ]; - A005 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _017 [ shape="record", label="Var sint32" ]; - A005 -> _017:w [ arrowhead="tee" ]; - A006 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _018 [ shape="record", label="Var sint32" ]; - A006 -> _018:w [ arrowhead="tee" ]; - A007 [ label="D[]", shape="oval" ]; - _019 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A007; _019; } - _019 -> A007 [ arrowhead="tee" ]; - _020 [ shape="record", label="<_p1> Ref" ]; - _020:_p1 -> A010:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A007 -> _020:w [ arrowhead="tee" ]; - A008 [ label="R[]", shape="oval", fillcolor="green", style="filled" ]; - _021 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A008; _021; } - _021 -> A008 [ arrowhead="tee" ]; - _022 [ shape="record", label="Mem sint32" ]; - A008 -> _022:w [ arrowhead="tee" ]; - A009 [ label="RW[]", shape="oval", fillcolor="green", style="filled" ]; - _023 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A009; _023; } - _023 -> A009 [ arrowhead="tee" ]; - _024 [ shape="record", label="Mem sint32" ]; - A009 -> _024:w [ arrowhead="tee" ]; - A010 [ label="R[]", shape="oval", fillcolor="green", style="filled" ]; - _025 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A010; _025; } - _025 -> A010 [ arrowhead="tee" ]; - _026 [ shape="record", label="Mem sint32" ]; - A010 -> _026:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle deleted file mode 100644 index 01ca9097b9d..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/matrix.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing matrix.i (no preprocessing) -[wp] Region Graph: matrix.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray1.0.dot b/src/plugins/wp/tests/wp_region/oracle/structarray1.0.dot deleted file mode 100644 index c9b16ac8ffe..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray1.0.dot +++ /dev/null @@ -1,70 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="M", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="X", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="R", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="j", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - A000 [ label="D", shape="oval" ]; - _005 [ label="roots:&M", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _005; } - _005 -> A000 [ arrowhead="tee" ]; - _006 [ shape="record", label="<_p1> Ref" ]; - _006:_p1 -> A005:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _006:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _007 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _007; } - _007 -> A001 [ arrowhead="tee" ]; - _008 [ shape="record", label="<_p1> Ref" ]; - _008:_p1 -> A006:w [ taillabel="*", labelangle="+30", color="red" ]; - A001 -> _008:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _009 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _009; } - _009 -> A002 [ arrowhead="tee" ]; - _010 [ shape="record", label="<_p1> Ref" ]; - _010:_p1 -> A006:w [ taillabel="*", labelangle="+30", color="red" ]; - A002 -> _010:w [ arrowhead="tee" ]; - A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _011 [ shape="record", label="Var sint32" ]; - A003 -> _011:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _012 [ shape="record", label="Var sint32" ]; - A004 -> _012:w [ arrowhead="tee" ]; - A005 [ label="", shape="oval" ]; - _013 [ label="roots:&M", style="filled", color="lightblue", shape="box" ]; - { rank=same; A005; _013; } - _013 -> A005 [ arrowhead="tee" ]; - _014 [ shape="record", label="<_p1> 0..511: D32[4,4]" ]; - _014:_p1 -> A007 [ style="dotted" ]; - A005 -> _014:w [ arrowhead="tee" ]; - A006 [ label="&", shape="oval", fillcolor="orange", style="filled" ]; - _015 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A006; _015; } - _015 -> A006 [ arrowhead="tee" ]; - _016 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _016:_p1 -> A008 [ style="dotted" ]; - A006 -> _016:w [ arrowhead="tee" ]; - A007 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _017 [ label="roots:&M+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A007; _017; } - _017 -> A007 [ arrowhead="tee" ]; - _018 [ shape="record", label="Mem sint32" ]; - A007 -> _018:w [ arrowhead="tee" ]; - A008 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _019 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A008; _019; } - _019 -> A008 [ arrowhead="tee" ]; - _020 [ shape="record", label="Mem sint32" ]; - A008 -> _020:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle deleted file mode 100644 index 393a63b1498..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray1.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing structarray1.i (no preprocessing) -[wp] Region Graph: structarray1.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray2.0.dot b/src/plugins/wp/tests/wp_region/oracle/structarray2.0.dot deleted file mode 100644 index c230c91fe3f..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray2.0.dot +++ /dev/null @@ -1,97 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="M", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="X", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="R", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="j", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - V005 [ label="C", shape="cds", style="filled", fillcolor="yellow" ]; - V005:e -> A005 ; - A000 [ label="D", shape="oval" ]; - _006 [ label="roots:&M", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _006; } - _006 -> A000 [ arrowhead="tee" ]; - _007 [ shape="record", label="<_p1> Ref" ]; - _007:_p1 -> A006:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _007:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _008 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _008; } - _008 -> A001 [ arrowhead="tee" ]; - _009 [ shape="record", label="<_p1> Ref" ]; - _009:_p1 -> A007:w [ taillabel="*", labelangle="+30", color="red" ]; - A001 -> _009:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _010 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _010; } - _010 -> A002 [ arrowhead="tee" ]; - _011 [ shape="record", label="<_p1> Ref" ]; - _011:_p1 -> A008:w [ taillabel="*", labelangle="+30", color="red" ]; - A002 -> _011:w [ arrowhead="tee" ]; - A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _012 [ shape="record", label="Var sint32" ]; - A003 -> _012:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="Var sint32" ]; - A004 -> _013:w [ arrowhead="tee" ]; - A005 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _014 [ shape="record", label="<_p1> Var ptr" ]; - _014:_p1 -> A009:w [ taillabel="*", labelangle="+30", color="red" ]; - A005 -> _014:w [ arrowhead="tee" ]; - A006 [ label="", shape="oval" ]; - _015 [ label="roots:&M", style="filled", color="lightblue", shape="box" ]; - { rank=same; A006; _015; } - _015 -> A006 [ arrowhead="tee" ]; - _016 [ shape="record", label="<_p1> 0..511: D32[4,4]" ]; - _016:_p1 -> A010 [ style="dotted" ]; - A006 -> _016:w [ arrowhead="tee" ]; - A007 [ label="", shape="oval" ]; - _017 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A007; _017; } - _017 -> A007 [ arrowhead="tee" ]; - _018 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _018:_p1 -> A011 [ style="dotted" ]; - A007 -> _018:w [ arrowhead="tee" ]; - A008 [ label="", shape="oval" ]; - _019 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A008; _019; } - _019 -> A008 [ arrowhead="tee" ]; - _020 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _020:_p1 -> A012 [ style="dotted" ]; - A008 -> _020:w [ arrowhead="tee" ]; - A009 [ label="&", shape="oval", fillcolor="orange", style="filled" ]; - _021 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _021:_p1 -> A010 [ style="dotted" ]; - A009 -> _021:w [ arrowhead="tee" ]; - A010 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _022 [ label="roots:&M+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A010; _022; } - _022 -> A010 [ arrowhead="tee" ]; - _023 [ shape="record", label="Mem sint32" ]; - A010 -> _023:w [ arrowhead="tee" ]; - A011 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _024 [ label="roots:&X+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A011; _024; } - _024 -> A011 [ arrowhead="tee" ]; - _025 [ shape="record", label="Mem sint32" ]; - A011 -> _025:w [ arrowhead="tee" ]; - A012 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _026 [ label="roots:&R+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A012; _026; } - _026 -> A012 [ arrowhead="tee" ]; - _027 [ shape="record", label="Mem sint32" ]; - A012 -> _027:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle deleted file mode 100644 index f71c9e902cc..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray2.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing structarray2.i (no preprocessing) -[wp] Region Graph: structarray2.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray3.0.dot b/src/plugins/wp/tests/wp_region/oracle/structarray3.0.dot deleted file mode 100644 index 8f7746c098f..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray3.0.dot +++ /dev/null @@ -1,114 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="c", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="P", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="Q", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="X", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="R", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - V005 [ label="M", shape="cds", style="filled", fillcolor="yellow" ]; - V005:e -> A005 ; - V006 [ label="tmp", shape="cds", style="filled", fillcolor="yellow" ]; - V006:e -> A006 ; - V007 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V007:e -> A007 ; - V008 [ label="j", shape="cds", style="filled", fillcolor="yellow" ]; - V008:e -> A008 ; - A000 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _009 [ label="roots:&c", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _009; } - _009 -> A000 [ arrowhead="tee" ]; - _010 [ shape="record", label="Var sint32" ]; - A000 -> _010:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _011 [ label="roots:&P", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _011; } - _011 -> A001 [ arrowhead="tee" ]; - _012 [ shape="record", label="<_p1> Ref" ]; - _012:_p1 -> A009:w [ taillabel="*", labelangle="+30", color="red" ]; - A001 -> _012:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _013 [ label="roots:&Q", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _013; } - _013 -> A002 [ arrowhead="tee" ]; - _014 [ shape="record", label="<_p1> Ref" ]; - _014:_p1 -> A009:w [ taillabel="*", labelangle="+30", color="red" ]; - A002 -> _014:w [ arrowhead="tee" ]; - A003 [ label="D", shape="oval" ]; - _015 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A003; _015; } - _015 -> A003 [ arrowhead="tee" ]; - _016 [ shape="record", label="<_p1> Ref" ]; - _016:_p1 -> A010:w [ taillabel="*", labelangle="+30", color="red" ]; - A003 -> _016:w [ arrowhead="tee" ]; - A004 [ label="D", shape="oval" ]; - _017 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A004; _017; } - _017 -> A004 [ arrowhead="tee" ]; - _018 [ shape="record", label="<_p1> Ref" ]; - _018:_p1 -> A011:w [ taillabel="*", labelangle="+30", color="red" ]; - A004 -> _018:w [ arrowhead="tee" ]; - A005 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _019 [ shape="record", label="<_p1> Var ptr" ]; - _019:_p1 -> A009:w [ taillabel="*", labelangle="+30", color="red" ]; - A005 -> _019:w [ arrowhead="tee" ]; - A006 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _020 [ shape="record", label="<_p1> Var ptr" ]; - _020:_p1 -> A009:w [ taillabel="*", labelangle="+30", color="red" ]; - A006 -> _020:w [ arrowhead="tee" ]; - A007 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _021 [ shape="record", label="Var sint32" ]; - A007 -> _021:w [ arrowhead="tee" ]; - A008 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _022 [ shape="record", label="Var sint32" ]; - A008 -> _022:w [ arrowhead="tee" ]; - A009 [ label="&", shape="oval", fillcolor="orange", style="filled" ]; - _023 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A009; _023; } - _023 -> A009 [ arrowhead="tee" ]; - _024 [ shape="record", label="<_p1> 0..511: D32[4,4]" ]; - _024:_p1 -> A012 [ style="dotted" ]; - A009 -> _024:w [ arrowhead="tee" ]; - A010 [ label="", shape="oval" ]; - _025 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A010; _025; } - _025 -> A010 [ arrowhead="tee" ]; - _026 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _026:_p1 -> A013 [ style="dotted" ]; - A010 -> _026:w [ arrowhead="tee" ]; - A011 [ label="", shape="oval" ]; - _027 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A011; _027; } - _027 -> A011 [ arrowhead="tee" ]; - _028 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _028:_p1 -> A014 [ style="dotted" ]; - A011 -> _028:w [ arrowhead="tee" ]; - A012 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _029 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A012; _029; } - _029 -> A012 [ arrowhead="tee" ]; - _030 [ shape="record", label="Mem sint32" ]; - A012 -> _030:w [ arrowhead="tee" ]; - A013 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _031 [ label="roots:&X+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A013; _031; } - _031 -> A013 [ arrowhead="tee" ]; - _032 [ shape="record", label="Mem sint32" ]; - A013 -> _032:w [ arrowhead="tee" ]; - A014 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _033 [ label="roots:&R+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A014; _033; } - _033 -> A014 [ arrowhead="tee" ]; - _034 [ shape="record", label="Mem sint32" ]; - A014 -> _034:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle deleted file mode 100644 index 1e7d3cfb400..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray3.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing structarray3.i (no preprocessing) -[wp] Region Graph: structarray3.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray4.0.dot b/src/plugins/wp/tests/wp_region/oracle/structarray4.0.dot deleted file mode 100644 index 7e75e995265..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray4.0.dot +++ /dev/null @@ -1,110 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="M", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="X", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="R", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - V003 [ label="p", shape="cds", style="filled", fillcolor="yellow" ]; - V003:e -> A003 ; - V004 [ label="i", shape="cds", style="filled", fillcolor="yellow" ]; - V004:e -> A004 ; - V005 [ label="j", shape="cds", style="filled", fillcolor="yellow" ]; - V005:e -> A005 ; - V006 [ label="C", shape="cds", style="filled", fillcolor="yellow" ]; - V006:e -> A006 ; - A000 [ label="D", shape="oval" ]; - _007 [ label="roots:&M", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _007; } - _007 -> A000 [ arrowhead="tee" ]; - _008 [ shape="record", label="<_p1> Ref" ]; - _008:_p1 -> A007:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _008:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _009 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _009; } - _009 -> A001 [ arrowhead="tee" ]; - _010 [ shape="record", label="<_p1> Ref" ]; - _010:_p1 -> A008:w [ taillabel="*", labelangle="+30", color="red" ]; - A001 -> _010:w [ arrowhead="tee" ]; - A002 [ label="D", shape="oval" ]; - _011 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A002; _011; } - _011 -> A002 [ arrowhead="tee" ]; - _012 [ shape="record", label="<_p1> Ref" ]; - _012:_p1 -> A009:w [ taillabel="*", labelangle="+30", color="red" ]; - A002 -> _012:w [ arrowhead="tee" ]; - A003 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _013 [ shape="record", label="<_p1> Var ptr" ]; - _013:_p1 -> A010:w [ taillabel="[..]", labeldistance="1.7", - labelangle="+40", color="red" - ]; - A003 -> _013:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _014 [ shape="record", label="Var sint32" ]; - A004 -> _014:w [ arrowhead="tee" ]; - A005 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _015 [ shape="record", label="Var sint32" ]; - A005 -> _015:w [ arrowhead="tee" ]; - A006 [ label="DW", shape="oval", fillcolor="green", style="filled" ]; - _016 [ shape="record", label="<_p1> Var ptr" ]; - _016:_p1 -> A011:w [ taillabel="*", labelangle="+30", color="red" ]; - A006 -> _016:w [ arrowhead="tee" ]; - A007 [ label="", shape="oval" ]; - _017 [ label="roots:&M", style="filled", color="lightblue", shape="box" ]; - { rank=same; A007; _017; } - _017 -> A007 [ arrowhead="tee" ]; - _018 [ shape="record", label="<_p1> 0..511: D32[16]" ]; - _018:_p1 -> A012 [ style="dotted" ]; - A007 -> _018:w [ arrowhead="tee" ]; - A008 [ label="", shape="oval" ]; - _019 [ label="roots:&X", style="filled", color="lightblue", shape="box" ]; - { rank=same; A008; _019; } - _019 -> A008 [ arrowhead="tee" ]; - _020 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _020:_p1 -> A013 [ style="dotted" ]; - A008 -> _020:w [ arrowhead="tee" ]; - A009 [ label="", shape="oval" ]; - _021 [ label="roots:&R", style="filled", color="lightblue", shape="box" ]; - { rank=same; A009; _021; } - _021 -> A009 [ arrowhead="tee" ]; - _022 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _022:_p1 -> A014 [ style="dotted" ]; - A009 -> _022:w [ arrowhead="tee" ]; - A010 [ label="[]&", shape="oval", fillcolor="orange", style="filled" ]; - _023 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A010; _023; } - _023 -> A010 [ arrowhead="tee" ]; - _024 [ shape="record", label="<_p1> 0..511: D32[16]" ]; - _024:_p1 -> A012 [ style="dotted" ]; - A010 -> _024:w [ arrowhead="tee" ]; - A011 [ label="&", shape="oval", fillcolor="orange", style="filled" ]; - _025 [ shape="record", label="<_p1> 0..127: D32[4]" ]; - _025:_p1 -> A012 [ style="dotted" ]; - A011 -> _025:w [ arrowhead="tee" ]; - A012 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _026 [ label="roots:*", style="filled", color="lightblue", shape="box" ]; - { rank=same; A012; _026; } - _026 -> A012 [ arrowhead="tee" ]; - _027 [ shape="record", label="Mem sint32" ]; - A012 -> _027:w [ arrowhead="tee" ]; - A013 [ label="R", shape="oval", fillcolor="green", style="filled" ]; - _028 [ label="roots:&X+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A013; _028; } - _028 -> A013 [ arrowhead="tee" ]; - _029 [ shape="record", label="Mem sint32" ]; - A013 -> _029:w [ arrowhead="tee" ]; - A014 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _030 [ label="roots:&R+(..)", style="filled", color="lightblue", - shape="box" - ]; - { rank=same; A014; _030; } - _030 -> A014 [ arrowhead="tee" ]; - _031 [ shape="record", label="Mem sint32" ]; - A014 -> _031:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle deleted file mode 100644 index 0f68a735ae3..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/structarray4.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing structarray4.i (no preprocessing) -[wp] Region Graph: structarray4.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.0.dot b/src/plugins/wp/tests/wp_region/oracle/swap.0.dot deleted file mode 100644 index f4e8e067375..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/swap.0.dot +++ /dev/null @@ -1,40 +0,0 @@ -digraph "job" { - rankdir="LR" ; - node [ fontname="monospace" ]; - edge [ fontname="monospace" ]; - V000 [ label="x", shape="cds", style="filled", fillcolor="yellow" ]; - V000:e -> A000 ; - V001 [ label="y", shape="cds", style="filled", fillcolor="yellow" ]; - V001:e -> A001 ; - V002 [ label="t", shape="cds", style="filled", fillcolor="yellow" ]; - V002:e -> A002 ; - A000 [ label="D", shape="oval" ]; - _003 [ label="roots:&x", style="filled", color="lightblue", shape="box" ]; - { rank=same; A000; _003; } - _003 -> A000 [ arrowhead="tee" ]; - _004 [ shape="record", label="<_p1> Ref" ]; - _004:_p1 -> A003:w [ taillabel="*", labelangle="+30", color="red" ]; - A000 -> _004:w [ arrowhead="tee" ]; - A001 [ label="D", shape="oval" ]; - _005 [ label="roots:&y", style="filled", color="lightblue", shape="box" ]; - { rank=same; A001; _005; } - _005 -> A001 [ arrowhead="tee" ]; - _006 [ shape="record", label="<_p1> Ref" ]; - _006:_p1 -> A004:w [ taillabel="*", labelangle="+30", color="red" ]; - A001 -> _006:w [ arrowhead="tee" ]; - A002 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _007 [ shape="record", label="Var sint32" ]; - A002 -> _007:w [ arrowhead="tee" ]; - A003 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _008 [ label="roots:&x", style="filled", color="lightblue", shape="box" ]; - { rank=same; A003; _008; } - _008 -> A003 [ arrowhead="tee" ]; - _009 [ shape="record", label="Var sint32" ]; - A003 -> _009:w [ arrowhead="tee" ]; - A004 [ label="RW", shape="oval", fillcolor="green", style="filled" ]; - _010 [ label="roots:&y", style="filled", color="lightblue", shape="box" ]; - { rank=same; A004; _010; } - _010 -> A004 [ arrowhead="tee" ]; - _011 [ shape="record", label="Var sint32" ]; - A004 -> _011:w [ arrowhead="tee" ]; -} diff --git a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle deleted file mode 100644 index 77078dae158..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle/swap.res.oracle +++ /dev/null @@ -1,4 +0,0 @@ -[kernel] Parsing swap.i (no preprocessing) -[wp] Region Graph: swap.0.dot -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle deleted file mode 100644 index e7bafef6d0d..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array1.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array1.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle deleted file mode 100644 index f65e5113a5d..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array2.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array2.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle deleted file mode 100644 index 8a0eef80a86..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array3.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array3.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle deleted file mode 100644 index 43b02d2fdd5..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array4.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array4.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle deleted file mode 100644 index 5dde4c62c22..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array5.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array5.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle deleted file mode 100644 index 87e0d0c26bf..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array6.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array6.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle deleted file mode 100644 index 58b7b84d760..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array7.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array7.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle deleted file mode 100644 index ee372986dc5..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/array8.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing array8.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle deleted file mode 100644 index 65aa343de9a..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_ADD.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing fb_ADD.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle deleted file mode 100644 index eed91319fd7..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/fb_SORT.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing fb_SORT.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle deleted file mode 100644 index ef140ddb094..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/garbled.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing garbled.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle deleted file mode 100644 index 514228d38dc..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/index.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing index.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle deleted file mode 100644 index 2b4866fb08a..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/matrix.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing matrix.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle deleted file mode 100644 index ffb1d191f76..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray1.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing structarray1.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle deleted file mode 100644 index 7625bb9224d..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray2.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing structarray2.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle deleted file mode 100644 index ecc9c7ec63c..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray3.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing structarray3.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle deleted file mode 100644 index f71833e1171..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/structarray4.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing structarray4.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle deleted file mode 100644 index ee37192b877..00000000000 --- a/src/plugins/wp/tests/wp_region/oracle_qualif/swap.res.oracle +++ /dev/null @@ -1,6 +0,0 @@ -# frama-c -wp [...] -[kernel] Parsing swap.i (no preprocessing) -[wp] Running WP plugin... -[wp] Warning: Missing RTE guards -[wp] Warning: No goal generated ------------------------------------------------------------- diff --git a/src/plugins/wp/tests/wp_region/structarray1.i b/src/plugins/wp/tests/wp_region/structarray1.i deleted file mode 100644 index e8fb0e753eb..00000000000 --- a/src/plugins/wp/tests/wp_region/structarray1.i +++ /dev/null @@ -1,18 +0,0 @@ -typedef struct Vector { - int coord[4]; -} * vector ; - -typedef struct Matrix { - int coef[4][4]; -} * matrix ; - -//@ \wp::wpregion *X , *R ; -void job( matrix M , vector X , vector R ) -{ - for (int i = 0; i < 4; i++) { - R->coord[i] = 0 ; - for (int j = 0; j < 4; i++) { - R->coord[i] += M->coef[i][j] * X->coord[j]; - } - } -} diff --git a/src/plugins/wp/tests/wp_region/structarray2.i b/src/plugins/wp/tests/wp_region/structarray2.i deleted file mode 100644 index 472077d231c..00000000000 --- a/src/plugins/wp/tests/wp_region/structarray2.i +++ /dev/null @@ -1,18 +0,0 @@ -typedef struct Vector { - int coord[4]; -} * vector ; - -typedef struct Matrix { - int coef[4][4]; -} * matrix ; - -void job( matrix M , vector X , vector R ) -{ - for (int i = 0; i < 4; i++) { - R->coord[i] = 0 ; - for (int j = 0; j < 4; i++) { - vector C = (vector) (M->coef[i]) ; - R->coord[i] += C->coord[j] * X->coord[j]; - } - } -} diff --git a/src/plugins/wp/tests/wp_region/structarray3.i b/src/plugins/wp/tests/wp_region/structarray3.i deleted file mode 100644 index fc05e0a87a7..00000000000 --- a/src/plugins/wp/tests/wp_region/structarray3.i +++ /dev/null @@ -1,18 +0,0 @@ -typedef struct Vector { - int coord[4]; -} * vector ; - -typedef struct Matrix { - int coef[4][4]; -} * matrix ; - -void job( int c , matrix P , matrix Q , vector X , vector R ) -{ - matrix M = c ? P : Q ; - for (int i = 0; i < 4; i++) { - R->coord[i] = 0 ; - for (int j = 0; j < 4; i++) { - R->coord[i] += M->coef[i][j] * X->coord[j]; - } - } -} diff --git a/src/plugins/wp/tests/wp_region/structarray4.i b/src/plugins/wp/tests/wp_region/structarray4.i deleted file mode 100644 index c27ac7ed8f7..00000000000 --- a/src/plugins/wp/tests/wp_region/structarray4.i +++ /dev/null @@ -1,20 +0,0 @@ -typedef struct Vector { - int coord[4]; -} * vector ; - -typedef struct Matrix { - int coef[4][4]; -} * matrix ; - -void job( matrix M , vector X , vector R ) -{ - int * p = (int *) M->coef ; - p[14] = 2 ; - for (int i = 0; i < 4; i++) { - R->coord[i] = 0 ; - for (int j = 0; j < 4; i++) { - vector C = (vector) (M->coef[i]) ; - R->coord[i] += C->coord[j] * X->coord[j]; - } - } -} diff --git a/src/plugins/wp/tests/wp_region/swap.i b/src/plugins/wp/tests/wp_region/swap.i deleted file mode 100644 index f299d968704..00000000000 --- a/src/plugins/wp/tests/wp_region/swap.i +++ /dev/null @@ -1,8 +0,0 @@ -// Test Config - -void job(int *x,int *y) -{ - int t = *x ; - *x = *y ; - *y = t ; -} diff --git a/src/plugins/wp/tests/wp_region/test_config b/src/plugins/wp/tests/wp_region/test_config deleted file mode 100644 index 4d45c6ca7df..00000000000 --- a/src/plugins/wp/tests/wp_region/test_config +++ /dev/null @@ -1,4 +0,0 @@ -PLUGIN: wp,rtegen -CMD: @frama-c@ -LOG: @PTEST_NAME@.@PTEST_NUMBER@.dot -OPT: -wp-prover none -wp-region -wp-msg-key dot,chunk,roots,garbled -wp-warn-key pedantic-assigns=inactive -wp-region-output-dot @PTEST_RESULT@/@PTEST_NAME@.@PTEST_NUMBER@.dot -wp-fct job -generated-spec-custom assigns:skip,exits:skip,terminates:skip diff --git a/src/plugins/wp/tests/wp_region/test_config_qualif b/src/plugins/wp/tests/wp_region/test_config_qualif deleted file mode 100644 index 4cd9b34453a..00000000000 --- a/src/plugins/wp/tests/wp_region/test_config_qualif +++ /dev/null @@ -1 +0,0 @@ -OPT: -wp-region -generated-spec-custom assigns:skip,exits:skip,terminates:skip -- GitLab