From d4af1830b30c48e0038c61336a172a50d2ac6cd2 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 11 Jun 2024 17:14:50 +0200
Subject: [PATCH] [wp] renamed (old) region annotations
---
src/plugins/wp/RegionAnnot.ml | 4 ++--
src/plugins/wp/tests/wp_region/annot.i | 8 ++++----
src/plugins/wp/tests/wp_region/annot/a.i | 10 ++++------
src/plugins/wp/tests/wp_region/annot/b.i | 10 ++++------
src/plugins/wp/tests/wp_region/array1.i | 2 +-
src/plugins/wp/tests/wp_region/array2.i | 2 +-
src/plugins/wp/tests/wp_region/fb_ADD.i | 2 +-
src/plugins/wp/tests/wp_region/fb_SORT.i | 8 ++++----
src/plugins/wp/tests/wp_region/oracle/annot.res.oracle | 8 ++++----
src/plugins/wp/tests/wp_region/structarray1.i | 2 +-
10 files changed, 26 insertions(+), 30 deletions(-)
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
index dd4561560a3..f2697affd43 100644
--- a/src/plugins/wp/RegionAnnot.ml
+++ b/src/plugins/wp/RegionAnnot.ml
@@ -468,7 +468,7 @@ let typecheck typing_context _loc ps =
let of_extid = Hashtbl.find registry
let of_extrev = function
- | { ext_name="region" ; ext_kind = Ext_id k } -> of_extid k
+ | { ext_name="wpregion" ; ext_kind = Ext_id k } -> of_extid k
| _ -> raise Not_found
let of_extension e = List.rev (of_extrev e)
let of_behavior bhv =
@@ -498,7 +498,7 @@ let register () =
then
begin
registered := true ;
- Acsl_extension.register_behavior ~plugin:"wp" "region"
+ Acsl_extension.register_behavior ~plugin:"wp" "wpregion"
typecheck ~printer:pp_extension false
end
diff --git a/src/plugins/wp/tests/wp_region/annot.i b/src/plugins/wp/tests/wp_region/annot.i
index e141f13431a..2312dafd8a4 100644
--- a/src/plugins/wp/tests/wp_region/annot.i
+++ b/src/plugins/wp/tests/wp_region/annot.i
@@ -31,7 +31,7 @@ typedef struct Block {
SN sum ;
} FB ;
-//@ \wp::region *fb ;
+//@ \wp::wpregion *fb ;
void fb_ADD(FB *fb)
{
fb->out1->v = fb->out1->v + fb->out2->v ;
@@ -39,9 +39,9 @@ void fb_ADD(FB *fb)
}
/*@
- \wp::region IN: (fb->inp1 .. fb->inp3), \pattern{PMEM} ;
- \wp::region OUT: (fb->out1 .. fb->out3), \pattern{PVECTOR} ;
- \wp::region IDX: (fb->idx1 .. fb->idx3), \pattern{PVECTOR} ;
+ \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)
{
diff --git a/src/plugins/wp/tests/wp_region/annot/a.i b/src/plugins/wp/tests/wp_region/annot/a.i
index e684198b0e9..fb6d84c2cb8 100644
--- a/src/plugins/wp/tests/wp_region/annot/a.i
+++ b/src/plugins/wp/tests/wp_region/annot/a.i
@@ -24,7 +24,7 @@ struct Block {
};
typedef struct Block FB;
/*@ terminates \true;
- \wp::region *fb; */
+ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
}
/*@ terminates \true;
- \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
- \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
- \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+ \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)
{
@@ -56,5 +56,3 @@ void fb_SORT(FB *fb)
(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
index e684198b0e9..fb6d84c2cb8 100644
--- a/src/plugins/wp/tests/wp_region/annot/b.i
+++ b/src/plugins/wp/tests/wp_region/annot/b.i
@@ -24,7 +24,7 @@ struct Block {
};
typedef struct Block FB;
/*@ terminates \true;
- \wp::region *fb; */
+ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -33,9 +33,9 @@ void fb_ADD(FB *fb)
}
/*@ terminates \true;
- \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
- \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
- \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+ \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)
{
@@ -56,5 +56,3 @@ void fb_SORT(FB *fb)
(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
index e7b235b05c2..bf3da7a503c 100644
--- a/src/plugins/wp/tests/wp_region/array1.i
+++ b/src/plugins/wp/tests/wp_region/array1.i
@@ -1,4 +1,4 @@
-//@ \wp::region *p, *q ;
+//@ \wp::wpregion *p, *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
diff --git a/src/plugins/wp/tests/wp_region/array2.i b/src/plugins/wp/tests/wp_region/array2.i
index 1bc2f1baac5..be59f8c030d 100644
--- a/src/plugins/wp/tests/wp_region/array2.i
+++ b/src/plugins/wp/tests/wp_region/array2.i
@@ -1,4 +1,4 @@
-//@ \wp::region *p; \wp::region *q ;
+//@ \wp::wpregion *p; \wp::wpregion *q ;
int job( int n, int * p , int * q )
{
int s = 0 ;
diff --git a/src/plugins/wp/tests/wp_region/fb_ADD.i b/src/plugins/wp/tests/wp_region/fb_ADD.i
index 2c939c92e0b..dc378f6d5e6 100644
--- a/src/plugins/wp/tests/wp_region/fb_ADD.i
+++ b/src/plugins/wp/tests/wp_region/fb_ADD.i
@@ -16,7 +16,7 @@ typedef struct Block {
} FB ;
/*@
- \wp::region A: fb ;
+ \wp::wpregion A: fb ;
*/
void job(FB *fb)
{
diff --git a/src/plugins/wp/tests/wp_region/fb_SORT.i b/src/plugins/wp/tests/wp_region/fb_SORT.i
index f5a79d97a69..72629334e8a 100644
--- a/src/plugins/wp/tests/wp_region/fb_SORT.i
+++ b/src/plugins/wp/tests/wp_region/fb_SORT.i
@@ -16,10 +16,10 @@ typedef struct Block {
} FB ;
/*@
- \wp::region Shared: *(fb->inp1 .. fb->inp3);
- \wp::region IN: (fb->inp1 .. fb->inp3);
- \wp::region OUT: (fb->out1 .. fb->out3);
- \wp::region IDX: (fb->idx1 .. fb->idx3);
+ \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)
{
diff --git a/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle b/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle
index 07f96795974..11a2a154085 100644
--- a/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle
+++ b/src/plugins/wp/tests/wp_region/oracle/annot.res.oracle
@@ -24,7 +24,7 @@ struct Block {
SN sum ;
};
typedef struct Block FB;
-/*@ \wp::region *fb; */
+/*@ \wp::wpregion *fb; */
void fb_ADD(FB *fb)
{
(fb->out1)->v += (fb->out2)->v;
@@ -32,9 +32,9 @@ void fb_ADD(FB *fb)
return;
}
-/*@ \wp::region IN: \pattern{PMEM}, (fb->inp1..fb->inp3);
- \wp::region OUT: \pattern{PVECTOR}, (fb->out1..fb->out3);
- \wp::region IDX: \pattern{PVECTOR}, (fb->idx1..fb->idx3);
+/*@ \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)
{
diff --git a/src/plugins/wp/tests/wp_region/structarray1.i b/src/plugins/wp/tests/wp_region/structarray1.i
index 474cab2dd54..e8fb0e753eb 100644
--- a/src/plugins/wp/tests/wp_region/structarray1.i
+++ b/src/plugins/wp/tests/wp_region/structarray1.i
@@ -6,7 +6,7 @@ typedef struct Matrix {
int coef[4][4];
} * matrix ;
-//@ \wp::region *X , *R ;
+//@ \wp::wpregion *X , *R ;
void job( matrix M , vector X , vector R )
{
for (int i = 0; i < 4; i++) {
--
GitLab