diff --git a/ivette/src/frama-c/kernel/api/parameters/index.ts b/ivette/src/frama-c/kernel/api/parameters/index.ts
index f42b08cf6cd7c4df096be969b4b1ff93861bacd4..8fca8d4066e468e70fbdc1f924826e08a4a5b41a 100644
--- a/ivette/src/frama-c/kernel/api/parameters/index.ts
+++ b/ivette/src/frama-c/kernel/api/parameters/index.ts
@@ -8284,294 +8284,6 @@ const wpModel_internal: State.State<string> = {
/** State of parameter -wp-model */
export const wpModel: State.State<string> = wpModel_internal;
-/** Signal for state [`regionAnnot`](#regionannot) */
-export const signalRegionAnnot: Server.Signal = {
- name: 'kernel.parameters.signalRegionAnnot',
-};
-
-const getRegionAnnot_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getRegionAnnot',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`regionAnnot`](#regionannot) */
-export const getRegionAnnot: Server.GetRequest<null,boolean>= getRegionAnnot_internal;
-
-const setRegionAnnot_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setRegionAnnot',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`regionAnnot`](#regionannot) */
-export const setRegionAnnot: Server.SetRequest<boolean,null>= setRegionAnnot_internal;
-
-const regionAnnot_internal: State.State<boolean> = {
- name: 'kernel.parameters.regionAnnot',
- signal: signalRegionAnnot,
- getter: getRegionAnnot,
- setter: setRegionAnnot,
-};
-/** State of parameter -region-annot */
-export const regionAnnot: State.State<boolean> = regionAnnot_internal;
-
-/** Signal for state [`wpRegionFlat`](#wpregionflat) */
-export const signalWpRegionFlat: Server.Signal = {
- name: 'kernel.parameters.signalWpRegionFlat',
-};
-
-const getWpRegionFlat_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegionFlat',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegionFlat`](#wpregionflat) */
-export const getWpRegionFlat: Server.GetRequest<null,boolean>= getWpRegionFlat_internal;
-
-const setWpRegionFlat_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegionFlat',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegionFlat`](#wpregionflat) */
-export const setWpRegionFlat: Server.SetRequest<boolean,null>= setWpRegionFlat_internal;
-
-const wpRegionFlat_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegionFlat',
- signal: signalWpRegionFlat,
- getter: getWpRegionFlat,
- setter: setWpRegionFlat,
-};
-/** State of parameter -wp-region-flat */
-export const wpRegionFlat: State.State<boolean> = wpRegionFlat_internal;
-
-/** Signal for state [`wpRegionPack`](#wpregionpack) */
-export const signalWpRegionPack: Server.Signal = {
- name: 'kernel.parameters.signalWpRegionPack',
-};
-
-const getWpRegionPack_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegionPack',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegionPack`](#wpregionpack) */
-export const getWpRegionPack: Server.GetRequest<null,boolean>= getWpRegionPack_internal;
-
-const setWpRegionPack_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegionPack',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegionPack`](#wpregionpack) */
-export const setWpRegionPack: Server.SetRequest<boolean,null>= setWpRegionPack_internal;
-
-const wpRegionPack_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegionPack',
- signal: signalWpRegionPack,
- getter: getWpRegionPack,
- setter: setWpRegionPack,
-};
-/** State of parameter -wp-region-pack */
-export const wpRegionPack: State.State<boolean> = wpRegionPack_internal;
-
-/** Signal for state [`wpRegionRw`](#wpregionrw) */
-export const signalWpRegionRw: Server.Signal = {
- name: 'kernel.parameters.signalWpRegionRw',
-};
-
-const getWpRegionRw_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegionRw',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegionRw`](#wpregionrw) */
-export const getWpRegionRw: Server.GetRequest<null,boolean>= getWpRegionRw_internal;
-
-const setWpRegionRw_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegionRw',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegionRw`](#wpregionrw) */
-export const setWpRegionRw: Server.SetRequest<boolean,null>= setWpRegionRw_internal;
-
-const wpRegionRw_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegionRw',
- signal: signalWpRegionRw,
- getter: getWpRegionRw,
- setter: setWpRegionRw,
-};
-/** State of parameter -wp-region-rw */
-export const wpRegionRw: State.State<boolean> = wpRegionRw_internal;
-
-/** Signal for state [`wpRegionInline`](#wpregioninline) */
-export const signalWpRegionInline: Server.Signal = {
- name: 'kernel.parameters.signalWpRegionInline',
-};
-
-const getWpRegionInline_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegionInline',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegionInline`](#wpregioninline) */
-export const getWpRegionInline: Server.GetRequest<null,boolean>= getWpRegionInline_internal;
-
-const setWpRegionInline_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegionInline',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegionInline`](#wpregioninline) */
-export const setWpRegionInline: Server.SetRequest<boolean,null>= setWpRegionInline_internal;
-
-const wpRegionInline_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegionInline',
- signal: signalWpRegionInline,
- getter: getWpRegionInline,
- setter: setWpRegionInline,
-};
-/** State of parameter -wp-region-inline */
-export const wpRegionInline: State.State<boolean> = wpRegionInline_internal;
-
-/** Signal for state [`wpRegionCluster`](#wpregioncluster) */
-export const signalWpRegionCluster: Server.Signal = {
- name: 'kernel.parameters.signalWpRegionCluster',
-};
-
-const getWpRegionCluster_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegionCluster',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegionCluster`](#wpregioncluster) */
-export const getWpRegionCluster: Server.GetRequest<null,boolean>= getWpRegionCluster_internal;
-
-const setWpRegionCluster_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegionCluster',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegionCluster`](#wpregioncluster) */
-export const setWpRegionCluster: Server.SetRequest<boolean,null>= setWpRegionCluster_internal;
-
-const wpRegionCluster_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegionCluster',
- signal: signalWpRegionCluster,
- getter: getWpRegionCluster,
- setter: setWpRegionCluster,
-};
-/** State of parameter -wp-region-cluster */
-export const wpRegionCluster: State.State<boolean> = wpRegionCluster_internal;
-
-/** Signal for state [`wpRegionFixpoint`](#wpregionfixpoint) */
-export const signalWpRegionFixpoint: Server.Signal = {
- name: 'kernel.parameters.signalWpRegionFixpoint',
-};
-
-const getWpRegionFixpoint_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegionFixpoint',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegionFixpoint`](#wpregionfixpoint) */
-export const getWpRegionFixpoint: Server.GetRequest<null,boolean>= getWpRegionFixpoint_internal;
-
-const setWpRegionFixpoint_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegionFixpoint',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegionFixpoint`](#wpregionfixpoint) */
-export const setWpRegionFixpoint: Server.SetRequest<boolean,null>= setWpRegionFixpoint_internal;
-
-const wpRegionFixpoint_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegionFixpoint',
- signal: signalWpRegionFixpoint,
- getter: getWpRegionFixpoint,
- setter: setWpRegionFixpoint,
-};
-/** State of parameter -wp-region-fixpoint */
-export const wpRegionFixpoint: State.State<boolean> = wpRegionFixpoint_internal;
-
-/** Signal for state [`wpRegion`](#wpregion) */
-export const signalWpRegion: Server.Signal = {
- name: 'kernel.parameters.signalWpRegion',
-};
-
-const getWpRegion_internal: Server.GetRequest<null,boolean> = {
- kind: Server.RqKind.GET,
- name: 'kernel.parameters.getWpRegion',
- input: Json.jNull,
- output: Json.jBoolean,
- fallback: false,
- signals: [],
-};
-/** Getter for state [`wpRegion`](#wpregion) */
-export const getWpRegion: Server.GetRequest<null,boolean>= getWpRegion_internal;
-
-const setWpRegion_internal: Server.SetRequest<boolean,null> = {
- kind: Server.RqKind.SET,
- name: 'kernel.parameters.setWpRegion',
- input: Json.jBoolean,
- output: Json.jNull,
- fallback: null,
- signals: [],
-};
-/** Setter for state [`wpRegion`](#wpregion) */
-export const setWpRegion: Server.SetRequest<boolean,null>= setWpRegion_internal;
-
-const wpRegion_internal: State.State<boolean> = {
- name: 'kernel.parameters.wpRegion',
- signal: signalWpRegion,
- getter: getWpRegion,
- setter: setWpRegion,
-};
-/** State of parameter -wp-region */
-export const wpRegion: State.State<boolean> = wpRegion_internal;
-
/** Signal for state [`wpWhy3ExtraConfig`](#wpwhy3extraconfig) */
export const signalWpWhy3ExtraConfig: Server.Signal = {
name: 'kernel.parameters.signalWpWhy3ExtraConfig',
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 303cbaecda2f4dd3c6fdcb11de0957c2eab4c1c8..322dcfd08e9b6ae33b81668cce69d067f8ff5689 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -24,7 +24,8 @@
Plugin WP <next-release>
###############################################################################
-* WP [2024-07-02] Fixed parsing of decimal literals
+-! WP [2024-08-23] Remove wp_region
+-* WP [2024-07-02] Fixed parsing of decimal literals
###############################################################################
Plugin WP 29.0 (Copper)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 6c66a582bf1367a4012415a32b106f6c75267bb4..488ce673bc4bf6c3da09f5ec1d0545ed45297c8b 100644
--- a/src/plugins/wp/Factory.ml
+++ b/src/plugins/wp/Factory.ml
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
+type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva
type mvar = Raw | Var | Ref | Caveat
type setup = {
@@ -64,7 +64,6 @@ let descr_mtyped d = function
| MemTyped.Fits -> ()
let descr_mheap d = function
- | Region -> main d "region"
| ZeroAlias -> main d "zeroalias"
| Hoare -> main d "hoare"
| Typed p -> main d "typed" ; descr_mtyped d p
@@ -218,7 +217,6 @@ struct
module A = LogicAssigns.Make(M)(L)
end
-module Comp_Region = MakeCompiler(Register(MemVar.Static)(MemRegion))
module Comp_MemZeroAlias = MakeCompiler(MemZeroAlias)
module Comp_Hoare_Raw = MakeCompiler(Model_Hoare_Raw)
module Comp_Hoare_Ref = MakeCompiler(Model_Hoare_Ref)
@@ -232,7 +230,6 @@ module Comp_MemVal = MakeCompiler(MemVal)
let compiler mheap mvar : (module Sigs.Compiler) =
match mheap , mvar with
| ZeroAlias , _ -> (module Comp_MemZeroAlias)
- | Region , _ -> (module Comp_Region)
| _ , Caveat -> (module Comp_Caveat)
| Hoare , (Raw|Var) -> (module Comp_Hoare_Raw)
| Hoare , Ref -> (module Comp_Hoare_Ref)
@@ -248,7 +245,6 @@ let compiler mheap mvar : (module Sigs.Compiler) =
let configure_mheap = function
| Hoare -> MemEmpty.configure ()
| ZeroAlias -> MemZeroAlias.configure ()
- | Region -> MemRegion.configure ()
| Eva -> MemVal.configure ()
| Typed p ->
let rollback_memtyped = MemTyped.configure () in
@@ -329,7 +325,6 @@ let split ~warning (m:string) : string list =
let update_config ~warning m s = function
| "ZEROALIAS" -> { s with mheap = ZeroAlias }
- | "REGION" -> { s with mheap = Region }
| "HOARE" -> { s with mheap = Hoare }
| "TYPED" -> { s with mheap = Typed MemTyped.Fits }
| "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
diff --git a/src/plugins/wp/Factory.mli b/src/plugins/wp/Factory.mli
index eaa02b38e678049a00ff835a010c649e115e3b88..dc9e29707e3241907c83617588ce6900b2d4fcec 100644
--- a/src/plugins/wp/Factory.mli
+++ b/src/plugins/wp/Factory.mli
@@ -24,7 +24,7 @@
(* --- Model Factory --- *)
(* -------------------------------------------------------------------------- *)
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
+type mheap = Hoare | ZeroAlias | Typed of MemTyped.pointer | Eva
type mvar = Raw | Var | Ref | Caveat
type setup = {
diff --git a/src/plugins/wp/Layout.ml b/src/plugins/wp/Layout.ml
index 39b59cd426aa54145b25cf23dbd39b524abe6358..6661a8ddf21a976e0af492d6de048f1fd766eb88 100644
--- a/src/plugins/wp/Layout.ml
+++ b/src/plugins/wp/Layout.ml
@@ -216,15 +216,6 @@ struct
end
-module Mode(OPT : sig val get : unit -> bool end) =
-struct
- let default = OPT.get
- let merge a b = if default () then a && b else a || b
-end
-
-module RW = Mode(Wp.Region_rw)
-module Flat = Mode(Wp.Region_flat)
-module Pack = Mode(Wp.Region_pack)
(* -------------------------------------------------------------------------- *)
(* --- Data Layout --- *)
diff --git a/src/plugins/wp/Layout.mli b/src/plugins/wp/Layout.mli
index 5370aa2299e1ca43c79644f52c12c27e6815f7ac..1db68dd9fa0d75eb25f20a5d3b97a0f49f655595 100644
--- a/src/plugins/wp/Layout.mli
+++ b/src/plugins/wp/Layout.mli
@@ -261,25 +261,4 @@ end
(** {2 Options} *)
(* -------------------------------------------------------------------------- *)
-(** Read-Write access *)
-module RW :
-sig
- val default : unit -> bool
- val merge : bool -> bool -> bool
-end
-
-(** Flatten arrays *)
-module Flat :
-sig
- val default : unit -> bool
- val merge : bool -> bool -> bool
-end
-
-(** Pack fields *)
-module Pack :
-sig
- val default : unit -> bool
- val merge : bool -> bool -> bool
-end
-
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
deleted file mode 100644
index 9ff7c488921994ae1b68c5b8908b621a091713ea..0000000000000000000000000000000000000000
--- a/src/plugins/wp/MemRegion.ml
+++ /dev/null
@@ -1,898 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* TODO DEVEL MODE *)
-[@@@ warning "-32-37-60"]
-
-(* -------------------------------------------------------------------------- *)
-(* --- Region Memory Model --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Cil_types
-open Sigs
-open Definitions
-
-module Wp = Wp_parameters
-module F = Lang.F
-module L = Qed.Logic
-
-(* -------------------------------------------------------------------------- *)
-(* --- Why-3 Region Theory --- *)
-(* -------------------------------------------------------------------------- *)
-
-let library = "region"
-
-let cluster_region () =
- Definitions.cluster ~id:"Region" ~title:"Region Index Constructors" ()
-
-(* Index *)
-let t_addr = MemAddr.t_addr
-let t_index = L.Data( Lang.datatype ~library "index" ,[] )
-let f_addrof = Lang.extern_f ~library ~result:t_addr "addrof"
-let f_consistent = Lang.extern_fp ~library "consistent"
-let f_consistent_range = Lang.extern_fp ~library "consistent_range"
-
-let a_addrof l = F.e_fun f_addrof [l]
-let p_consistent l = F.p_call f_consistent [l]
-let p_consistent_range l n = F.p_call f_consistent_range [l;n]
-let p_range k n ps = F.(p_leq e_zero k :: p_lt k n :: ps)
-
-(* Null *)
-let f_inull = Lang.extern_f ~library ~result:t_index "inull"
-let l_inull = F.e_fun f_inull []
-let p_inull l = F.p_equal MemAddr.null (a_addrof l)
-
-(* Constructors *)
-let region_ctor ~result =
- Lang.extern_f ~library ~category:L.Constructor ~result "%s"
-
-let f_addr_var = region_ctor ~result:t_addr "addr_var"
-let f_addr_ref = region_ctor ~result:t_addr "addr_ref"
-let f_base_var = region_ctor ~result:L.Int "base_var"
-let f_base_ref = region_ctor ~result:L.Int "base_ref"
-let f_index_var = region_ctor ~result:t_index "index_var"
-let f_index_ref = region_ctor ~result:t_index "index_ref"
-let f_index_mem = region_ctor ~result:t_index "index_mem"
-
-let a_addr_var x = F.e_fun f_addr_var [x]
-let a_addr_ref p = F.e_fun f_addr_ref [p]
-let l_index_var x = F.e_fun f_index_var [F.e_int x]
-let l_index_mem l k n = F.e_fun f_index_ref [l;k;n]
-let l_index_ref l = F.e_fun f_index_ref [l]
-
-(* Shifts *)
-
-let f_shift_index = Lang.extern_f ~library ~result:t_index "shift_index"
-let l_shift_index l p = F.e_fun f_shift_index [l;p]
-
-(* Bits *)
-let t_bits = L.Int
-
-(* -------------------------------------------------------------------------- *)
-(* --- Index Simplifiers --- *)
-(* -------------------------------------------------------------------------- *)
-
-type index_builtin = {
- index: (Lang.lfun -> F.term list -> F.term -> F.term) ;
- addrof : (F.term list -> F.term) ;
- consistent : (F.term list -> F.pred) ;
-}
-
-module IndexBuiltin = WpContext.Static
- (struct
- type key = Lang.lfun
- type data = index_builtin
- let name = "MemRegion.INDEXER"
- include Lang.Fun
- end)
-
-(* f enjoys shifting props:
- - f(l,p,...)+k == f(l,p+k,...)
- - &f(l,p,...) = &l+p
-*)
-let is_shiftable f =
- ( f == f_shift_index ) || ( f == f_index_mem)
-
-let phi_addrof index =
- match F.repr index with
- | L.Fun(f,[]) when f == f_inull -> MemAddr.null
- | L.Fun(f,[x]) when f == f_index_var -> a_addr_var x
- | L.Fun(f,[l]) when f == f_index_ref -> a_addr_ref (a_addrof l)
- | L.Fun(f,l::p::_) when is_shiftable f -> MemAddr.shift (a_addrof l) p
- | L.Fun(f,es) -> (IndexBuiltin.find f).addrof es
- | _ -> raise Not_found
-
-let phi_shift_index l p =
- if p == F.e_zero then l else
- match F.repr l with
- | L.Fun(f,l::q::w) when is_shiftable f -> F.e_fun f (l::(F.e_add p q)::w)
- | L.Fun(f,es) -> (IndexBuiltin.find f).index f es p
- | _ -> raise Not_found
-
-let phi_consistent index =
- match F.repr index with
- | L.Fun(f,[]) when f == f_inull -> F.e_false
- | L.Fun(f,[x]) when f == f_index_var ->
- F.e_neq x F.e_zero
- | L.Fun(f,[l]) when f == f_index_ref ->
- F.e_prop @@ p_consistent l
- | L.Fun(f,[l;k;n]) when f == f_index_mem ->
- F.e_prop @@ F.p_conj @@ p_range k n [p_consistent l]
- | L.Fun(f,es) ->
- F.e_prop @@ (IndexBuiltin.find f).consistent es
- | _ -> raise Not_found
-
-let phi_consistent_range index sizeof =
- match F.repr index with
- | L.Fun(f,[l;k;n]) when f == f_index_mem ->
- F.e_prop @@ F.p_conj @@ F.[
- p_leq e_zero sizeof ;
- p_leq e_zero k ;
- p_leq (e_add k sizeof) n ;
- p_consistent l ;
- ]
- | _ -> raise Not_found
-
-let () = Context.register
- begin fun () ->
- MemAddr.register f_addr_var
- ~base:(F.e_fun f_base_var) ~offset:(fun _ -> F.e_zero) ;
- MemAddr.register f_addr_ref
- ~base:(F.e_fun f_base_ref) ;
- F.set_builtin_1 f_addrof phi_addrof ;
- F.set_builtin_1 f_consistent phi_consistent ;
- F.set_builtin_2 f_shift_index phi_shift_index ;
- F.set_builtin_2 f_consistent_range phi_consistent_range ;
- end
-
-let cid = ref 0 (* TODO: projectified *)
-
-let constructor ~basename ~params ~index ~addrof ~consistent =
- let id = incr cid ; !cid in
- let lfun = Lang.generated_f ~result:t_index "%s_%d" basename id in
- let ps = List.map F.e_var params in
- let l = F.e_fun lfun ps in
- let k = Lang.freshvar ~basename:"k" L.Int in
- let ofs = F.e_var k in
- (* Must compute properties before registering simplifiers *)
- let p_addrof = F.p_equal (a_addrof l) (addrof ps) in
- let p_consistent = F.p_equiv (p_consistent l) (consistent ps) in
- let p_index = F.p_equal (l_shift_index l ofs) (index lfun ps ofs) in
- IndexBuiltin.define lfun { index ; addrof ; consistent } ;
- fun cluster ->
- begin
- Definitions.define_symbol {
- d_cluster = cluster ;
- d_lfun = lfun ; d_params = params ; d_types = 0 ;
- d_definition = Logic t_index ;
- } ;
- Definitions.define_lemma {
- l_cluster = cluster ;
- l_kind = Admit ;
- l_name = Printf.sprintf "addrof_%s_%d" basename id ;
- l_forall = params ; l_triggers = [] ;
- l_lemma = p_addrof ;
- } ;
- Definitions.define_lemma {
- l_cluster = cluster ;
- l_kind = Admit ;
- l_name = Printf.sprintf "consistent_%s_%d" basename id ;
- l_forall = params ; l_triggers = [] ;
- l_lemma = p_consistent ;
- } ;
- if p_index != F.p_true then
- Definitions.define_lemma {
- l_cluster = cluster ;
- l_kind = Admit ;
- l_name = Printf.sprintf "index_%s_%d" basename id ;
- l_forall = params @ [k] ; l_triggers = [] ;
- l_lemma = p_index ;
- } ;
- lfun
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Field Index Constructors --- *)
-(* -------------------------------------------------------------------------- *)
-
-module FIELD =
-struct
-
- type t = int list (* Overlay offsets *)
-
- let pretty fmt = function
- | [] -> Format.fprintf fmt "{}"
- | p::ps ->
- begin
- Format.fprintf fmt "@[<hov 2>{%d" p ;
- List.iter (fun p -> Format.fprintf fmt ",@,%d" p) ps ;
- Format.fprintf fmt "}@]" ;
- end
-
- let compare = Stdlib.compare
-
- (* Extract constant offset *)
- let offset k =
- let rec walk s a =
- match F.repr a with
- | L.Add es -> List.fold_left walk s es
- | L.Kint z ->
- (try s + Integer.to_int_exn z
- with Z.Overflow -> s)
- | _ -> s
- in walk 0 k
-
- let builtin_index f es q = match es with
- | [l;p] -> F.e_fun f [l;F.e_add q p]
- | _ -> raise Not_found
-
- let builtin_addrof = function
- | [l;p] -> MemAddr.shift (a_addrof l) p
- | _ -> raise Not_found
-
- let builtin_consistent fds = function
- | [l;p] -> F.p_and (p_consistent l)
- (F.p_any (fun fd -> F.p_equal (F.e_int fd) p) fds)
- | _ -> raise Not_found
-
-end
-
-(* Model Independant Generators *)
-module FIELD_GEN = WpContext.StaticGenerator(FIELD)
- (struct
- type key = FIELD.t
- type data = cluster -> Lang.lfun
- let name = "MemRegion.FIELD_GEN"
- let compile fds =
- let l = Lang.freshvar ~basename:"l" t_index in
- let p = Lang.freshvar ~basename:"p" L.Int in
- constructor
- ~basename:"field"
- ~params:[l;p]
- ~index:FIELD.builtin_index
- ~addrof:FIELD.builtin_addrof
- ~consistent:(FIELD.builtin_consistent fds)
- end)
-
-(* Model Dependent Definitions *)
-module FIELD_MODEL = WpContext.Generator(FIELD)
- (struct
- type key = FIELD.t
- type data = Lang.lfun
- let name = "MemRegion.FIELD_MODEL"
- let compile fds = FIELD_GEN.get fds @@ cluster_region ()
- end)
-
-let l_field ovl l k =
- let fds = List.map (fun rg -> rg.Layout.ofs) ovl in
- F.e_fun (FIELD_MODEL.get fds) [l;k]
-
-(* -------------------------------------------------------------------------- *)
-(* --- Array Index Constructors --- *)
-(* -------------------------------------------------------------------------- *)
-
-module ARRAY =
-struct
-
- type t = int * int list
- let compare = Stdlib.compare
- let pretty fmt (s,ds) = Format.fprintf fmt "%d%a" s Layout.Matrix.pretty ds
-
- (* Coefficient from Matrix dimensions: c_i = \Pi_{i<j} d_j *)
- let coefs s ds =
- let rec walk cs s = function
- | d::ds -> walk (s::cs) (d*s) ds
- | [] -> cs
- in walk [] s ds
-
- (* All zeroes *)
- let zeroes = List.map (fun _ -> F.e_zero)
-
- (* Address shift with coefficient c_i for each index k_i *)
- let rec shift a cs ks =
- match cs , ks with
- | c::cs , k::ks -> shift (MemAddr.shift a (F.e_fact c k)) cs ks
- | _ -> a
-
- (* Address of an array index *)
- let builtin_addrof cs = function
- | l::ks -> shift (a_addrof l) cs ks
- | _ -> raise Not_found
-
- (* Add conditions (0 <= ki < ni) to [ps].
- WARNING: ns = rev ds *)
- let rec add_range_dims ps ks ns =
- match ks , ns with
- | k::ks , n::ns ->
- add_range_dims F.(p_range k (e_int n) ps) ks ns
- | k::ks , [] ->
- add_range_dims F.(p_equal e_zero k :: ps) ks []
- | [] , _ -> ps
-
- (* Consistent index.
- WARNING: ns = rev ds *)
- let builtin_consistent ns = function
- | l::ks -> F.p_conj (add_range_dims [p_consistent l] ks ns)
- | _ -> raise Not_found
-
- (* Extract linear forms *)
- let rec get_linear poly a =
- match F.repr a with
- | L.Add es -> List.fold_left get_linear poly es
- | L.Kint z ->
- (try (Integer.to_int_exn z,F.e_one)::poly
- with Z.Overflow -> (1,a)::poly)
- | L.Times(c,e) ->
- (try (Integer.to_int_exn c,e)::poly
- with Z.Overflow -> (1,a)::poly)
- | _ -> (1,a)::poly
-
- (* Some of linear form *)
- let rec add_linear s = function
- | (k,e)::poly -> add_linear (F.e_add s (F.e_fact k e)) poly
- | [] -> s
-
- (* Euclidian division *)
- (* euclid q r ci p = q',r' <-> p + ci.q + r = ci.q' + r' *)
- let rec euclid q r ci = function
- | [] -> q,r
- | (c,k)::poly ->
- let q0 = c / ci in
- let r0 = c mod ci in
- euclid (F.e_add q (F.e_fact q0 k)) ((r0,k)::r) ci poly
-
- (* Linear offset decomposed on each coefficient *)
- let rec add_linear_index cs ks ks' p =
- match cs , ks with
- | c :: cs , k :: ks ->
- let k' , r = euclid k [] c p in
- add_linear_index cs ks (k'::ks') r
- | _ -> List.rev_append ks' ks , p
-
- (* Linear offset and remainder delta *)
- let offset cs ks p =
- let ks',r = add_linear_index cs ks [] (get_linear [] p) in
- ks' , add_linear F.e_zero r
-
- (* Builtin simplifier *)
- let builtin_index cs f es p = match es with
- | l::ks ->
- let ks' , r = offset cs ks p in
- if Qed.Hcons.equal_list F.equal ks ks' then
- raise Not_found
- else
- let l' = F.e_fun f (l :: ks) in
- l_shift_index l' r
- | _ -> raise Not_found
-
-end
-
-module ARRAY_GEN = WpContext.StaticGenerator(ARRAY)
- (struct
- type key = ARRAY.t
- type data = (cluster -> Lang.lfun)
- let name = "MemRegion.ARRAY_GEN"
- let compile (s,ds) =
- let l = Lang.freshvar ~basename:"l" t_index in
- let ks = List.map (fun _ -> Lang.freshvar ~basename:"k" L.Int) ds in
- let cs = ARRAY.coefs s ds in
- let ns = List.rev ds in
- constructor
- ~basename:"array"
- ~params:(l::ks)
- ~index:(ARRAY.builtin_index cs)
- ~addrof:(ARRAY.builtin_addrof cs)
- ~consistent:(ARRAY.builtin_consistent ns)
- end)
-
-module ARRAY_MODEL = WpContext.Generator(ARRAY)
- (struct
- type key = ARRAY.t
- type data = Lang.lfun
- let name = "MemRegion.ARRAY_MODEL"
- let compile dim = ARRAY_GEN.get dim @@ cluster_region ()
- end)
-
-let l_array s ds l ks = F.e_fun (ARRAY_MODEL.get (s,ds)) (l::ks)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Model Context --- *)
-(* -------------------------------------------------------------------------- *)
-
-let datatype = "MemRegion"
-
-let configure () =
- begin
- let orig_pointer = Context.push Lang.pointer t_index in
- let orig_null = Context.push Cvalues.null p_inull in
- let rollback () =
- Context.pop Lang.pointer orig_pointer ;
- Context.pop Cvalues.null orig_null
- in
- rollback
- end
-
-let configure_ia =
- let no_binder = { bind = fun _ f v -> f v } in
- fun _vertex -> no_binder
-
-let hypotheses p = p
-
-let error msg = Warning.error ~source:"Region Model" msg
-
-(* -------------------------------------------------------------------------- *)
-(* --- Region Maps --- *)
-(* -------------------------------------------------------------------------- *)
-
-let map () =
- RegionAnalysis.get
- begin match WpContext.get_scope () with
- | WpContext.Global -> None
- | WpContext.Kf kf -> Some kf
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Locations --- *)
-(* -------------------------------------------------------------------------- *)
-
-open Layout
-
-type region = Region.region
-type index = F.term
-
-let pp_index = F.pp_term
-let pp_region = Region.R.pretty
-let pp_value = Value.pretty pp_region
-let pp_args fmt = function
- | [] -> ()
- | k::ks ->
- F.pp_term fmt k ;
- List.iter (fun k -> Format.fprintf fmt "@,,%a" F.pp_term k) ks
-
-let pp_field fmt k =
- if F.is_atomic k then
- Format.fprintf fmt "@,+%a" F.pp_term k
- else
- Format.fprintf fmt "@,+(%a)" F.pp_term k
-
-let pp_delta fmt k =
- if k != F.e_zero then pp_field fmt k
-
-type loc =
- | GarbledMix (* any possible location *)
- | Index of index (* unqualified address *)
- | Lref of region * index * region
- | Lmem of region * index * root * region value
- | Lraw of region * index * root * region option
- | Lfld of region * index * F.term * region overlay
- | Larr of region * index * F.term * F.term list * int * int list
- (* For Lxxx locations:
- - index: start index inside the chunk
- - term: additional shift index
- - term list: array index from start *)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Loc Basics --- *)
-(* -------------------------------------------------------------------------- *)
-
-let null = Index l_inull
-
-let vars = function
- | GarbledMix -> F.Vars.empty
- | Index l | Lref(_,l,_) | Lmem(_,l,_,_) | Lraw(_,l,_,_) -> F.vars l
- | Lfld(_,l,k,_) ->
- F.Vars.union (F.vars l) (F.vars k)
- | Larr(_,l,k,ks,_,_) ->
- Qed.Hcons.fold_list F.Vars.union F.vars F.Vars.empty (l::k::ks)
-
-let occurs x = function
- | GarbledMix -> false
- | Index l | Lref(_,l,_) | Lmem(_,l,_,_) | Lraw(_,l,_,_) -> F.occurs x l
- | Lfld(_,l,k,_) ->
- F.occurs x l || F.occurs x k
- | Larr(_,l,k,ks,_,_) ->
- List.exists (F.occurs x) (l::k::ks)
-
-let pretty fmt = function
- | GarbledMix -> Format.pp_print_string fmt "garbled-mix"
- | Index l ->
- Format.fprintf fmt "@[<hov 2>Index(%a)@]" pp_index l
- | Lref(r,l,r') ->
- Format.fprintf fmt "@[<hov 2>Ref@,{%a->%a}@,(%a)@]"
- pp_region r pp_region r' pp_index l
- | Lmem(r,l,_,v) ->
- Format.fprintf fmt "@[<hov 2>Mem@,{%a:@,%a}@,(%a)@]"
- pp_region r pp_value v pp_index l
- | Lraw(r,l,_,None) ->
- Format.fprintf fmt "@[<hov 2>Raw@,{%a}@,(%a)"
- pp_region r pp_index l
- | Lraw(r,l,_,Some r') ->
- Format.fprintf fmt "@[<hov 2>Raw@,{%a->%a}@,(%a)"
- pp_region r pp_region r' pp_index l
- | Lfld(r,l,k,_) ->
- Format.fprintf fmt "@[<hov 2>Field@,{%a}@,(%a%a)@]"
- pp_region r pp_index l pp_field k
- | Larr(r,l,k,ks,_,_) ->
- Format.fprintf fmt "@[<hov 2>Index@,{%a}@,@[<hov 2>(%a[%a]%a)@]@]"
- pp_region r pp_index l pp_args ks pp_delta k
-
-(* -------------------------------------------------------------------------- *)
-(* --- Loc Constructors --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec index map (r:region) (l:index) (ofs:F.term) (len:int) =
- index_chunk map r l ofs len (Region.chunk map r)
-
-and index_chunk map (r:region) l ofs len = function
- | Mref r' -> Lref(r,l_shift_index l ofs,r')
- | Mraw(m,p) -> Lraw(r,l_shift_index l ofs,m,p)
- | Mmem(m,v) -> Lmem(r,l_shift_index l ofs,m,v)
- | Mcomp(_,[{ofs=0;reg;dim}]) -> index_dim map reg l ofs len dim
- | Mcomp(_,overlay) -> index_field map r l ofs len overlay
-
-and index_field map r l ofs len overlay =
- try
- let k = FIELD.offset ofs in
- let rg = List.find (Layout.Range.included k len) overlay in
- let fd = F.e_int k in
- let l' = l_field overlay l fd in
- index_dim map rg.reg l' (F.e_sub ofs fd) len rg.dim
- with Not_found ->
- Lfld(r,l,ofs,overlay)
-
-and index_dim map r l ofs len = function
- | Raw s | Dim(s,[]) ->
- index map r (l_index_mem l F.e_zero (F.e_int s)) ofs len
- | Dim(s,ds) ->
- index_array map r l (ARRAY.zeroes ds) ofs len s ds
-
-and index_array map r l ks ofs len s ds =
- let cs = ARRAY.coefs s ds in
- let ks,ofs = ARRAY.offset cs ks ofs in
- if len <= s then
- let l' = l_array s ds l ks in
- index map r l' ofs len
- else
- Larr(r,l,ofs,ks,s,ds)
-
-and shift_index_loc map loc ofs len =
- match loc with
- | GarbledMix -> GarbledMix
- | Index l -> Index (l_shift_index l ofs)
- | Lref(r,l,r') -> Lref(r,l_shift_index l ofs,r')
- | Lmem(r,l,m,v) -> Lmem(r,l_shift_index l ofs,m,v)
- | Lraw(r,l,m,p) -> Lraw(r,l_shift_index l ofs,m,p)
- | Lfld(r,l,k,overlay) -> index_field map r l (F.e_add k ofs) len overlay
- | Larr(r,l,k,ks,s,ds) -> index_array map r l ks (F.e_add k ofs) len s ds
-
-let cvar x =
- let map = map () in
- let region = Region.of_cvar map x in
- let id = if Cil.isConstType x.vtype then - x.vid else x.vid in
- index map region (l_index_var id) F.e_zero (Cil.bitsSizeOf x.vtype)
-
-let field loc fd =
- let map = map () in
- let ofs,len = Region.field_offset map fd in
- shift_index_loc map loc (F.e_int ofs) len
-
-let shift loc obj n =
- let map = map () in
- let s = Ctypes.bits_sizeof_object obj in
- shift_index_loc map loc (F.e_fact s n) s
-
-let pointer_loc l = Index l
-let pointer_val = function
- | GarbledMix -> error "Can not obtain address of Garbled-Mix location"
- | Index l | Lref(_,l,_) | Lmem(_,l,_,_) | Lraw(_,l,_,_) -> l
- | Lfld(_,l,k,overlay) -> l_field overlay l k
- | Larr(_,l,k,ks,s,ds) -> l_shift_index (l_array s ds l ks) k
-
-let loc_of_index re ty l =
- index (map()) re l F.e_zero (Cil.bitsSizeOf ty)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Chunks --- *)
-(* -------------------------------------------------------------------------- *)
-
-type chunk =
- | Mu_alloc
- | Mu_raw of region * root
- | Mu_mem of region * root * region value
-
-module Chunk =
-struct
-
- type t = chunk
- let self = "region"
-
- let id = function
- | Mu_raw(r,_) | Mu_mem(r,_,_) -> Region.id r
- | Mu_alloc -> Region.noid
-
- let hash m = id m
- let compare m m' =
- if m==m then 0 else Stdlib.compare (id m) (id m')
- let equal m m' = m==m' || (id m = id m')
-
- let tau_of_value = function
- | Int _ -> L.Int
- | Float _ -> L.Real
- | Pointer _ -> t_index
-
- let tau_of_chunk = function
- | Mu_alloc -> MemMemory.t_malloc
- | Mu_raw _ -> t_bits
- | Mu_mem(_,root,v) ->
- let value = tau_of_value v in
- if Root.indexed root then L.Array(t_addr,value) else value
-
- let basename_of_chunk = function
- | Mu_raw _ -> "B"
- | Mu_mem(_,root,Int _) -> if Root.indexed root then "M" else "V"
- | Mu_mem(_,root,Float _) -> if Root.indexed root then "Mf" else "F"
- | Mu_mem(_,root,Pointer _) -> if Root.indexed root then "Mp" else "M"
- | Mu_alloc -> "A"
-
- let is_framed = function
- | Mu_raw(_,root) | Mu_mem(_,root,_) -> Root.framed root
- | Mu_alloc -> false
-
- let pretty fmt mu = Format.pp_print_string fmt (basename_of_chunk mu)
-
-end
-
-module Heap =
-struct
- include Qed.Collection.Make(Chunk)
- let empty = Set.empty
- let of_raw r rt = Set.singleton (Mu_raw(r,rt))
- let of_mem r rt v = Set.singleton (Mu_mem(r,rt,v))
-
- let rec of_region map r =
- match Region.chunk map r with
- | Mref _ -> Set.empty
- | Mraw(rt,_) -> of_raw r rt
- | Mmem(rt,v) -> of_mem r rt v
- | Mcomp(_,overlay) -> of_overlay map overlay
-
- and of_range map { reg } = of_region map reg
-
- and of_overlay map ovl =
- Qed.Hcons.fold_list Set.union (of_range map) empty ovl
-
-end
-module Sigma = Sigma.Make(Chunk)(Heap)
-
-type sigma = Sigma.t
-type domain = Sigma.domain
-
-let value_footprint _obj = function
- | GarbledMix | Index _ -> error "Can not compute Garbled-mix domain"
- | Lref _ -> Heap.empty
- | Lraw(r,_,rt,_) -> Heap.of_raw r rt
- | Lmem(r,_,rt,v) -> Heap.of_mem r rt v
- | Lfld(_,_,_,ovl) -> Heap.of_overlay (map()) ovl
- | Larr(r,_,_,_,_,_) -> Heap.of_region (map()) r
-
-let init_footprint _ _ = Heap.empty
-
-let is_well_formed _s = Lang.F.p_true
-
-let region_of_loc = function
- | (GarbledMix | Index _) as l -> error "Can not find region of %a" pretty l
- | Lref(r,_,_) | Lraw(r,_,_,_) | Lmem(r,_,_,_)
- | Lfld(r,_,_,_) | Larr(r,_,_,_,_,_) -> r
-
-(* -------------------------------------------------------------------------- *)
-(* --- Loader --- *)
-(* -------------------------------------------------------------------------- *)
-
-module MODEL =
-struct
-
- module Chunk = Chunk
- module Sigma = Sigma
- let name = "MemRegion.LOADER"
- type nonrec loc = loc
- let field = field
- let shift = shift
- let sizeof obj = Lang.F.e_int (Ctypes.bits_sizeof_object obj)
- let value_footprint = value_footprint
- let init_footprint = init_footprint
- let frames _ _ _ = []
-
- let to_addr l = a_addrof (pointer_val l)
- let to_region_pointer l = Region.id (region_of_loc l) , pointer_val l
- let of_region_pointer r obj l =
- let map = map () in
- index map (Region.region map r) l F.e_zero (Ctypes.bits_sizeof_object obj)
-
- let load_mem sigma r rt v l =
- let m = Sigma.value sigma (Mu_mem(r,rt,v)) in
- if Root.indexed rt then F.e_get m (a_addrof l) else m
-
- let load_int sigma i = function
- | Lmem(r,l,rt,(Int i0 as v)) when i = i0 -> load_mem sigma r rt v l
- | l -> error "Can not load %a value from %a" Ctypes.pp_int i pretty l
-
- let load_float sigma f = function
- | Lmem(r,l,rt,(Float f0 as v)) when f = f0 -> load_mem sigma r rt v l
- | l -> error "Can not load %a value from %a" Ctypes.pp_float f pretty l
-
- let load_pointer sigma ty = function
- | Lmem(r,l,rt,(Pointer r' as v)) ->
- loc_of_index r' ty (load_mem sigma r rt v l)
- | Lref(_,l,r') ->
- loc_of_index r' ty (l_index_ref l)
- | l -> error "Can not load pointer value from %a" pretty l
-
- let havoc obj loc ~length (chunk:chunk) ~fresh ~current =
- match chunk with
- | Mu_alloc -> fresh
- | Mu_raw _ -> error "Can not havoc raw memories"
- | Mu_mem(_,root,_) ->
- if Layout.Root.indexed root then
- let addr = to_addr loc in
- let offset = F.e_fact (Ctypes.bits_sizeof_object obj) length in
- F.e_fun MemMemory.f_havoc [fresh;current;addr;offset]
- else
- fresh
-
- let eqmem obj loc chunk m1 m2 =
- match chunk with
- | Mu_alloc -> error "Can not compare allocation tables"
- | Mu_raw _ -> error "Can not compare raw memories"
- | Mu_mem(_,root,_) ->
- if Layout.Root.indexed root then
- let addr = to_addr loc in
- let offset = F.e_int (Ctypes.bits_sizeof_object obj) in
- F.p_call MemMemory.p_eqmem [m1;m2;addr;offset]
- else F.p_equal m1 m2
-
- let eqmem_forall obj loc chunk m1 m2 =
- match chunk with
- | Mu_alloc -> error "Can not compare allocation tables"
- | Mu_raw _ -> error "Can not compare raw memories"
- | Mu_mem(_,root,_) ->
- if Layout.Root.indexed root then
- let xp = Lang.freshvar ~basename:"p" t_addr in
- let p = F.e_var xp in
- let a = to_addr loc in
- let n = F.e_int (Ctypes.bits_sizeof_object obj) in
- let separated = F.p_call MemAddr.p_separated [ p ; F.e_one ; a ; n ] in
- let equal = F.p_equal (F.e_get m1 p) (F.e_get m2 p) in
- [xp],separated,equal
- else [],F.p_true,F.p_equal m1 m2
-
- let last _ = error "Can not compute last valid index"
-
- let store_mem sigma r rt v l value =
- let c = Mu_mem(r,rt,v) in
- if Root.indexed rt then
- c , F.e_set (Sigma.value sigma c) (a_addrof l) value
- else c , value
-
- let store_int sigma i loc value =
- match loc with
- | Lmem(r,l,rt,(Int i0 as v)) when i = i0 -> store_mem sigma r rt v l value
- | _ -> error "Can not store %a value into %a" Ctypes.pp_int i pretty loc
-
- let store_float sigma f loc value =
- match loc with
- | Lmem(r,l,rt,(Float f0 as v)) when f = f0 -> store_mem sigma r rt v l value
- | _ -> error "Can not store %a value into %a" Ctypes.pp_float f pretty loc
-
- let store_pointer sigma _ty loc value =
- match loc with
- | Lmem(r,l,rt,(Pointer _ as v)) -> store_mem sigma r rt v l value
- | _ -> error "Can not store pointer values into %a" pretty loc
-
- let set_init_atom _ _ _ = assert false
- let set_init _obj _loc ~length _chunk ~current =
- let _ = length in
- let _ = current in
- assert false
- let is_init_atom _ _ = assert false
- let is_init_range _ _ _ _ = assert false
- let monotonic_init _ _ = assert false
-
-end
-
-module LOADER = MemLoader.Make(MODEL)
-
-let load = LOADER.load
-let load_init = LOADER.load_init
-let load_value = LOADER.load_value
-
-let stored = LOADER.stored
-let stored_init = LOADER.stored_init
-let copied = LOADER.copied
-let copied_init = LOADER.copied_init
-let assigned = LOADER.assigned
-let initialized = LOADER.initialized
-
-let domain = LOADER.domain
-
-(* -------------------------------------------------------------------------- *)
-(* --- Loc Segments --- *)
-(* -------------------------------------------------------------------------- *)
-
-type segment = loc rloc
-
-let region_of_sloc = function Rloc(_,l) | Rrange(l,_,_,_) -> region_of_loc l
-
-let disjoint_region s1 s2 =
- let map = map () in
- let c1 = Region.chunks map (region_of_sloc s1) in
- let c2 = Region.chunks map (region_of_sloc s2) in
- not (Qed.Intset.intersect c1 c2)
-
-
-let addrof = MODEL.to_addr
-let sizeof = MODEL.sizeof
-
-let included s1 s2 =
- if disjoint_region s1 s2 then F.p_false else
- MemAddr.included ~shift ~addrof ~sizeof s1 s2
-
-let separated s1 s2 =
- if disjoint_region s1 s2 then F.p_true else
- MemAddr.separated ~shift ~addrof ~sizeof s1 s2
-
-(* -------------------------------------------------------------------------- *)
-(* --- TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO TODO --- *)
-(* -------------------------------------------------------------------------- *)
-
-type state = unit
-
-let state _ = ()
-let iter _ _ = ()
-let lookup _ _ = Mterm
-let updates _ _ = Bag.empty
-let apply _ _ = ()
-
-let literal ~eid _ = ignore eid ; GarbledMix
-
-let base_addr _l = GarbledMix
-let base_offset l = MemAddr.offset (addrof l)
-let block_length _s _obj _l = F.e_zero
-
-let cast _ _l = GarbledMix
-let loc_of_int _ _ = GarbledMix
-let int_of_loc _ _ = F.e_zero
-
-let not_yet_pointer () = error "Pointer comparison not yet implemented"
-
-let is_null _ = not_yet_pointer ()
-let loc_eq _ _ = not_yet_pointer ()
-let loc_lt _ _ = not_yet_pointer ()
-let loc_leq _ _ = not_yet_pointer ()
-let loc_neq _ _ = not_yet_pointer ()
-let loc_diff _ _ _ = not_yet_pointer ()
-
-let frame _sigma = []
-let alloc sigma _xs = sigma
-let scope _seq _s _xs = []
-let valid _sigma _acs _l = error "Validity not yet implemented"
-let invalid _sigma _l = error "Validity not yet implemented"
-let global _sigma _p = F.p_true
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
deleted file mode 100644
index ab78db145f0b52ef58a3e5ee367c4e94d1750d92..0000000000000000000000000000000000000000
--- a/src/plugins/wp/MemRegion.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Empty Memory Model --- *)
-(* -------------------------------------------------------------------------- *)
-
-include Sigs.Model
diff --git a/src/plugins/wp/Region.ml b/src/plugins/wp/Region.ml
deleted file mode 100644
index f2640d16056f7b3e17d3a2639a237d815424ebc9..0000000000000000000000000000000000000000
--- a/src/plugins/wp/Region.ml
+++ /dev/null
@@ -1,644 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_datatype
-open Layout
-
-module Wp = Wp_parameters
-
-(* -------------------------------------------------------------------------- *)
-(* --- Access Maps --- *)
-(* -------------------------------------------------------------------------- *)
-
-module Vmap = Varinfo.Map
-module Smap = Datatype.String.Map
-module Rmap = Qed.Intmap
-module Rset = Qed.Intset
-module Dmap = Qed.Listmap.Make(Offset)
-module Dset = Qed.Listset.Make(Deref)
-module Acs = Qed.Listset.Make(Lvalue)
-module Class = Qed.Listset.Make(Datatype.String)
-
-type region = {
- id : int ;
- mutable garbled : bool ;
- rw : bool ;
- pack : bool ;
- flat : bool ;
- mutable names : Class.t ;
- mutable alias : alias ;
- mutable delta : int Dmap.t ;
- mutable deref : Dset.t ;
- mutable read : Acs.t ;
- mutable written : Acs.t ;
- mutable shifted : Acs.t ;
- mutable copiedTo : Rset.t ; (* copies to *)
- mutable pointsTo : int option ;
-}
-
-type map = {
- cache : Offset.cache ;
- queue : int Queue.t ;
- mutable rid : int ;
- mutable vars : int Vmap.t ;
- mutable return : int ; (* -1 when undefined *)
- mutable strings : (int * string) Rmap.t ; (* eid -> rid *)
- mutable index : int Smap.t ;
- mutable region : region Rmap.t ;
- mutable aliasing : int Rmap.t ;
- mutable cluster : region cluster Rmap.t ;
- mutable roots : root Rmap.t ;
- mutable froms : region from list Rmap.t ;
- mutable domain : Rset.t ; (* reachable regions via clusters *)
- mutable chunk : region chunk Rmap.t ; (* memory chunks *)
-}
-
-let create () = {
- rid = 0 ;
- return = (-1) ;
- cache = Offset.cache () ;
- vars = Vmap.empty ;
- strings = Rmap.empty ;
- index = Smap.empty ;
- region = Rmap.empty ;
- aliasing = Rmap.empty ;
- queue = Queue.create () ;
- cluster = Rmap.empty ;
- roots = Rmap.empty ;
- froms = Rmap.empty ;
- domain = Rset.empty ;
- chunk = Rmap.empty ;
-}
-
-let noid = 0
-let is_empty map = (map.rid = 0)
-
-let fresh map =
- let id = map.rid in
- map.rid <- succ id ;
- let region = {
- id ;
- garbled = false ;
- rw = RW.default () ;
- flat = Flat.default () ;
- pack = Pack.default () ;
- names = [] ;
- alias = NotUsed ;
- delta = Dmap.empty ;
- deref = Dset.empty ;
- read = Acs.empty ;
- written = Acs.empty ;
- shifted = Acs.empty ;
- copiedTo = Rset.empty ;
- pointsTo = None ;
- } in
- map.region <- Rmap.add id region map.region ;
- region
-
-(* -------------------------------------------------------------------------- *)
-(* --- Datatype --- *)
-(* -------------------------------------------------------------------------- *)
-
-module R =
-struct
- type t = region
- let id a = a.id
- let equal a b = (a.id = b.id)
- let compare a b = Stdlib.compare a.id b.id
- let pp_rid fmt id = Format.fprintf fmt "R%03d" id
- let pretty fmt r = pp_rid fmt r.id
-end
-
-module Map = Qed.Idxmap.Make(R)
-module Set = Qed.Idxset.Make(R)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Union Find --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec aliasing map i =
- try
- let j = aliasing map (Rmap.find i map.aliasing) in
- if j <> i then map.aliasing <- Rmap.add i j map.aliasing ; j
- with Not_found -> i
-
-let linkto map i k =
- if i <> k then
- begin
- map.aliasing <- Rmap.add i k map.aliasing ;
- Queue.add i map.queue ;
- end
-
-let region map r =
- try Rmap.find (aliasing map r) map.region
- with Not_found -> failwith "Wp.Region: Undefined Region"
-
-let join_classes map i j =
- let k = min i j in (linkto map i k ; linkto map j k ; k)
-
-let join_id map i j =
- let i = aliasing map i in
- let j = aliasing map j in
- if i = j then i else join_classes map i j
-
-let join_region map ra rb =
- let i = aliasing map ra.id in
- let j = aliasing map rb.id in
- let k = join_classes map i j in
- if k = i then ra else
- if k = j then rb else
- (* defensive *) region map k
-
-(* -------------------------------------------------------------------------- *)
-(* --- Aliasing --- *)
-(* -------------------------------------------------------------------------- *)
-
-let alias map a b =
- let k = join_id map a.id b.id in
- let r = region map k in
- r.alias <- Aliased ; r
-
-let do_alias map a b = ignore (alias map a b)
-
-let add_alias map ~into:a b =
- let i = aliasing map a.id in
- let j = aliasing map b.id in
- let wa = (region map i).alias in
- let wb = (region map j).alias in
- let k = join_classes map i j in
- (* Aliasing has changed *)
- (region map k).alias <- Alias.alias wa (Alias.use wb)
-
-let get_merged map r =
- let i = aliasing map r.id in
- if i <> r.id then Some (region map i) else None
-
-let get_alias map r =
- let i = aliasing map r.id in
- if i <> r.id then region map i else r
-
-let eq_alias map a b = (aliasing map a.id = aliasing map b.id)
-
-(* -------------------------------------------------------------------------- *)
-(* --- General Iterator --- *)
-(* -------------------------------------------------------------------------- *)
-
-let once mark r =
- if Rset.mem r.id !mark then false
- else ( mark := Rset.add r.id !mark ; true )
-
-let iter map f =
- let do_once marks f r = if once marks r then f r else () in
- Rmap.iter (do_once (ref Rset.empty) f) map.region
-
-(* -------------------------------------------------------------------------- *)
-(* --- Region Accessor --- *)
-(* -------------------------------------------------------------------------- *)
-
-let id reg = reg.id
-let is_garbled reg = reg.garbled
-let has_pointed reg = reg.pointsTo <> None
-let has_deref reg = not (Dset.is_empty reg.deref)
-let has_layout reg = not (Dmap.is_empty reg.delta)
-let has_offset reg d = Dmap.mem d reg.delta
-let iter_offset map f reg =
- Dmap.iter (fun ofs r -> f ofs (region map r)) reg.delta
-
-let has_copies reg = not (Rset.is_empty reg.copiedTo)
-let iter_copies map f reg =
- Rset.iter (fun r -> f (region map r)) reg.copiedTo
-
-let add_offset map reg d =
- try region map (Dmap.find d reg.delta)
- with Not_found ->
- let rd = fresh map in
- reg.delta <- Dmap.add d rd.id reg.delta ; rd
-
-let add_pointed map reg =
- match reg.pointsTo with
- | Some k -> region map k
- | None ->
- let r = fresh map in
- reg.pointsTo <- Some r.id ; r
-
-let get_addrof map reg =
- let addr = fresh map in
- addr.pointsTo <- Some reg.id ; addr
-
-let get_pointed map reg =
- match reg.pointsTo with
- | None -> None
- | Some r -> Some (region map r)
-
-let get_offset map reg d =
- try Some (region map (Dmap.find d reg.delta))
- with Not_found -> None
-
-let get_copies map reg =
- List.map (region map) (Rset.elements reg.copiedTo)
-
-(* -------------------------------------------------------------------------- *)
-(* --- Access --- *)
-(* -------------------------------------------------------------------------- *)
-
-let acs_read rg lvalue = rg.read <- Acs.add lvalue rg.read
-let acs_write rg lvalue = rg.written <- Acs.add lvalue rg.written
-let acs_shift rg lvalue = rg.shifted <- Acs.add lvalue rg.shifted
-let acs_deref rg deref = rg.deref <- Dset.add deref rg.deref
-let acs_copy ~src ~tgt =
- if tgt.id <> src.id then src.copiedTo <- Rset.add tgt.id src.copiedTo
-
-let iter_read f rg = Acs.iter f rg.read
-let iter_write f rg = Acs.iter f rg.written
-let iter_shift f rg = Acs.iter f rg.shifted
-let iter_deref f rg = Dset.iter f rg.deref
-
-let is_read rg = not (Acs.is_empty rg.read)
-let is_written rg = not (Acs.is_empty rg.written)
-let is_shifted rg = not (Acs.is_empty rg.shifted)
-let is_aliased rg = Alias.is_aliased rg.alias
-
-(* -------------------------------------------------------------------------- *)
-(* --- Varinfo Index --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rvar map x r =
- let reg = region map r in
- if reg.id <> r then map.vars <- Vmap.add x reg.id map.vars ; reg
-
-let of_null map = fresh map (* A fresh region each time: polymorphic *)
-
-let of_cvar map x =
- try rvar map x (Vmap.find x map.vars)
- with Not_found ->
- let reg = fresh map in
- map.vars <- Vmap.add x reg.id map.vars ; reg
-
-let of_return map =
- if map.return < 0 then
- let reg = fresh map in
- map.return <- reg.id ; reg
- else
- region map map.return
-
-let has_return map = 0 <= map.return
-
-let iter_vars map f = Vmap.iter (fun x r -> f x (rvar map x r)) map.vars
-
-(* -------------------------------------------------------------------------- *)
-(* --- Field Info Index --- *)
-(* -------------------------------------------------------------------------- *)
-
-let field_offset map fd = Offset.field_offset map.cache fd
-
-(* -------------------------------------------------------------------------- *)
-(* --- String Literal Index --- *)
-(* -------------------------------------------------------------------------- *)
-
-let of_cstring map ~eid ~cst =
- try region map (fst @@ Rmap.find eid map.strings)
- with Not_found ->
- let reg = fresh map in
- map.strings <- Rmap.add eid (reg.id,cst) map.strings ; reg
-
-let iter_strings map f =
- Rmap.iter (fun (rid,cst) -> f (region map rid) cst) map.strings
-
-(* -------------------------------------------------------------------------- *)
-(* --- Region Index --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rindex map a r =
- let reg = region map r in
- if reg.id <> r then map.index <- Smap.add a reg.id map.index ; reg
-
-let of_name map a =
- try rindex map a (Smap.find a map.index)
- with Not_found ->
- let reg = fresh map in
- reg.names <- [a] ;
- map.index <- Smap.add a reg.id map.index ; reg
-
-let of_class map = function
- | None -> fresh map
- | Some a -> of_name map a
-
-let has_names reg = not (Class.is_empty reg.names)
-let iter_names map f = Smap.iter (fun a r -> f a (rindex map a r)) map.index
-
-(* -------------------------------------------------------------------------- *)
-(* --- Fusion --- *)
-(* -------------------------------------------------------------------------- *)
-
-let merge_pointed map u v =
- match u,v with
- | None , w | w , None -> w
- | Some i , Some j -> Some (join_id map i j)
-
-let merge_delta map _d a b = join_id map a b
-
-let merge_region map ~id a b =
- {
- id ;
- garbled = a.garbled || b.garbled ;
- rw = RW.merge a.rw b.rw ;
- flat = Flat.merge a.flat b.flat ;
- pack = Pack.merge a.pack b.pack ;
- alias = Alias.merge a.alias b.alias ;
- names = Class.union a.names b.names ;
- read = Acs.union a.read b.read ;
- written = Acs.union a.written b.written ;
- shifted = Acs.union a.shifted b.shifted ;
- copiedTo = Rset.union a.copiedTo b.copiedTo ;
- pointsTo = merge_pointed map a.pointsTo b.pointsTo ;
- delta = Dmap.union (merge_delta map) a.delta b.delta ;
- deref = Dset.union a.deref b.deref ;
- }
-
-let fusion map =
- while not (Queue.is_empty map.queue) do
- let i = Queue.pop map.queue in
- let j = aliasing map i in
- if i <> j then
- begin
- if not (Wp.Region_fixpoint.get ()) then
- Wp.debug "Region %a -> %a" R.pp_rid i R.pp_rid j ;
- let a = try Rmap.find i map.region with Not_found -> assert false in
- let b = try Rmap.find j map.region with Not_found -> assert false in
- assert (i = a.id) ;
- assert (j = b.id ) ;
- let c = merge_region map ~id:j a b in
- map.region <- Rmap.add j c (Rmap.remove i map.region) ;
- end
- done
-
-let fusionned map = not (Queue.is_empty map.queue)
-let iter_fusion map f = Queue.iter (fun i -> f i (region map i)) map.queue
-
-(* -------------------------------------------------------------------------- *)
-(* --- Garbling --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec garblify map reg =
- if not reg.garbled then
- begin
- reg.garbled <- true ;
- Dmap.iter
- (fun _delta r ->
- garblify map (region map r) ;
- ignore (join_id map reg.id r) ;
- ) reg.delta ;
- reg.delta <- Dmap.empty ;
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Clustering --- *)
-(* -------------------------------------------------------------------------- *)
-
-let cluster map reg =
- try Rmap.find reg.id map.cluster
- with Not_found -> Layout.Empty
-
-module Cluster =
-struct
- open Layout
-
- let rec from_region map reg =
- try Rmap.find reg.id map.cluster
- with Not_found ->
- if reg.garbled then Garbled else
- if not (Wp.Region_cluster.get ()) then Empty else
- begin
- map.cluster <- Rmap.add reg.id Empty map.cluster ;
- let mu ~raw ra rb =
- if raw then
- begin
- garblify map ra ;
- garblify map rb ;
- end ;
- join_region map ra rb
- in
- let cluster =
- if has_layout reg then
- Cluster.reshape ~eq:R.equal ~flat:reg.flat ~pack:reg.pack @@
- from_layout map mu reg
- else
- from_deref map mu reg
- in
- if cluster = Garbled then garblify map reg ;
- map.cluster <- Rmap.add reg.id cluster map.cluster ;
- cluster
- end
-
- and from_deref map mu reg =
- let pointed = lazy (add_pointed map reg) in
- List.fold_left
- (fun chunk deref ->
- Cluster.merge R.pretty mu chunk (Cluster.deref ~pointed deref)
- ) Empty reg.deref
-
- and from_layout map mu reg =
- Dmap.fold
- (fun offset tgt acc ->
- let layout = shift map offset (region map tgt) in
- Cluster.merge R.pretty mu (Layout layout) acc
- ) reg.delta Empty
-
- and shift map offset target =
- let inline = Wp.Region_inline.get () || not (is_aliased target) in
- let cluster = from_region map target in
- Cluster.shift map.cache R.pretty offset target ~inline cluster
-
- let compute map reg =
- begin
- if has_layout reg && has_deref reg then
- begin
- Dset.iter
- (fun deref ->
- let target = add_offset map reg (Index(snd deref,1)) in
- target.read <- Acs.union reg.read target.read ;
- target.written <- Acs.union reg.written target.written ;
- acs_deref target deref
- ) reg.deref ;
- reg.deref <- Dset.empty ;
- reg.read <- Acs.empty ;
- reg.written <- Acs.empty ;
- Queue.add reg.id map.queue ;
- end ;
- ignore (from_region map reg) ;
- end
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Froms Analysis --- *)
-(* -------------------------------------------------------------------------- *)
-
-let get_froms map reg =
- try Rmap.find reg.id map.froms
- with Not_found -> []
-
-let add_from map ~from ~target =
- let rs = get_froms map target in
- map.froms <- Rmap.add target.id (from :: rs) map.froms
-
-module Froms =
-struct
- open Layout
-
- let rec forward map marks ~source ~from ~target =
- map.domain <- Rset.add source.id map.domain ;
- add_from map ~from ~target ;
- if once marks target then add_region map marks target
-
- and add_region map marks reg =
- begin
- add_points_to map marks ~source:reg reg.pointsTo ;
- add_cluster map marks ~source:reg (cluster map reg) ;
- end
-
- and add_points_to map marks ~source = function
- | None -> ()
- | Some p -> add_deref map marks ~source ~target:(region map p)
-
- and add_deref map marks ~source ~target =
- let from = if is_shifted target then Farray source else Fderef source in
- forward map marks ~source ~from ~target
-
- and add_cluster map marks ~source = function
- | Empty | Garbled | Chunk (Int _ | Float _) -> ()
- | Chunk (Pointer target) -> add_deref map marks ~source ~target
- | Layout { layout } -> List.iter (add_range map marks ~source) layout
-
- and add_range map marks ~source = function
- | { ofs ; reg = target ; dim = Dim(_,[]) } ->
- forward map marks ~source ~from:(Ffield(source,ofs)) ~target
- | { reg = target } ->
- forward map marks ~source ~from:(Findex source) ~target
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Roots Analysis --- *)
-(* -------------------------------------------------------------------------- *)
-
-let get_roots map reg =
- try Rmap.find reg.id map.roots
- with Not_found -> Rnone
-
-let has_roots map reg = get_roots map reg <> Rnone
-
-module Roots =
-struct
-
- let rec of_region map region =
- try Rmap.find region.id map.roots
- with Not_found ->
- let froms = get_froms map region in
- let roots =
- List.fold_left
- (fun roots from ->
- Root.merge roots (Root.from ~root:(of_region map) from)
- ) Rnone froms
- in map.roots <- Rmap.add region.id roots map.roots ; roots
-
- let compute map reg = ignore (of_region map reg)
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Forward & Backward Propagation --- *)
-(* -------------------------------------------------------------------------- *)
-
-let forward map =
- begin
- let marks = ref Rset.empty in
- map.domain <- Rset.empty ;
- Vmap.iter
- (fun x r ->
- let reg = region map r in
- let open Cil_types in
- if x.vglob || x.vformal then
- add_from map ~from:(Fvar x) ~target:(region map r) ;
- Froms.add_region map marks reg ;
- ) map.vars ;
- end
-
-let backward map =
- begin
- Rmap.iter (Roots.compute map) map.region ;
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Chunk Analysis --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec chunk map region =
- try Rmap.find region.id map.chunk
- with Not_found ->
- let roots = get_roots map region in
- let chunk =
- match cluster map region with
- | Empty | Garbled -> Mraw (roots,get_pointed map region)
- | Chunk v ->
- if is_read region || is_written region then
- Mmem(roots,v)
- else
- begin match v with
- | Pointer r -> Mref r
- | _ -> Mraw (roots,get_pointed map region)
- end
- | Layout { layout } ->
- let chunks = Chunk.union_map (fun { reg } -> chunks map reg) layout
- in Mcomp(chunks,layout)
-
- in map.chunk <- Rmap.add region.id chunk map.chunk ; chunk
-
-and chunks map region =
- match chunk map region with
- | Mcomp(rs,_) -> rs
- | _ -> Chunk.singleton region.id
-
-(* -------------------------------------------------------------------------- *)
-(* --- Fixpoint --- *)
-(* -------------------------------------------------------------------------- *)
-
-let fixpoint map =
- begin
- let turn = ref 0 in
- let loop = ref true in
- while !loop do
- incr turn ;
- Wp.feedback ~ontty:`Transient "Region clustering (loop #%d)" !turn ;
- fusion map ;
- map.cluster <- Rmap.empty ;
- iter map (Cluster.compute map) ;
- loop := fusionned map ;
- done ;
- Wp.feedback ~ontty:`Transient "Region forward analysis" ;
- forward map ;
- Wp.feedback ~ontty:`Transient "Region backward analysis" ;
- backward map ;
- Wp.feedback ~ontty:`Transient "Region fixpoint reached" ;
- end
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Region.mli b/src/plugins/wp/Region.mli
deleted file mode 100644
index 1852732e5034a8e3f76b196b666b2fd3441bf2b4..0000000000000000000000000000000000000000
--- a/src/plugins/wp/Region.mli
+++ /dev/null
@@ -1,105 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Layout
-
-type region
-type map
-
-module R : Layout.Data with type t = region
-module Map : Qed.Idxmap.S with type key = region
-module Set : Qed.Idxset.S with type elt = region
-
-val create : unit -> map
-val is_empty : map -> bool
-val iter : map -> (region -> unit) -> unit
-
-val id: region -> int
-val noid: int
-
-val get_addrof : map -> region -> region
-val add_pointed : map -> region -> region
-val add_offset : map -> region -> offset -> region
-val field_offset : map -> fieldinfo -> int * int
-
-val get_froms : map -> region -> region from list
-val get_roots : map -> region -> root
-val has_roots : map -> region -> bool
-
-val is_garbled : region -> bool
-val has_pointed : region -> bool
-val has_layout : region -> bool
-val has_offset : region -> offset -> bool
-val has_copies : region -> bool
-val has_deref : region -> bool
-val has_names : region -> bool
-val has_return : map -> bool
-
-val get_pointed : map -> region -> region option
-val get_offset : map -> region -> offset -> region option
-val get_copies : map -> region -> region list
-val get_alias : map -> region -> region
-val get_merged : map -> region -> region option
-val eq_alias : map -> region -> region -> bool
-
-val acs_read : region -> lvalue -> unit
-val acs_write : region -> lvalue -> unit
-val acs_shift : region -> lvalue -> unit
-val acs_deref : region -> deref -> unit
-val acs_copy : src:region -> tgt:region -> unit
-
-val is_read : region -> bool
-val is_written : region -> bool
-val is_shifted : region -> bool
-val is_aliased : region -> bool
-
-val iter_read : (lvalue -> unit) -> region -> unit
-val iter_write : (lvalue -> unit) -> region -> unit
-val iter_shift : (lvalue -> unit) -> region -> unit
-val iter_deref : (deref -> unit) -> region -> unit
-val iter_offset : map -> (offset -> region -> unit) -> region -> unit
-val iter_copies : map -> (region -> unit) -> region -> unit
-val iter_vars : map -> (varinfo -> region -> unit) -> unit
-val iter_names : map -> (string -> region -> unit) -> unit
-val iter_strings : map -> (region -> string -> unit) -> unit
-
-val of_null : map -> region
-val of_return : map -> region
-val of_cvar : map -> varinfo -> region
-val of_cstring : map -> eid:int -> cst:string -> region
-val of_name : map -> string -> region
-val of_class : map -> string option -> region
-
-val region : map -> int -> region
-val cluster : map -> region -> region cluster
-val chunk : map -> region -> region chunk
-val chunks : map -> region -> chunks
-
-val alias : map -> region -> region -> region
-val do_alias : map -> region -> region -> unit
-val add_alias : map -> into:region -> region -> unit
-
-val fusion : map -> unit
-val fusionned : map -> bool
-val iter_fusion : map -> (int -> region -> unit) -> unit
-val fixpoint : map -> unit
diff --git a/src/plugins/wp/RegionAccess.ml b/src/plugins/wp/RegionAccess.ml
deleted file mode 100644
index 68f734e9e57610f5ef3a2d72bd045af15a22cf3b..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionAccess.ml
+++ /dev/null
@@ -1,453 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Layout
-open Region
-
-(* -------------------------------------------------------------------------- *)
-(* --- Location Compiler --- *)
-(* -------------------------------------------------------------------------- *)
-
-type addr = {
- addrof : Region.region ;
- typeOfPointed : typ ;
- shift : bool ;
-}
-
-type value =
- | Pure
- | Read_at of typ * region
- | Addr_of of addr
-
-[@@@ warning "-32"]
-let pp_value fmt = function
- | Pure -> Format.pp_print_string fmt "scalar"
- | Read_at(_,r) -> Format.fprintf fmt "read %a" R.pretty r
- | Addr_of a ->
- if a.shift then
- Format.fprintf fmt "addr %a+" R.pretty a.addrof
- else
- Format.fprintf fmt "addr %a" R.pretty a.addrof
-[@@@ warning "+32"]
-
-(* -------------------------------------------------------------------------- *)
-(* --- Strings --- *)
-(* -------------------------------------------------------------------------- *)
-
-let cc_string map exp =
- let cst = Pretty_utils.to_string Cil_datatype.Exp.pretty exp in
- let addrof = Region.of_cstring map ~eid:exp.eid ~cst in
- { addrof ; typeOfPointed = Cil_const.charType ; shift=false }
-
-(* -------------------------------------------------------------------------- *)
-(* --- Reading Values --- *)
-(* -------------------------------------------------------------------------- *)
-
-let read acs = function
- | Pure -> ()
- | Addr_of _ -> ()
- | Read_at(tr,r) ->
- acs_deref r (Value,tr) ;
- acs_read r acs
-
-let points_to = function { shift ; addrof = pointed ; typeOfPointed = typ } ->
- acs_deref pointed ((if shift then Array else Deref),typ)
-
-let addrof map = function
- | Pure -> failwith "Wp.Region: physical address"
- | Read_at(tr,r) ->
- acs_deref r (Value,tr) ;
- {
- addrof = add_pointed map r ;
- typeOfPointed = Cil.typeOf_pointed tr ;
- shift = false ;
- }
- | Addr_of addr -> addr
-
-let cast ty value =
- if Cil.isPointerType ty then
- match value with
- | Addr_of addr ->
- Addr_of { addr with typeOfPointed = Cil.typeOf_pointed ty }
- | Read_at (_,r) -> Read_at(ty,r)
- | Pure -> Pure
- else
- value
-
-let is_pointer_value = function
- | Pure -> false
- | Addr_of _ -> true
- | Read_at(tr,_) -> Cil.isPointerType tr
-
-let merge_type t t' =
- if Cil.isVoidType t then t' else
- if Cil.isVoidType t' then t else
- if Cil_datatype.Typ.equal t t' then t
- else failwith "Wp.Region: merge incompatible pointer types"
-
-let merge_addrof (map:map) v1 v2 =
- if not (is_pointer_value v1) then v2 else
- if not (is_pointer_value v2) then v1 else
- let a1 = addrof map v1 in
- let a2 = addrof map v2 in
- let typeOfPointed = merge_type a1.typeOfPointed a2.typeOfPointed in
- let addrof = Region.alias map a1.addrof a2.addrof in
- let shift = a1.shift || a2.shift in
- Addr_of { addrof ; typeOfPointed ; shift }
-
-(* -------------------------------------------------------------------------- *)
-(* --- Expressions & L-values --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec cc_exp (map:map) exp =
- match exp.enode with
- | BinOp( (PlusPI | MinusPI) , a , b , _ ) ->
- cc_read map b ;
- let { addrof = pointed } as addr = cc_addr map a in
- acs_shift pointed (Eval exp) ;
- Addr_of { addr with shift = true }
- | AddrOf lv | StartOf lv ->
- Addr_of {
- addrof = cc_lval map lv ;
- typeOfPointed = Cil.typeOfLval lv ;
- shift = false ;
- }
- | Lval lv -> Read_at (Cil.typeOfLval lv , cc_lval map lv)
- | CastE(ty,e) -> cast ty (cc_exp map e)
- | Const (CStr _ | CWStr _) -> Addr_of (cc_string map exp)
- | Const (CInt64 _ | CChr _ | CEnum _ | CReal _)
- | SizeOf _ | SizeOfE _ | SizeOfStr _
- | AlignOf _ | AlignOfE _ -> Pure
- | UnOp(_,e,ty) ->
- assert (not (Cil.isPointerType ty)) ;
- cc_read map e ; Pure
- | BinOp(_,a,b,ty) ->
- assert (not (Cil.isPointerType ty)) ;
- cc_read map a ; cc_read map b ; Pure
-
-and cc_host map = function
- | Var x -> of_cvar map x , x.vtype
- | Mem e ->
- let a = cc_addr map e in
- points_to a ; (* deref, not read !*)
- a.addrof , a.typeOfPointed
-
-and cc_lval map (host , offset) =
- let r,ty = cc_host map host in cc_offset map r ty offset
-
-and cc_offset map r ty = function
- | Cil_types.NoOffset -> r
- | Cil_types.Field(fd,ofs) ->
- let df = Offset.field fd in
- cc_offset map (add_offset map r df) fd.ftype ofs
- | Cil_types.Index(e,ofs) ->
- cc_read map e ;
- let de = Offset.index ty in
- let te = Offset.typeof de in
- cc_offset map (add_offset map r de) te ofs
-
-and cc_addr map a = addrof map (cc_exp map a)
-
-and cc_read map e = read (Eval e) (cc_exp map e)
-
-and cc_comp map e =
- match cc_exp map e with
- | Pure | Addr_of _ -> failwith "Wp.Region: comp expected"
- | Read_at(_,r) -> r
-
-let cc_writes map stmt tgt typ e =
- acs_deref tgt (Value,typ) ;
- acs_write tgt (Assigned stmt) ;
- match Cil.unrollType typ with
- | TPtr _ ->
- let a = cc_addr map e in
- points_to a ; (* deref, not read! *)
- do_alias map a.addrof (add_pointed map tgt)
- | TComp _ ->
- let src = cc_comp map e in
- acs_copy ~src ~tgt
- | _ ->
- cc_read map e
-
-let cc_assign map stmt lv e =
- cc_writes map stmt (cc_lval map lv) (Cil.typeOfLval lv) e
-
-let cc_return map stmt e =
- cc_writes map stmt (Region.of_return map) (Cil.typeOf e) e
-
-(* -------------------------------------------------------------------------- *)
-(* --- Stmt & Instructions --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec cc_init map stmt lv = function
- | SingleInit e -> cc_assign map stmt lv e
- | CompoundInit(_,content) ->
- List.iter
- (fun (ofs,vi) ->
- cc_init map stmt (Cil.addOffsetLval ofs lv) vi
- ) content
-
-let cc_local_init map stmt x = function
- | AssignInit vi -> cc_init map stmt (Var x,NoOffset) vi
- | ConsInit _ -> failwith "Wp.Region: cons-init not implemented"
-
-let cc_instr map stmt = function
- | Set(lv,e,_) -> cc_assign map stmt lv e
- | Call _ -> failwith "Wp.Region: call not implemented"
- | Local_init(x,vi,_) -> cc_local_init map stmt x vi
- | Asm _ | Skip _ | Code_annot _ -> ()
-
-let cc_skind map stmt =
- match stmt.skind with
- | Instr instr -> cc_instr map stmt instr
- | Return(Some ve,_) -> cc_return map stmt ve
- | If(e,_,_,_) -> cc_read map e
- | Switch(e,_,_,_) -> cc_read map e
-
- | Return(None,_) | Goto _ | Break _ | Continue _ | Loop _
- | Block _ | UnspecifiedSequence _
- | Throw _ | TryCatch _ | TryFinally _ | TryExcept _ -> ()
-
-(* -------------------------------------------------------------------------- *)
-(* --- ACSL Terms --- *)
-(* -------------------------------------------------------------------------- *)
-
-let rec cc_term map t = read (Tval t) (cc_term_value map t)
-
-and cc_term_value (map:map) (term:term) =
- match term.term_node with
- | TLval lv ->
- begin match cc_term_lval map lv with
- | None -> Pure
- | Some(ty,reg) -> Read_at(ty,reg)
- end
- | TAddrOf lv | TStartOf lv ->
- begin match cc_term_lval map lv with
- | None -> failwith "Wp.Region: pure term-value"
- | Some(ty,reg) -> Addr_of {
- addrof = reg ;
- typeOfPointed = ty ;
- shift = false ;
- }
- end
- | TBinOp( (PlusPI | MinusPI) , a , b ) ->
- begin
- cc_term map b ;
- let { addrof = pointed } as addr = cc_term_addr map a in
- acs_shift pointed (Tval term) ;
- Addr_of { addr with shift = true }
- end
-
- | Tnull ->
- Addr_of {
- addrof = Region.of_null map ;
- typeOfPointed = Cil_const.charType ;
- shift = false ;
- }
-
- | TUnOp(_,a) -> cc_term map a ; Pure
- | TBinOp(_,a,b) -> cc_term map a ; cc_term map b ; Pure
-
- | Tat(t,_) -> cc_term_value map t
-
- | TCast (_, Ctype ty,t) -> cast ty @@ cc_term_value map t
- | TCast (true, _,t) -> cc_term_value map t
- | TCast (false, _,_) -> assert false
-
- | TConst _
- | TSizeOf _ | TSizeOfE _ | TSizeOfStr _
- | TAlignOf _ | TAlignOfE _ | Ttype _ | Ttypeof _
- -> Pure
-
- | TDataCons(_,ts) -> List.iter (cc_term map) ts ; Pure
- | TUpdate(w,ofs,v) ->
- cc_term map w ;
- cc_term map v ;
- cc_term_offset_read map ofs ;
- Pure
-
- | Tbase_addr(_at,t) -> cast Cil_const.voidPtrType @@ cc_term_value map t
- | Tblock_length(_at,t) | Toffset(_at,t) -> cc_term map t ; Pure
-
- | Tif(c,a,b) ->
- cc_term map c ;
- merge_addrof map (cc_term_value map a) (cc_term_value map b)
-
- | Tempty_set -> Pure
- | Tunion ts | Tinter ts ->
- List.fold_left
- (fun v t -> merge_addrof map v (cc_term_value map t)) Pure ts
-
- | Tcomprehension(t,_,None) -> cc_term_value map t
- | Tcomprehension(t,_,Some p) -> cc_pred map p ; cc_term_value map t
- | Trange(a,b) -> cc_term_option map a ; cc_term_option map b ; Pure
-
- | Tlet _ | Tlambda _ | Tapp _ ->
- failwith "Wp.Region: unsupported logic functions and bindings"
-
-and cc_term_lval map (lhost,loffset) =
- match lhost with
- | TResult typ -> Some(typ,of_return map)
- | TVar lvar ->
- begin
- match lvar.lv_origin with
- | Some x ->
- let ty,rv = cc_term_offset map (of_cvar map x) x.vtype loffset in
- Some(ty,rv)
- | None ->
- cc_term_offset_read map loffset ;
- None
- end
- | TMem p ->
- begin
- let a = cc_term_addr map p in
- points_to a ;
- let ty,ra = cc_term_offset map a.addrof a.typeOfPointed loffset in
- Some(ty,ra)
- end
-
-and cc_term_offset map r ty = function
- | TNoOffset -> ty,r
- | TField(fd,ofs) ->
- let df = Offset.field fd in
- cc_term_offset map (add_offset map r df) fd.ftype ofs
- | TIndex(t,ofs) ->
- cc_term map t ;
- let de = Offset.index ty in
- let te = Offset.typeof de in
- cc_term_offset map (add_offset map r de) te ofs
- | TModel _ -> failwith "Wp.Region: model field"
-
-and cc_term_offset_read map = function
- | TNoOffset -> ()
- | TField(_,ofs) -> cc_term_offset_read map ofs
- | TModel(_,ofs) -> cc_term_offset_read map ofs
- | TIndex(t,ofs) -> cc_term map t ; cc_term_offset_read map ofs
-
-and cc_term_addr map t = addrof map @@ cc_term_value map t
-
-and cc_term_option map = function None -> () | Some t -> cc_term map t
-
-(* -------------------------------------------------------------------------- *)
-(* --- ACSL Predicates --- *)
-(* -------------------------------------------------------------------------- *)
-
-and cc_pred (map:map) (p:predicate) =
- match p.pred_content with
- | Pfalse | Ptrue -> ()
-
- | Prel(_,a,b) ->
- cc_term map a ; cc_term map b
-
- | Pnot a -> cc_pred map a
- | Pif(t,a,b) ->
- cc_term map t ; cc_pred map a ; cc_pred map b
- | Pand(a,b) | Por(a,b) | Pxor(a,b) | Pimplies(a,b) | Piff(a,b) ->
- cc_pred map a ; cc_pred map b
-
- | Pforall(_,p) | Pexists(_,p) -> cc_pred map p
-
- | Pseparated ts -> List.iter (cc_term map) ts
- | Pvalid(_,t) | Pvalid_read(_,t) | Pobject_pointer(_,t) | Pvalid_function t
- | Pinitialized(_,t) | Pdangling(_,t) | Pallocable(_,t)
- | Pfreeable(_,t) -> cc_term map t
- | Pfresh(_,_,ptr,n) -> cc_term map ptr ; cc_term map n
-
- | Pat(p,_at) -> cc_pred map p
-
- | Plet _ | Papp _ ->
- failwith "Wp.Region: unsupported logic predicates and bindings"
-
-(* -------------------------------------------------------------------------- *)
-(* --- ACSL Spec & Defs --- *)
-(* -------------------------------------------------------------------------- *)
-
-class visitor map =
- object
- inherit Visitor.frama_c_inplace as super
-
- method! vpredicate p = cc_pred map p ; Cil.SkipChildren
- method! vterm t = cc_term map t ; Cil.SkipChildren
- method! vstmt s = cc_skind map s ; super#vstmt s
- (* vpredicate and vterm are called from vcode_annot *)
-
- (* speed up: skip non interesting subtrees *)
- method! vvdec _ = Cil.SkipChildren (* done via stmt *)
- method! vexpr _ = Cil.SkipChildren (* done via stmt *)
- method! vlval _ = Cil.SkipChildren (* done via stmt *)
- method! vattr _ = Cil.SkipChildren (* done via stmt *)
- method! vinst _ = Cil.SkipChildren (* done via stmt *)
- end
-
-let cc_fundec map def =
- let visitor = new visitor map in
- ignore (Cil.visitCilFunction (visitor:>Cil.cilVisitor) def)
-
-let cc_spec map spec =
- let visitor = new visitor map in
- ignore (Cil.visitCilFunspec (visitor:>Cil.cilVisitor) spec)
-
-(* -------------------------------------------------------------------------- *)
-(* --- L-path Iterator --- *)
-(* -------------------------------------------------------------------------- *)
-
-open RegionAnnot
-
-let iter_star map f t r =
- let pointed = add_pointed map r in
- acs_deref pointed (Deref,t) ; f pointed
-
-let iter_shift map f t r =
- let pointed = add_pointed map r in
- acs_deref pointed (Array,t) ; f r
-
-let iter_index map f tarr r =
- f (add_offset map r (Offset.index tarr))
-
-let iter_fields map f fds r =
- List.iter (fun fd -> f (add_offset map r (Offset.field fd))) fds
-
-let rec iter_lpath map f lv =
- match lv.lnode with
- | L_var x -> f (of_cvar map x)
- | L_region a -> f (of_name map a)
- | L_cast(_,a) -> iter_lpath map f a
- | L_addr a -> iter_lpath map (fun r -> f (get_addrof map r)) a
- | L_star(te,a) -> iter_lpath map (iter_star map f te) a
- | L_shift(a,te,_) -> iter_lpath map (iter_shift map f te) a
- | L_index(a,_,_) -> iter_lpath map (iter_index map f lv.ltype) a
- | L_field(a,fs) -> iter_lpath map (iter_fields map f fs) a
-
-(* -------------------------------------------------------------------------- *)
-(* --- Region Specs --- *)
-(* -------------------------------------------------------------------------- *)
-
-let cc_lpath map rclass _rpattern lv =
- iter_lpath map (Region.add_alias map ~into:rclass) lv
-
-let cc_region map spec =
- let rclass = Region.of_class map spec.region_name in
- let rpattern = spec.region_pattern in
- List.iter (cc_lpath map rclass rpattern) spec.region_lpath
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/RegionAccess.mli b/src/plugins/wp/RegionAccess.mli
deleted file mode 100644
index b422f3af429e2fd85d7c7b09ec2e39973733e0ac..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionAccess.mli
+++ /dev/null
@@ -1,42 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Region
-
-(* -------------------------------------------------------------------------- *)
-
-val cc_lval : map -> lval -> region
-val cc_read : map -> exp -> unit
-val cc_assign : map -> stmt -> lval -> exp -> unit
-val cc_init : map -> stmt -> lval -> init -> unit
-val cc_instr : map -> stmt -> instr -> unit
-val cc_fundec : map -> fundec -> unit
-
-val cc_pred : map -> predicate -> unit
-val cc_term : map -> term -> unit
-val cc_spec : map -> spec -> unit
-
-open RegionAnnot
-val cc_region : map -> region_spec -> unit
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/RegionAnalysis.ml b/src/plugins/wp/RegionAnalysis.ml
deleted file mode 100644
index 6a97a95abac711cf459f44063e4007314675d855..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionAnalysis.ml
+++ /dev/null
@@ -1,116 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-module Wp = Wp_parameters
-module Kf = Kernel_function
-
-(* ---------------------------------------------------------------------- *)
-(* --- Compute Analysis --- *)
-(* ---------------------------------------------------------------------- *)
-
-let compute kf =
- let map = Region.create () in
- if Kf.is_definition kf then
- begin
- Wp.feedback ~ontty:`Transient "[region] Analyzing %a" Kf.pretty kf ;
- let def = Kf.get_definition kf in
- RegionAccess.cc_fundec map def ;
- Populate_spec.populate_funspec kf [`Assigns];
- let spec = Annotations.funspec kf in
- RegionAccess.cc_spec map spec ;
- List.iter
- (fun bhv ->
- let region_specs = RegionAnnot.of_behavior bhv in
- if region_specs <> [] then
- if Cil.is_default_behavior bhv then
- List.iter (RegionAccess.cc_region map) region_specs
- else
- Wp.warning ~once:true
- "Region specifications in non-default behaviours are skipped."
- ) spec.spec_behavior ;
- if Wp.Region_fixpoint.get () then Region.fixpoint map ;
- end ;
- map
-
-(* ---------------------------------------------------------------------- *)
-(* --- Projectified Analysis Result --- *)
-(* ---------------------------------------------------------------------- *)
-
-module REGION = Datatype.Make
- (struct
- type t = Region.map
- include Datatype.Undefined
- let reprs = [Region.create ()]
- let name = "Wp.RegionAnalysis.region"
- let mem_project = Datatype.never_any_project
- end)
-
-module GLOBAL = State_builder.Ref
- (REGION)
- (struct
- let name = "Wp.RegionAnalysis.ref"
- let dependencies = [Ast.self]
- let default = Region.create
- end)
-
-module REGISTRY = State_builder.Hashtbl
- (Kernel_function.Hashtbl)
- (REGION)
- (struct
- let name = "Wp.RegionAnalysis.registry"
- let dependencies = [Ast.self]
- let size = 32
- end)
-
-let get = function
- | None -> GLOBAL.get ()
- | Some kf ->
- try REGISTRY.find kf
- with Not_found ->
- let map = compute kf in
- REGISTRY.add kf map ; map
-
-(* ---------------------------------------------------------------------- *)
-(* --- Command Line Registry --- *)
-(* ---------------------------------------------------------------------- *)
-
-let main () =
- if Wp.Region.get () then
- begin
- Ast.compute () ;
- let dump =
- if Wp_parameters.Region_output_dot.is_set () then
- RegionDump.dump_in_file ~file:(Wp_parameters.Region_output_dot.get())
- else
- RegionDump.dump_in_dir ~dir:(Wp.get_output_dir "region")
- in
- Wp.iter_kf (fun kf ->
- let map = get (Some kf) in
- if not (Region.is_empty map) then
- dump (Kernel_function.get_name kf) map
- ) ;
- end
-
-let () = Boot.Main.extend main
-
-(* ---------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/RegionAnalysis.mli b/src/plugins/wp/RegionAnalysis.mli
deleted file mode 100644
index d3d4b6998d5bee5ab060a3c3c96372066d5c0be8..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionAnalysis.mli
+++ /dev/null
@@ -1,29 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-
-(* -------------------------------------------------------------------------- *)
-
-(** Memoized and Projectified Region Analyzis for the given Function. *)
-val get : Kernel_function.t option -> Region.map
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/RegionAnnot.ml b/src/plugins/wp/RegionAnnot.ml
deleted file mode 100644
index f2697affd43569089fda263bbf4cb02213b1f987..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionAnnot.ml
+++ /dev/null
@@ -1,507 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-open Cil_datatype
-open Logic_ptree
-
-module Wp = Wp_parameters
-
-(* -------------------------------------------------------------------------- *)
-(* --- L-Path --- *)
-(* -------------------------------------------------------------------------- *)
-
-type region_pattern =
- | FREE
- | PVAR
- | PREF
- | PMEM
- | PVECTOR
- | PMATRIX
-
-type lrange =
- | R_index of term
- | R_range of term option * term option
-
-type lpath = {
- loc : location ;
- lnode : lnode ;
- ltype : typ ;
-}
-and lnode =
- | L_var of varinfo
- | L_region of string
- | L_addr of lpath
- | L_star of typ * lpath
- | L_shift of lpath * typ * lrange
- | L_index of lpath * typ * lrange
- | L_field of lpath * fieldinfo list
- | L_cast of typ * lpath
-
-type region_spec = {
- region_name: string option ;
- region_pattern: region_pattern ;
- region_lpath: lpath list ;
-}
-
-(*
-let get_int e =
- match Logic_utils.constFoldTermToInt e with
- | None -> None
- | Some a -> Some (Integer.to_int_exn a)
-
-let get_int_option = function
- | None -> None
- | Some e -> get_int e
-*)
-
-module Lpath =
-struct
-
- type t = lpath
-
- let compare_bound a b =
- match a,b with
- | None , None -> 0
- | Some a , Some b -> Term.compare a b
- | None , Some _ -> (-1)
- | Some _ , None -> 1
-
- let compare_range a b =
- match a,b with
- | R_index a , R_index b -> Term.compare a b
- | R_index _ , _ -> (-1)
- | _ , R_index _ -> 1
- | R_range(a1,b1) , R_range(a2,b2) ->
- let cmp = compare_bound a1 a2 in
- if cmp <> 0 then cmp else compare_bound b1 b2
-
- let rec compare a b =
- match a.lnode , b.lnode with
- | L_var x , L_var y -> Varinfo.compare x y
- | L_var _ , _ -> (-1)
- | _ , L_var _ -> 1
- | L_region a , L_region b -> String.compare a b
- | L_region _ , _ -> (-1)
- | _ , L_region _ -> 1
- | L_star(ta,a) , L_star(tb,b) ->
- let cmp = Typ.compare ta tb in
- if cmp <> 0 then cmp else compare a b
- | L_star _ , _ -> (-1)
- | _ , L_star _ -> 1
- | L_addr a , L_addr b -> compare a b
- | L_addr _ , _ -> (-1)
- | _ , L_addr _ -> 1
- | L_shift(a,ta,i) , L_shift(b,tb,j) -> compare_index a ta i b tb j
- | L_shift _ , _ -> (-1)
- | _ , L_shift _ -> 1
- | L_index(a,ta,i) , L_index(b,tb,j) -> compare_index a ta i b tb j
- | L_index _ , _ -> (-1)
- | _ , L_index _ -> 1
- | L_field(a,fs) , L_field(b,gs) ->
- let cmp = compare a b in
- if cmp <> 0 then cmp
- else Qed.Hcons.compare_list Fieldinfo.compare fs gs
- | L_field _ , _ -> (-1)
- | _ , L_field _ -> 1
- | L_cast(ta,a) , L_cast(tb,b) ->
- let cmp = Typ.compare ta tb in
- if cmp <> 0 then cmp else compare a b
-
- and compare_index a ta i b tb j =
- let cmp = compare a b in
- if cmp <> 0 then cmp else
- let cmp = Typ.compare ta tb in
- if cmp <> 0 then cmp else
- compare_range i j
-
- let equal a b = (compare a b = 0)
-
- let pp_bound pp fmt = function None -> () | Some a -> pp fmt a
- let pp_range pp fmt = function
- | R_index a -> pp fmt a
- | R_range(a,b) ->
- begin
- pp_bound pp fmt a ;
- Format.fprintf fmt "@,.." ;
- pp_bound pp fmt b ;
- end
-
- let first = function [] -> assert false | f::_ -> f
- let rec last = function [] -> assert false | [f] -> f | _::fs -> last fs
-
- let is_lval = function
- | L_var _ | L_region _ | L_index _ | L_field _ -> true
- | _ -> false
-
- let rec pp_lpath pp fmt a = match a.lnode with
- | L_var x -> Varinfo.pretty fmt x
- | L_region a -> Format.pp_print_string fmt a
- | L_field( p , [f] ) -> pfield pp p f fmt
- | L_field( p , fs ) ->
- Format.fprintf fmt "@[<hov 2>(%t@,..%t)@]"
- (pfield pp p (first fs)) (pfield pp p (last fs))
- | L_index(a,_,i) ->
- Format.fprintf fmt "@[<hov 2>%a@,[%a]@]"
- (pp_lval pp) a (pp_range pp) i
- | L_shift(a,_,i) ->
- Format.fprintf fmt "@[<hov 2>%a@,+(%a)@]"
- (pp_lpath pp) a (pp_range pp) i
- | L_star(_,a) -> Format.fprintf fmt "*%a" (pp_lval pp) a
- | L_addr a -> Format.fprintf fmt "&%a" (pp_lval pp) a
- | L_cast(t,a) -> Format.fprintf fmt "(%a)@,%a" Typ.pretty t (pp_lval pp) a
-
- and pfield pp a f fmt =
- Format.fprintf fmt "@[<hov 2>%a%a@]" (panchor pp) a Fieldinfo.pretty f
-
- and panchor pp fmt a =
- match a.lnode with
- | L_star(_,p) -> Format.fprintf fmt "%a@,->" (pp_lval pp) p
- | _ -> Format.fprintf fmt "%a@,." (pp_lval pp) a
-
- and pp_lval pp fmt a =
- if is_lval a.lnode then pp_lpath pp fmt a
- else Format.fprintf fmt "(%a)" (pp_lpath pp) a
-
- let pretty = pp_lpath Term.pretty
-
-end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Region Spec Printer --- *)
-(* -------------------------------------------------------------------------- *)
-
-let patterns = [
- "PVAR" , PVAR ;
- "PREF" , PREF ;
- "PMEM" , PMEM ;
- "PVECTOR" , PVECTOR ;
- "PMATRIX" , PMATRIX ;
-]
-
-let p_name p = fst (List.find (fun (_,q) -> q = p) patterns)
-
-let pp_pattern_spec fmt p =
- try Format.fprintf fmt "\\pattern{%s}" (p_name p) ; true
- with Not_found -> false
-
-let pp_path_spec pp fmt coma lv =
- if coma then Format.fprintf fmt ",@ " ;
- Lpath.pp_lpath pp fmt lv ; true
-
-let pp_region_spec pp fmt coma spec =
- begin
- if coma then Format.fprintf fmt ",@ " ;
- Format.fprintf fmt "@[<hv 2>" ;
- Option.iter (Format.fprintf fmt "%s:@ ") spec.region_name ;
- let coma = pp_pattern_spec fmt spec.region_pattern in
- let coma = List.fold_left (pp_path_spec pp fmt) coma spec.region_lpath in
- Format.fprintf fmt "@]" ;
- coma
- end
-
-(* -------------------------------------------------------------------------- *)
-(* --- Typing Env --- *)
-(* -------------------------------------------------------------------------- *)
-
-type env = {
- context : Logic_typing.typing_context ;
- mutable declared : string list ;
- mutable name : string option ;
- mutable pattern : region_pattern ;
- mutable paths : lpath list ;
- mutable specs : region_spec list ;
-}
-
-let error env ~loc msg = env.context.Logic_typing.error loc msg
-
-let flush env =
- let region_name = env.name in env.name <- None ;
- let region_pattern = env.pattern in env.pattern <- FREE ;
- let region_lpath = List.rev env.paths in env.paths <- [] ;
- Option.iter (fun a -> env.declared <- a::env.declared) region_name ;
- if not (region_name = None && region_lpath = []) then
- let region = { region_name ; region_pattern ; region_lpath } in
- env.specs <- region :: env.specs
-
-(* -------------------------------------------------------------------------- *)
-(* --- Type Utils --- *)
-(* -------------------------------------------------------------------------- *)
-
-let isIndexType t =
- match Logic_utils.unroll_type t with
- | Ctype (TInt _) | Linteger -> true
- | _ -> false
-
-let getCompoundType env ~loc typ =
- match Cil.unrollType typ with
- | TComp(comp,_) -> comp
- | _ -> error env ~loc "Expected compound type for term"
-
-(* -------------------------------------------------------------------------- *)
-(* --- Path Typechecking --- *)
-(* -------------------------------------------------------------------------- *)
-
-let parse_varinfo env ~loc x =
- try
- match env.context.Logic_typing.find_var x with
- | { lv_origin = Some v } -> v
- | _ -> error env ~loc "Variable '%s' is not a C-variable" x
- with Not_found ->
- error env ~loc "Unknown variable (or region) '%s'" x
-
-let parse_fieldinfo env ~loc comp f =
- try List.find (fun fd -> fd.fname = f) (Option.value ~default:[] comp.cfields)
- with Not_found ->
- error env ~loc "No field '%s' in compound type '%s'" f comp.cname
-
-let parse_lindex env e =
- let open Logic_typing in
- let g = env.context in
- let t = g.type_term g g.pre_state e in
- if isIndexType t.term_type then t
- else error env ~loc:t.term_loc "Index term shall have a integer type"
-
-let parse_ltype env ~loc t =
- let open Logic_typing in
- let g = env.context in
- let t = g.logic_type g loc g.pre_state t in
- match Logic_utils.unroll_type t with
- | Ctype typ -> typ
- | _ -> error env ~loc "C-type expected for casting l-values"
-
-let parse_lbound env = function
- | None -> None
- | Some e -> Some (parse_lindex env e)
-
-let parse_lrange env e =
- match e.lexpr_node with
- | PLrange(a,b) -> R_range( parse_lbound env a , parse_lbound env b )
- | _ -> R_index( parse_lindex env e )
-
-let sugar ~loc node = { lexpr_loc = loc ; lexpr_node = node }
-
-let rec field_range ~inside fa fb = function
- | [] -> []
- | f::fs ->
- let bound = Fieldinfo.equal f fa || Fieldinfo.equal f fb in
- if inside then f :: (if bound then [] else field_range ~inside fa fb fs)
- else if bound then f :: (field_range ~inside:true fa fb fs)
- else field_range ~inside fa fb fs
-
-let rec typeof_fields = function
- | [] -> TVoid []
- | [f] -> f.ftype
- | f::fs ->
- let t = typeof_fields fs in
- if Typ.equal f.ftype t then t else TVoid []
-
-let rec parse_lpath env e =
- let loc = e.lexpr_loc in
- match e.lexpr_node with
- | PLvar x ->
- if List.mem x env.declared
- then { loc ; lnode = L_region x ; ltype = TVoid [] }
- else
- let v = parse_varinfo env ~loc x in
- { loc ; lnode = L_var v ; ltype = v.vtype }
- | PLunop( Ustar , p ) ->
- let lv = parse_lpath env p in
- if Cil.isPointerType lv.ltype then
- let te = Cil.typeOf_pointed lv.ltype in
- { loc ; lnode = L_star(te,lv) ; ltype = te }
- else
- error env ~loc "Pointer-type expected for operator '&'"
- | PLunop( Uamp , p ) ->
- let lv = parse_lpath env p in
- let ltype = TPtr( lv.ltype , [] ) in
- { loc ; lnode = L_addr lv ; ltype }
- | PLbinop( p , Badd , r ) ->
- let { ltype } as lv = parse_lpath env p in
- let rg = parse_lrange env r in
- if Cil.isPointerType ltype then
- let te = Cil.typeOf_pointed ltype in
- { loc ; lnode = L_shift(lv,te,rg) ; ltype = ltype }
- else
- if Cil.isArrayType ltype then
- let te = Cil.typeOf_array_elem ltype in
- { loc ; lnode = L_shift(lv,te,rg) ; ltype = TPtr(te,[]) }
- else
- error env ~loc "Pointer-type expected for operator '+'"
- | PLdot( p , f ) ->
- let lv = parse_lpath env p in
- let comp = getCompoundType env ~loc:lv.loc lv.ltype in
- let fd = parse_fieldinfo env ~loc comp f in
- { loc ; lnode = L_field(lv,[fd]) ; ltype = fd.ftype }
- | PLarrow( p , f ) ->
- let sp = sugar ~loc (PLunop(Ustar,p)) in
- let pf = sugar ~loc (PLdot(sp,f)) in
- parse_lpath env pf
- | PLarrget( p , k ) ->
- let { ltype } as lv = parse_lpath env p in
- let rg = parse_lrange env k in
- if Cil.isPointerType ltype then
- let pointed = Cil.typeOf_pointed ltype in
- let ls = { loc ; lnode = L_shift(lv,pointed,rg) ; ltype } in
- { loc ; lnode = L_star(pointed,ls) ; ltype = pointed }
- else
- if Cil.isArrayType ltype then
- let elt = Cil.typeOf_array_elem ltype in
- { loc ; lnode = L_index(lv,elt,rg) ; ltype = elt }
- else
- error env ~loc:lv.loc "Pointer or array type expected"
- | PLcast( t , a ) ->
- let lv = parse_lpath env a in
- let ty = parse_ltype env ~loc t in
- { loc ; lnode = L_cast(ty,lv) ; ltype = ty }
- | PLrange( Some a , Some b ) ->
- let pa,fa = parse_fpath env a in
- let pb,fb = parse_fpath env b in
- let p =
- if Lpath.equal pa pb then pa
- else error env ~loc "Range of fields from different l-values" in
- let comp =
- if Compinfo.equal fa.fcomp fb.fcomp then fa.fcomp
- else error env ~loc "Range of fields from incompatible types" in
- let fields =
- field_range ~inside:false fa fb
- (Option.value ~default:[] comp.cfields)
- in
- let ltype = typeof_fields fields in
- { loc ; lnode = L_field(p,fields) ; ltype }
- | PLrange( Some a , None ) ->
- let p,fd = parse_fpath env a in
- let fields =
- field_range ~inside:false fd fd
- (Option.value ~default:[] fd.fcomp.cfields)
- in
- let ltype = typeof_fields fields in
- { loc ; lnode = L_field(p,fields) ; ltype }
- | PLrange( None , Some a ) ->
- let p,fd = parse_fpath env a in
- let fields =
- field_range ~inside:true fd fd
- (Option.value ~default:[] fd.fcomp.cfields)
- in
- let ltype = typeof_fields fields in
- { loc ; lnode = L_field(p,fields) ; ltype }
- | _ ->
- error env ~loc "Unexpected expression for region spec"
-
-and parse_fpath env p =
- let lv = parse_lpath env p in
- match lv.lnode with
- | L_field( a , [f] ) -> a , f
- | _ -> error env ~loc:lv.loc "Missing field access in range"
-
-(* -------------------------------------------------------------------------- *)
-(* --- Spec Typechecking --- *)
-(* -------------------------------------------------------------------------- *)
-
-let kspec = ref 0
-let registry = Hashtbl.create 0
-
-let parse_pattern env ~loc names params =
- match names with
- | [name] ->
- let pattern =
- try List.assoc name patterns
- with Not_found -> error env ~loc "Unknown pattern '%s'" name in
- if params <> [] then
- error env ~loc "Unexpected parameters for pattern '%s'" name ;
- pattern
- | [] -> error env ~loc "Missing pattern name"
- | _ -> error env ~loc "Duplicate pattern names"
-
-let rec parse_region env p =
- let loc = p.lexpr_loc in
- match p.lexpr_node with
- | PLnamed( name , p ) ->
- flush env ;
- env.name <- Some name ;
- parse_region env p
- | PLapp("\\pattern",names,params) ->
- let pattern = parse_pattern env ~loc names params in
- if env.pattern <> FREE && env.pattern <> pattern then
- error env ~loc "Duplicate pattern definition in region"
- else
- env.pattern <- pattern
- | _ ->
- let path = parse_lpath env p in
- env.paths <- path :: env.paths
-
-let typecheck typing_context _loc ps =
- let env = {
- name = None ;
- declared = [] ;
- context = typing_context ;
- pattern = FREE ;
- paths = [] ; specs = [] ;
- } in
- List.iter (parse_region env) ps ;
- let id = !kspec in incr kspec ;
- let specs = flush env ; env.specs in
- Hashtbl.add registry id specs ; Ext_id id
-
-(* -------------------------------------------------------------------------- *)
-(* --- Registry --- *)
-(* -------------------------------------------------------------------------- *)
-
-let of_extid = Hashtbl.find registry
-let of_extrev = function
- | { 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 =
- List.fold_left
- (fun acc e -> List.rev_append (try of_extrev e with Not_found -> []) acc)
- [] bhv.Cil_types.b_extended
-
-let pp_extension printer fmt = function
- | Ext_id k ->
- let spec = try Hashtbl.find registry k with Not_found -> [] in
- ignore (List.fold_left (pp_region_spec printer#term fmt) false spec)
- | _ -> ()
-
-let specified =
- let re = Str.regexp_case_fold "region" in
- fun model ->
- try
- ignore (Str.search_forward re model 0) ; true
- with Not_found -> false
-
-let registered = ref false
-let register () =
- if not !registered && (
- Wp.Region.get () || Wp.Region_annot.get () ||
- List.exists specified (Wp.Model.get ())
- )
- then
- begin
- registered := true ;
- Acsl_extension.register_behavior ~plugin:"wp" "wpregion"
- typecheck ~printer:pp_extension false
- end
-
-let () = Cmdline.run_after_configuring_stage register
-
-(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/RegionAnnot.mli b/src/plugins/wp/RegionAnnot.mli
deleted file mode 100644
index 7ebe1d8ed6247ccb8db8f12cd9ba0e48aa661fde..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionAnnot.mli
+++ /dev/null
@@ -1,70 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-open Cil_types
-
-type lrange =
- | R_index of term
- | R_range of term option * term option
-
-type lpath = {
- loc : location ;
- lnode : lnode ;
- ltype : typ ;
-}
-and lnode =
- | L_var of varinfo
- | L_region of string
- | L_addr of lpath
- | L_star of typ * lpath
- | L_shift of lpath * typ * lrange
- | L_index of lpath * typ * lrange
- | L_field of lpath * fieldinfo list
- | L_cast of typ * lpath
-
-module Lpath :
-sig
- type t = lpath
- val equal : t -> t -> bool
- val compare : t -> t -> int
- val pretty : Format.formatter -> t -> unit
-end
-
-type region_pattern =
- | FREE
- | PVAR
- | PREF
- | PMEM
- | PVECTOR
- | PMATRIX
-
-type region_spec = {
- region_name: string option ;
- region_pattern: region_pattern ;
- region_lpath: lpath list ;
-}
-
-val p_name : region_pattern -> string
-val of_extension : acsl_extension -> region_spec list
-val of_behavior : behavior -> region_spec list
-
-val register : unit -> unit (** Auto when `-wp-region` *)
diff --git a/src/plugins/wp/RegionDump.ml b/src/plugins/wp/RegionDump.ml
deleted file mode 100644
index 87ba674bee5ce22df81b134ea30a9a2248d3b739..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionDump.ml
+++ /dev/null
@@ -1,297 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-module Wp = Wp_parameters
-module G = Dotgraph
-module R = G.Node(Region.Map)
-
-let node_default = [`Attr("fontname","monospace")]
-let edge_default = [`Attr("fontname","monospace")]
-
-let attr_offset = [ `Filled ; `Color "grey" ; `Box ]
-let attr_write = [ `Label "W" ; `Fillcolor "green" ; `Filled ]
-let attr_read = [ `Label "R" ; `Fillcolor "green" ; `Filled ]
-let attr_alias = [ `Label "&" ; `Fillcolor "orange" ; `Filled ]
-let attr_merge = [ `Color "red" ; `Fillcolor "red" ; `Filled ]
-let attr_shift = [ `Label "[]" ]
-let attr_delta = [ `Filled ; `Color "lightblue" ; `Box ]
-let attr_deref = [ `ArrowHead "tee" ]
-let attr_cil = [ `Filled ; `Fillcolor "yellow" ]
-let attr_region = `Shape "tab" :: attr_cil
-let attr_var = `Shape "cds" :: attr_cil
-let attr_garbled = [`Fillcolor "red";`Filled]
-let attr_froms = [ `Color "blue" ; `Attr("dir","back") ]
-
-let attr_pointed = [
- `Color "red"
-]
-
-let attr_pointed_deref = [
- `Attr("taillabel","*");
- `Attr("labelangle","+30");
- `Color "red";
-]
-
-let attr_pointed_shift = [
- `Attr("taillabel","[..]");
- `Attr("labeldistance","1.7");
- `Attr("labelangle","+40");
- `Color "red";
-]
-
-let rid_key = Wp.register_category "rid"
-let dot_key = Wp.register_category "dot"
-let pdf_key = Wp.register_category "pdf"
-let deref_key = Wp.register_category "deref"
-let roots_key = Wp.register_category "roots"
-let froms_key = Wp.register_category "froms"
-let cluster_key = Wp.register_category "cluster"
-let chunk_key = Wp.register_category "chunk"
-let offset_key = Wp.register_category "offset"
-
-let sfprintf = Format.asprintf
-
-let dotpointed ~label r =
- let attr =
- if Region.is_shifted r
- then attr_pointed_shift else attr_pointed_deref in
- let target = G.port (R.get r) "w" in
- `Port ("",["",attr,target],label)
-
-let dotvalue ?(prefix="") value : Dotgraph.record =
- let open Layout in
- match value with
- | Int i -> `Label (sfprintf "%s%a" prefix Ctypes.pp_int i)
- | Float f -> `Label (sfprintf "%s%a" prefix Ctypes.pp_float f)
- | Pointer r -> dotpointed ~label:(prefix ^ "ptr") r
-
-let dotrange ?(prefix="") rg : Dotgraph.record =
- let open Layout in
- let pp_dim fmt = function
- | Raw _ -> Format.pp_print_string fmt "raw"
- | Dim(s,ds) -> Format.fprintf fmt "%d%a" s Matrix.pretty ds
- in
- let label = sfprintf "%d..%d: %s%a"
- rg.ofs (rg.ofs + rg.len - 1)
- prefix pp_dim rg.dim in
- `Port("",["",[`Dotted],R.get rg.reg],label)
-
-let dotcluster cluster : Dotgraph.record =
- let open Layout in
- match cluster with
- | Empty -> `Label "-"
- | Garbled -> `Label "Garbled"
- | Chunk v -> dotvalue v
- | Layout { sizeof ; layout } ->
- let label = Printf.sprintf "sizeof:%d" sizeof in
- `Hbox (`Label label :: List.map dotrange layout)
-
-let dotchunk mem : Dotgraph.record =
- let open Layout in
- match mem with
- | Mraw(_,None) -> `Label "Raw"
- | Mraw(_,Some r) -> dotpointed ~label:"Raw" r
- | Mref r -> dotpointed ~label:"Ref" r
- | Mmem(rt,v) ->
- let prefix = if Layout.Root.indexed rt then "Mem " else "Var " in
- dotvalue ~prefix v
- | Mcomp(_,ovl) ->
- let range rg = dotrange
- ~prefix:(if Overlay.once rg.reg ovl then "D" else "C") rg in
- `Hbox (List.map range ovl)
-
-let dotregion dot map region node =
- begin
- let is_read = Region.is_read region in
- let is_written = Region.is_written region in
- let is_aliased = Region.is_aliased region in
- let is_accessed = is_read || is_written || is_aliased in
- let has_deref = Wp.has_dkey deref_key && Region.has_deref region in
- let has_roots = Wp.has_dkey roots_key && Region.has_roots map region in
- let has_index_infos = has_deref || has_roots in
- let has_side_cluster =
- is_accessed ||
- has_index_infos ||
- Region.has_names region ||
- Wp.has_dkey offset_key ||
- Wp.has_dkey rid_key ||
- not (Wp.has_dkey cluster_key || Wp.has_dkey chunk_key) ||
- not (Wp.Region_fixpoint.get ())
- in
- if has_side_cluster then
- begin
- let attr = G.decorate [ `Oval ] [
- is_read , attr_read ;
- Region.has_pointed region , [ `Label "D" ] ;
- is_written , attr_write ;
- Region.is_shifted region , attr_shift ;
- is_aliased , attr_alias ;
- Region.get_alias map region != region , attr_merge ;
- Region.is_garbled region , attr_merge ;
- ] in
- G.node dot node attr ;
- end ;
- if Wp.has_dkey offset_key then
- Region.iter_offset map
- (fun offset target ->
- let label = Pretty_utils.to_string Layout.Offset.pretty offset in
- let delta = G.inode dot (`Label label :: attr_offset) in
- G.link dot [node;delta;R.get target] [`Dotted]
- ) region ;
- if Wp.has_dkey offset_key then
- Option.iter
- (fun target ->
- let label = if Region.is_shifted target then "[..]" else "*" in
- let deref = G.inode dot (`Label label :: attr_offset) in
- G.link dot [node;deref;R.get target] attr_pointed
- ) (Region.get_pointed map region) ;
- if has_index_infos then
- begin
- let derefs = ref [] in
- let label s = derefs := s :: !derefs in
- if has_roots then
- label @@ sfprintf "roots:%a"
- Layout.Root.pretty (Region.get_roots map region) ;
- if has_deref then
- Region.iter_deref
- (fun deref ->
- label @@ Pretty_utils.to_string Layout.Deref.pretty deref
- ) region ;
- if !derefs <> [] then
- begin
- let label = String.concat "\n" (List.rev !derefs) in
- let delta = G.inode dot (`Label label :: attr_delta) in
- G.rank dot [node;delta] ;
- G.edge dot delta node attr_deref
- end
- end ;
- if Wp.has_dkey cluster_key then
- begin
- let cluster = Region.cluster map region in
- if not (has_side_cluster && Layout.Cluster.is_empty cluster) then
- let record = dotcluster cluster in
- let attr = if Region.is_garbled region then attr_garbled else [] in
- if has_side_cluster then
- let delta = G.irecord dot ~attr record in
- G.edge dot node (G.port delta "w") attr_deref
- else
- G.record dot node ~attr record
- end ;
- if Wp.has_dkey chunk_key then
- begin
- let chunk = Region.chunk map region in
- let record = dotchunk chunk in
- let attr = if Region.is_garbled region then attr_garbled else [] in
- if has_side_cluster then
- let delta = G.irecord dot ~attr record in
- G.edge dot node (G.port delta "w") attr_deref
- else
- G.record dot node ~attr record
- end ;
- if Wp.has_dkey froms_key then
- begin
- let open Layout in
- List.iter
- (function
- | Fvar _ -> ()
- | Farray r ->
- G.edge dot (R.get r) node (`Label "[]"::attr_froms)
- | Fderef r ->
- G.edge dot (R.get r) node (`Label "*"::attr_froms)
- | Findex r ->
- G.edge dot (R.get r) node (`Label "+(..)"::attr_froms)
- | Ffield(r,ofs) ->
- let label = Printf.sprintf "+%d" ofs in
- G.edge dot (R.get r) node (`Label label::attr_froms)
- ) (Region.get_froms map region)
- end ;
- Region.iter_copies map
- (fun target ->
- G.edge dot node (R.get target) [`Color "green"]
- ) region ;
- Option.iter
- (fun target ->
- G.edge dot node (R.get target) [`Color "red"]
- ) (Region.get_merged map region) ;
- end
-
-let dotvar dot x r =
- begin
- let open Cil_types in
- let xnode = G.inode dot ~prefix:"V" (`Label x.vname :: attr_var) in
- G.edge dot (G.port xnode "e") (R.get r) [] ;
- end
-
-let dotlabel dot a r =
- begin
- let anode = G.inode dot ~prefix:"R" (`Label a :: attr_region) in
- let rnode = R.get r in
- G.rank dot [ anode ; rnode ] ;
- G.edge dot anode rnode []
- end
-
-let dotrid dot r =
- dotlabel dot (Pretty_utils.to_string Region.R.pretty r) r
-
-let dotstr dot r cst =
- dotlabel dot (String.escaped cst) r
-
-let dotgraph dot map =
- begin
- G.node_default dot node_default ;
- G.edge_default dot edge_default ;
- R.clear () ;
- R.define dot (dotregion dot map) ;
- Region.iter_vars map (dotvar dot) ;
- Region.iter_strings map (dotstr dot) ;
- G.run dot ;
- if Wp.has_dkey rid_key then Region.iter map (dotrid dot) ;
- Region.iter_names map (dotlabel dot) ;
- if Region.has_return map then
- dotlabel dot "\\result" (Region.of_return map) ;
- Region.iter_fusion map (fun i r ->
- let rid = Region.id r in
- if i <> rid then
- dotlabel dot (Printf.sprintf "Fusion R%03d" i) r
- else
- dotlabel dot "Fusion (Self)" r
- ) ;
- G.run dot ;
- end
-
-let dump_in_file ~file name map =
- if Wp.has_dkey dot_key || Wp.has_dkey pdf_key then
- begin
- let file = Pretty_utils.to_string Datatype.Filepath.pretty file in
- let dot = Dotgraph.open_dot ~attr:[`LR] ~name ~file () in
- dotgraph dot map ;
- Dotgraph.close dot ;
- let outcome =
- if Wp.has_dkey pdf_key
- then Dotgraph.layout dot
- else file in
- Wp.result "Region Graph: %s" outcome
- end
-
-let dump_in_dir ~dir name map =
- let file = Datatype.Filepath.concat dir (name ^ ".dot") in
- dump_in_file ~file name map
diff --git a/src/plugins/wp/RegionDump.mli b/src/plugins/wp/RegionDump.mli
deleted file mode 100644
index ea54c4d40745762ccfb7421b16683695bdacefe8..0000000000000000000000000000000000000000
--- a/src/plugins/wp/RegionDump.mli
+++ /dev/null
@@ -1,28 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of WP plug-in of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2024 *)
-(* CEA (Commissariat a l'energie atomique et aux energies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-(* Dump region graphs to dir according to -wp options.
- By default, does nothing. *)
-
-val dump_in_dir : dir:Datatype.Filepath.t -> string -> Region.map -> unit
-
-val dump_in_file : file:Datatype.Filepath.t -> string -> Region.map -> unit
diff --git a/src/plugins/wp/gui/GuiPanel.ml b/src/plugins/wp/gui/GuiPanel.ml
index 9370b0fef04609219dd0251fab6b1cbb71f62264..8292028a5c6851fa95f60b7e7fe612d0e641d7c5 100644
--- a/src/plugins/wp/gui/GuiPanel.ml
+++ b/src/plugins/wp/gui/GuiPanel.ml
@@ -99,7 +99,7 @@ let run_and_prove
(* --- Model Panel --- *)
(* ------------------------------------------------------------------------ *)
-type memory = TREE | HOARE | TYPED | REGION | EVA
+type memory = TREE | HOARE | TYPED | EVA
class model_selector (main : Design.main_window_extension_points) =
let dialog = new Wpane.dialog
@@ -145,7 +145,6 @@ class model_selector (main : Design.main_window_extension_points) =
begin
(match s.mheap with
| ZeroAlias -> memory#set TREE
- | Region -> memory#set REGION
| Hoare -> memory#set HOARE
| Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
| Eva -> memory#set EVA
@@ -159,7 +158,6 @@ class model_selector (main : Design.main_window_extension_points) =
method get : setup =
let m = match memory#get with
| TREE -> ZeroAlias
- | REGION -> Region
| HOARE -> Hoare
| TYPED -> Typed
(if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
diff --git a/src/plugins/wp/tests/ptests_config b/src/plugins/wp/tests/ptests_config
index 5221e8c0f16237b724d4e1a878776e1b22e8ac88..d71d6024da0cf68a48b803c1cebd369561434d5f 100644
--- a/src/plugins/wp/tests/ptests_config
+++ b/src/plugins/wp/tests/ptests_config
@@ -1,8 +1,8 @@
DEFAULT_SUITES= wp wp_acsl wp_plugin wp_ce wp_bts wp_store wp_hoare
-DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
+DEFAULT_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip
qualif_SUITES= wp wp_acsl wp_plugin wp_bts wp_store wp_hoare
-qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_region wp_tip
+qualif_SUITES= wp_typed wp_usage wp_gallery wp_manual wp_tip
qualif_SUITES= why3
ce_SUITES= wp_ce
diff --git a/src/plugins/wp/tests/wp_bts/bts_2110.i b/src/plugins/wp/tests/wp_bts/bts_2110.i
index 2b30f0a37265c6096a082ec72db3c61e46fa31a7..30ca648fd0547ee1a6c6b5da2f5e9974e8078c7c 100644
--- a/src/plugins/wp/tests/wp_bts/bts_2110.i
+++ b/src/plugins/wp/tests/wp_bts/bts_2110.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp -wp-msg-key shell,cluster,print-generated -wp-prover why3 -wp-gen -wp-share @PTEST_SHARE_DIR@ -wp-warn-key "pedantic-assigns=inactive"
+ CMD: @frama-c@ -wp -wp-msg-key shell,print-generated -wp-prover why3 -wp-gen -wp-share @PTEST_SHARE_DIR@ -wp-warn-key "pedantic-assigns=inactive"
OPT:
*/
diff --git a/src/plugins/wp/tests/wp_plugin/model.i b/src/plugins/wp/tests/wp_plugin/model.i
index 07e59f63a7ddb17bc624dde14525f1dd14bcdee8..4475ecd7fd97e7a12c736b542050f49b1187f32f 100644
--- a/src/plugins/wp/tests/wp_plugin/model.i
+++ b/src/plugins/wp/tests/wp_plugin/model.i
@@ -1,5 +1,5 @@
/* run.config
- CMD: @frama-c@ -wp-share @PTEST_SHARE_DIR@ -wp-msg-key cluster,shell,print-generated -wp-prover why3 -wp-warn-key "pedantic-assigns=inactive"
+ CMD: @frama-c@ -wp-share @PTEST_SHARE_DIR@ -wp-msg-key shell,print-generated -wp-prover why3 -wp-warn-key "pedantic-assigns=inactive"
OPT: -wp-model Typed -wp -wp-gen -wp-print -then -wp-model Typed+ref -wp -wp-gen -wp-print
*/
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 54aa9413764131ff977dc1b9539a6f01c5c599fa..0000000000000000000000000000000000000000
--- 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 2312dafd8a402817ff5cc572dee05384826bd01c..0000000000000000000000000000000000000000
--- 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 fb6d84c2cb8cf463ae9e13dd1b6a159325899843..0000000000000000000000000000000000000000
--- 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 fb6d84c2cb8cf463ae9e13dd1b6a159325899843..0000000000000000000000000000000000000000
--- 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 bf3da7a503c8df46be495fd87a2d73c2c600b6c6..0000000000000000000000000000000000000000
--- 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 be59f8c030d72f6deb45f68ddcb7e2102e840a61..0000000000000000000000000000000000000000
--- 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 5035254bf8aaa6b247354033761c93d685946871..0000000000000000000000000000000000000000
--- 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 bc3b3b68375becdfef9d8e8bbffcc76fe9d9dc30..0000000000000000000000000000000000000000
--- 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 9fd9f2aa9f6e13083b6fb42918c613bec93e32c1..0000000000000000000000000000000000000000
--- 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 8136a3c37b0541a2fce551b0c69651d1214258d0..0000000000000000000000000000000000000000
--- 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 8178ba26808b9319194fdf1966fd1a6b1ce531cd..0000000000000000000000000000000000000000
--- 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 2ded4d8661dcd95ee85c15161272ee6de7fc3831..0000000000000000000000000000000000000000
--- 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 dc378f6d5e6eab79016343050256ad68545f2b7e..0000000000000000000000000000000000000000
--- 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 72629334e8a760da79b4436a7880cd15e41da5aa..0000000000000000000000000000000000000000
--- 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 f070fd5bb55354fb5e143e54c8b4bdc752c274a1..0000000000000000000000000000000000000000
--- 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 6b703ba4245ba130e45827ac182b69f5dd03dfdd..0000000000000000000000000000000000000000
--- 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 6151de509bc5b4fc3eb172d09db656921aae72fb..0000000000000000000000000000000000000000
--- 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 f5133222090c0c4e7e9bfc09ca31aa381523eb44..0000000000000000000000000000000000000000
--- 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 11a2a15408554226d844aa54f49e22a8df444ae6..0000000000000000000000000000000000000000
--- 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 8061a50b2de13b2a37de192630ce8e3dc7ca4ba7..0000000000000000000000000000000000000000
--- 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 f594dcb8a6c44253248bd7915208a98c026474a0..0000000000000000000000000000000000000000
--- 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 4e9b35936cb28e85a2e52c1329c3263720bd15f5..0000000000000000000000000000000000000000
--- 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 493acb0f32107b413f25d1e04f2ad9358d77e7fc..0000000000000000000000000000000000000000
--- 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 02d81fff4e3f858e95add60a92a064b67aad324f..0000000000000000000000000000000000000000
--- 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 ff1d6ff8c4774317d4469a6f9a31d287a36c489e..0000000000000000000000000000000000000000
--- 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 e885c887b4e821e26250b46ada6140d9bf34d4bb..0000000000000000000000000000000000000000
--- 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 a98da77e19cd9c9eb3fc069ff3394fd087dc3d1e..0000000000000000000000000000000000000000
--- 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 f017daa76b51774c4d4fa9f340f6e92c6b42d810..0000000000000000000000000000000000000000
--- 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 49fd11f80bd23706ec5b54ff355c2fcd1775e119..0000000000000000000000000000000000000000
--- 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 a55f8bb5e6ea2b6edd1878b2c9e765168e6aa0e7..0000000000000000000000000000000000000000
--- 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 814e494ce84b36a29c84ac8253300456d1127889..0000000000000000000000000000000000000000
--- 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 e4b91ca2a02e735f39c91a531d400469093f4cd9..0000000000000000000000000000000000000000
--- 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 8bd34f4ece859e898fb01537baec9fe233b95f96..0000000000000000000000000000000000000000
--- 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 f062fa1492fad2f399e0458c6bb0dd25153c5714..0000000000000000000000000000000000000000
--- 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 045b9aa75392eb340e5721978817f7c314f76137..0000000000000000000000000000000000000000
--- 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 e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
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 c6648e78e8fafdbed4725292d27a9c09e54893e1..0000000000000000000000000000000000000000
--- 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 c174f1f4537b111fc04000bee0674114dd058fd4..0000000000000000000000000000000000000000
--- 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 c278bffd20975f825e0e81a8884920114b062563..0000000000000000000000000000000000000000
--- 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 bfcc8d4d3ca21cf73c28dcb50c0f414a8ac16774..0000000000000000000000000000000000000000
--- 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 1f13727a1f33006dd8dc3a85b608b3e74a1b5dc3..0000000000000000000000000000000000000000
--- 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 c390ec3e2ade1fc8b4890a2f7602092b90108f78..0000000000000000000000000000000000000000
--- 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 5aea05755a41cc4c8ae8eaf06c3a06ed763927e8..0000000000000000000000000000000000000000
--- 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 953037c02faad26a8582d6e58dfd2e5f879cff63..0000000000000000000000000000000000000000
--- 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 fcce73f07e94697143a17a714e1605709e77c9f6..0000000000000000000000000000000000000000
--- 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 01ca9097b9dfeb8be0bd47e99aa5de6975d8931e..0000000000000000000000000000000000000000
--- 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 c9b16ac8ffe732d0e3f0782dc984f4254a571ad3..0000000000000000000000000000000000000000
--- 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 393a63b149847c622bb8740e221e706652f5e603..0000000000000000000000000000000000000000
--- 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 c230c91fe3fba56ccab5ad31aeb5b20e6952036a..0000000000000000000000000000000000000000
--- 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 f71c9e902cc6a49c9f5b16bf570b5fd58216c719..0000000000000000000000000000000000000000
--- 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 8f7746c098f792497d8e861672c41824c426e180..0000000000000000000000000000000000000000
--- 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 1e7d3cfb40046d4e352658865cad70b70e222e9a..0000000000000000000000000000000000000000
--- 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 7e75e99526513c32b32f184aa7c173118bac28b1..0000000000000000000000000000000000000000
--- 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 0f68a735ae39b5918b9e2fda64ca0d901879e306..0000000000000000000000000000000000000000
--- 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 f4e8e067375c647f46f431296f159c8600f387aa..0000000000000000000000000000000000000000
--- 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 77078dae158d2c0aab7dffec8982c49d0d4cbeb8..0000000000000000000000000000000000000000
--- 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 e7bafef6d0ddb31c0c6b0bfbae553ed91e43a9ab..0000000000000000000000000000000000000000
--- 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 f65e5113a5de004f1735416feae1c6cccf9a2d17..0000000000000000000000000000000000000000
--- 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 8a0eef80a86db86ded3c0259766b6e8dfa11d6a4..0000000000000000000000000000000000000000
--- 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 43b02d2fdd5eca9ca26e7690ae3c8efd1c0dcb38..0000000000000000000000000000000000000000
--- 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 5dde4c62c227399d8568f8137b8e4b57221e8be6..0000000000000000000000000000000000000000
--- 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 87e0d0c26bf0a990fc829a839352f75b8e656f4e..0000000000000000000000000000000000000000
--- 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 58b7b84d760ce95e3c5d23a2c98b6be7086f2946..0000000000000000000000000000000000000000
--- 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 ee372986dc5310bb4f6978e2add72844ddf3da6b..0000000000000000000000000000000000000000
--- 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 65aa343de9a1b94acd10ff6274490c5a3f722d8c..0000000000000000000000000000000000000000
--- 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 eed91319fd7abab0f314fbbdfd71c1753ae78784..0000000000000000000000000000000000000000
--- 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 ef140ddb0945880bdc5b4a9fe7961a59f61aa854..0000000000000000000000000000000000000000
--- 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 514228d38dc3ab6a10dcfa8d33622f0628694515..0000000000000000000000000000000000000000
--- 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 2b4866fb08ab090c40ba740c4ccd906303dbc66c..0000000000000000000000000000000000000000
--- 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 ffb1d191f763685a760f84611bab0e15f56c7a1f..0000000000000000000000000000000000000000
--- 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 7625bb9224d3c4d3945cbc4efb68da60ffe10d52..0000000000000000000000000000000000000000
--- 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 ecc9c7ec63c066d46c5bf594011263da37558e9f..0000000000000000000000000000000000000000
--- 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 f71833e1171a8e563ddc262e66b27fa1d38b1a77..0000000000000000000000000000000000000000
--- 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 ee37192b8778fae5286ec682656d921730952fbe..0000000000000000000000000000000000000000
--- 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 e8fb0e753eb65c3fb5fd35c27ba3bd74b16cf5e9..0000000000000000000000000000000000000000
--- 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 472077d231c95dd046d466e3f7871abe3e46ad43..0000000000000000000000000000000000000000
--- 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 fc05e0a87a77b692fcd6a4106ffcf7532a7dd039..0000000000000000000000000000000000000000
--- 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 c27ac7ed8f7fa1ea3ea5a52a0c1e87b0a23a1bd9..0000000000000000000000000000000000000000
--- 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 f299d9687047b1df56a724cb770bc950972274f0..0000000000000000000000000000000000000000
--- 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 4d45c6ca7df1a65ec039b874d56601b4cf276e50..0000000000000000000000000000000000000000
--- 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 4cd9b34453a93bc0bdedc29d321928e781110942..0000000000000000000000000000000000000000
--- 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
diff --git a/src/plugins/wp/wp.ml b/src/plugins/wp/wp.ml
index 1c5a2d30adcc83efcba2be5271dc21ffaf8119a1..abeb0a7931bed7a557bac4234534ecc5a5447fdf 100644
--- a/src/plugins/wp/wp.ml
+++ b/src/plugins/wp/wp.ml
@@ -95,7 +95,6 @@ module MemDebug = MemDebug
module MemEmpty = MemEmpty
module MemLoader = MemLoader
module MemMemory = MemMemory
-module MemRegion = MemRegion
module MemTyped = MemTyped
module MemVal = MemVal
module MemVar = MemVar
@@ -123,12 +122,7 @@ module AssignsCompleteness = AssignsCompleteness
(** {2 Region Analysis} *)
-module Region = Region
module Layout = Layout
-module RegionAccess = RegionAccess
-module RegionAnalysis = RegionAnalysis
-module RegionAnnot = RegionAnnot
-module RegionDump = RegionDump
(** {2 Compilers} *)
diff --git a/src/plugins/wp/wp_parameters.ml b/src/plugins/wp/wp_parameters.ml
index a0334d13b33e70c17d25d9fb35223a6788ed728d..9268c9e87a80e682a9c5a7c346a9a1c04da61d68 100644
--- a/src/plugins/wp/wp_parameters.ml
+++ b/src/plugins/wp/wp_parameters.ml
@@ -284,95 +284,6 @@ module Volatile =
Use -wp-no-volatile to ignore volatile attributes."
end)
-(* -------------------------------------------------------------------------- *)
-(* --- Region Model --- *)
-(* -------------------------------------------------------------------------- *)
-
-let wp_region = add_group "Region Analysis"
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region =
- False
- (struct
- let option_name = "-wp-region"
- let help = "Perform Region Analysis (experimental)"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_fixpoint =
- True
- (struct
- let option_name = "-wp-region-fixpoint"
- let help = "Compute region aliasing fixpoint"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_cluster =
- True
- (struct
- let option_name = "-wp-region-cluster"
- let help = "Compute region clustering fixpoint"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_inline =
- True
- (struct
- let option_name = "-wp-region-inline"
- let help = "Inline aliased sub-clusters"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_rw =
- True
- (struct
- let option_name = "-wp-region-rw"
- let help = "Written region are considered read-write by default"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_pack =
- True
- (struct
- let option_name = "-wp-region-pack"
- let help = "Pack clusters by default"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.do_not_save ()
-module Region_flat =
- False
- (struct
- let option_name = "-wp-region-flat"
- let help = "Flatten arrays by default"
- end)
-
-let () = Parameter_customize.set_group wp_region
-module Region_annot =
- False
- (struct
- let option_name = "-region-annot"
- let help = "Register '@region' ACSL Annotations (auto with -wp-region)"
- end)
-
-let () = Parameter_customize.set_group wp_region
-let () = Parameter_customize.is_invisible ()
-module Region_output_dot =
- Filepath
- (struct
- let option_name = "-wp-region-output-dot"
- let arg_name = "output.dot"
- let file_kind = "DOT"
- let existence = Fc_Filepath.Indifferent
- let help = "Outputs the region graph in DOT format to the specified file."
- end)
-
(* ------------------------------------------------------------------------ *)
(* --- WP Strategy --- *)
(* ------------------------------------------------------------------------ *)
diff --git a/src/plugins/wp/wp_parameters.mli b/src/plugins/wp/wp_parameters.mli
index 5c5159c59b555de8425115b69d7971a89c18ec07..84a25a418c36a8b3ca43d84f4b195aeb76505873 100644
--- a/src/plugins/wp/wp_parameters.mli
+++ b/src/plugins/wp/wp_parameters.mli
@@ -64,16 +64,6 @@ module Literals : Parameter_sig.Bool
module Volatile : Parameter_sig.Bool
module WeakIntModel : Parameter_sig.Bool
-module Region: Parameter_sig.Bool
-module Region_rw: Parameter_sig.Bool
-module Region_pack: Parameter_sig.Bool
-module Region_flat: Parameter_sig.Bool
-module Region_annot: Parameter_sig.Bool
-module Region_inline: Parameter_sig.Bool
-module Region_fixpoint: Parameter_sig.Bool
-module Region_cluster: Parameter_sig.Bool
-module Region_output_dot : Parameter_sig.Filepath
-
(** {2 Computation Strategies} *)
module Init: Parameter_sig.Bool