diff --git a/nix/plugins-tests.nix b/nix/plugins-tests.nix
index a500d6d0ce11b44a18ed1f1690bd1ae250eb011a..b6a83abadd16fc420eb532347994f0e9646909e9 100644
--- a/nix/plugins-tests.nix
+++ b/nix/plugins-tests.nix
@@ -24,6 +24,7 @@ mk_tests {
@src/plugins/markdown-report/tests/ptests \
@src/plugins/nonterm/tests/ptests \
@src/plugins/report/tests/ptests \
+ @src/plugins/region/tests/ptests \
@src/plugins/server/tests/ptests \
@src/plugins/variadic/tests/ptests
'';
diff --git a/src/plugins/region/store.ml b/src/plugins/region/store.ml
index 7e6121b5da90de713c673d1dd1460820ca7fbb0c..4e964e42b373265fedea995c5665efd92e916e39 100644
--- a/src/plugins/region/store.ml
+++ b/src/plugins/region/store.ml
@@ -32,6 +32,7 @@ type 'a store = 'a Imap.t ref
let new_store () = ref Imap.empty
let copy r = ref !r
let rid = ref 0
+
let make s v =
let k = incr rid ; !rid in
s := Imap.add k v !s ; k
diff --git a/src/plugins/region/tests/ptests_config b/src/plugins/region/tests/ptests_config
new file mode 100644
index 0000000000000000000000000000000000000000..316166170520da8ec5a4067d38647cf887490c58
--- /dev/null
+++ b/src/plugins/region/tests/ptests_config
@@ -0,0 +1 @@
+DEFAULT_SUITES= region
diff --git a/src/plugins/region/tests/region/fb_ADD.i b/src/plugins/region/tests/region/fb_ADD.i
new file mode 100644
index 0000000000000000000000000000000000000000..8ceb168c7af4dbce81e6776ee4fffd4b2c838ae7
--- /dev/null
+++ b/src/plugins/region/tests/region/fb_ADD.i
@@ -0,0 +1,22 @@
+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 ;
+
+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/region/tests/region/fb_SORT.i b/src/plugins/region/tests/region/fb_SORT.i
new file mode 100644
index 0000000000000000000000000000000000000000..4ef65d2cfb6145f4c3266320fbeed7b8c7eb4145
--- /dev/null
+++ b/src/plugins/region/tests/region/fb_SORT.i
@@ -0,0 +1,38 @@
+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 ;
+
+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/region/tests/region/garbled.i b/src/plugins/region/tests/region/garbled.i
new file mode 100644
index 0000000000000000000000000000000000000000..6b703ba4245ba130e45827ac182b69f5dd03dfdd
--- /dev/null
+++ b/src/plugins/region/tests/region/garbled.i
@@ -0,0 +1,6 @@
+
+
+float job(int *p,int *q)
+{
+ return *q + *(float*)p + *p ;
+}
diff --git a/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..84e4fe84a136c3e51118270f99079d75072b4153
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/fb_ADD.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing fb_ADD.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0001: R-- fb (FB *) 64b (*R0003) ;
+ R0003: --- 704b 256..320 [1]: R0005 320..384 [1]: R0018 ;
+ R0005: R-- (struct N *) 64b (*R0008) ;
+ R0008: --- 128b 0..64 [1]: R000a 64..96 [1]: R0027 ;
+ R000a: RW- (double) 64b ;
+ R0027: RW- (int) 32b ;
+ R0018: R-- (struct N *) 64b (*R001b) ;
+ R001b: --- 128b 0..64 [1]: R001d 64..96 [1]: R003a ;
+ R001d: R-- (double) 64b ;
+ R003a: R-- (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..eec439e3a9f3c953ecd495bca08e0b55e1775ae9
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/fb_SORT.res.oracle
@@ -0,0 +1,33 @@
+[kernel] Parsing fb_SORT.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0003: R-- fb (FB *) 64b (*R0005) ;
+ R0005: ---
+ 704b
+ 0..128 [2]: R0007
+ 256..320 [1]: R000e
+ 320..384 [1]: R0066
+ 384..512 [2]: R0015
+ 640..704 [1]: R0053 ;
+ R0007: R-- (struct N *) 64b (*R0024) ;
+ R0024: --- 128b 0..64 [1]: R0026 64..96 [1]: R0046 ;
+ R0026: R-- (double) 64b ;
+ R0046: R-- (int) 32b ;
+ R000e: R-- (struct N *) 64b (*R001d) ;
+ R001d: --- 128b 0..64 [1]: R001f 64..96 [1]: R0038 ;
+ R001f: RW- (double) 64b ;
+ R0038: -W- (int) 32b ;
+ R0066: R-- (struct N *) 64b (*R0069) ;
+ R0069: --- 128b 0..64 [1]: R006b ;
+ R006b: R-- (double) 64b ;
+ R0015: R-- (struct N *) (struct L *) 64b (*R003e) ;
+ R003e: --- 64b 0..64 [2]: R0040 ;
+ R0040: RW- (int) (double) 32b ;
+ R0053: R-- (struct N *) 64b (*R0056) ;
+ R0056: --- 128b 0..64 [1]: R0058 64..96 [1]: R007f ;
+ R0058: -W- (double) 64b ;
+ R007f: -W- (int) 32b ;
+ R0001: RW- inp (SN *) 64b (*R0007) ;
+ R000a: RW- out (SN *) 64b (*R000e) ;
+ R0011: RW- idx (SL *) 64b (*R0015) ;
+ R0018: RW- i (int) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/garbled.res.oracle b/src/plugins/region/tests/region/oracle/garbled.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..024e97e7a347465d0c35c9340e432a711cbe9d92
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/garbled.res.oracle
@@ -0,0 +1,8 @@
+[kernel] Parsing garbled.i (no preprocessing)
+[region] Analyzing regions
+[region] Function job:
+ R0007: R-- p (int *) 64b (*R0009) ;
+ R0009: R-- (int) (float) 32b ;
+ R0002: R-- q (int *) 64b (*R0004) ;
+ R0004: R-- (int) 32b ;
+ R0001: RW- __retres (float) 32b ;
diff --git a/src/plugins/region/tests/region/oracle/swap.res.oracle b/src/plugins/region/tests/region/oracle/swap.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..3117fb686d5ee476901cd95a19ab05fd51194ca0
--- /dev/null
+++ b/src/plugins/region/tests/region/oracle/swap.res.oracle
@@ -0,0 +1,13 @@
+[kernel] Parsing swap.i (no preprocessing)
+[region] Analyzing regions
+[region] Function swap_aliased:
+ R0004: R-- a (int *) 64b (*R0007) ;
+ R0007: RW- R: (int) 32b ;
+ R0001: R-- b (int *) 64b (*R0007) ;
+ R0008: RW- tmp (int) 32b ;
+[region] Function swap_separated:
+ R0013: R-- a (int *) 64b (*R0016) ;
+ R0016: RW- A: (int) 32b ;
+ R0017: R-- b (int *) 64b (*R001a) ;
+ R001a: RW- B: (int) 32b ;
+ R001b: RW- tmp (int) 32b ;
diff --git a/src/plugins/region/tests/region/swap.i b/src/plugins/region/tests/region/swap.i
new file mode 100644
index 0000000000000000000000000000000000000000..04816ea5fd84319d9dad1009e3cbdb643cea9272
--- /dev/null
+++ b/src/plugins/region/tests/region/swap.i
@@ -0,0 +1,29 @@
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region A: *a, B: *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_separated(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
+
+/*@
+ requires \valid(a);
+ requires \valid(b);
+ region R: *a, *b;
+ ensures *a == \old(*b);
+ ensures *b == \old(*a);
+ assigns *a, *b;
+ */
+void swap_aliased(int *a, int *b)
+{
+ int tmp = *a ;
+ *a = *b;
+ *b = tmp ;
+}
diff --git a/src/plugins/region/tests/test_config b/src/plugins/region/tests/test_config
new file mode 100644
index 0000000000000000000000000000000000000000..4772d6b36660012dd7b95cfdc8bed12676c83fb1
--- /dev/null
+++ b/src/plugins/region/tests/test_config
@@ -0,0 +1,2 @@
+PLUGIN: region
+OPT: -region