diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml index dd4561560a3c2d839554448924670aa65437006b..f2697affd43569089fda263bbf4cb02213b1f987 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 e141f13431ac5907cd8a06d8b5d17392d761195d..2312dafd8a402817ff5cc572dee05384826bd01c 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 e684198b0e99768b84e7c3cf7aa9135e77220c27..fb6d84c2cb8cf463ae9e13dd1b6a159325899843 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 e684198b0e99768b84e7c3cf7aa9135e77220c27..fb6d84c2cb8cf463ae9e13dd1b6a159325899843 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 e7b235b05c2dae8fb2c2fc358b0b5a3b69461907..bf3da7a503c8df46be495fd87a2d73c2c600b6c6 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 1bc2f1baac572e05e322c75b69d676f993d21501..be59f8c030d72f6deb45f68ddcb7e2102e840a61 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 2c939c92e0be417532ac6033f0fa9de7dc04779f..dc378f6d5e6eab79016343050256ad68545f2b7e 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 f5a79d97a696e5ab2ffd3fa2afcb28cd44a2fa1c..72629334e8a760da79b4436a7880cd15e41da5aa 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 07f96795974121ec4b16386336d86296438694fc..11a2a15408554226d844aa54f49e22a8df444ae6 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 474cab2dd54d19aa8f53bb0618ac98aaec6ec373..e8fb0e753eb65c3fb5fd35c27ba3bd74b16cf5e9 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++) {