diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index d1a6abbfdbe41121f655f3a322e9c10f384e0d60..795aec9adeab33b0bbfbbc0c589149d4ccecb7b3 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -198,13 +198,9 @@ type sigma = Sigma.t
type domain = Sigma.domain
type segment = loc rloc
-let comp_cluster () =
- Definitions.cluster ~id:"Compound" ~title:"Memory Compound Loader" ()
-
let shift_cluster () =
Definitions.cluster ~id:"Shifts" ~title:"Shifts Definitions" ()
-
(* ********************************************************************** *)
(* SIZE *)
(* ********************************************************************** *)
@@ -677,9 +673,6 @@ module Model = struct
Why3.havoc fresh current loc n
else fresh
- let eqmem obj loc _chunk m1 m2 =
- Why3.eqmem m1 m2 loc @@ sizeof obj
-
let eqmem_forall obj loc _chunk m1 m2 =
let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
let p = e_var xp in
diff --git a/src/plugins/wp/MemBytes.mli b/src/plugins/wp/MemBytes.mli
new file mode 100644
index 0000000000000000000000000000000000000000..ddb5ce41037e817691479951fd8e66cb96de2a34
--- /dev/null
+++ b/src/plugins/wp/MemBytes.mli
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(* *)
+(* 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). *)
+(* *)
+(**************************************************************************)
+
+include MemRegion.ModelWithLoader
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index bf90ba1869515790d5b56fa5271ddd8180dc6481..a4a7a81650ba5429c9e47099f1a191c696a4568b 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -33,7 +33,7 @@ open MemMemory
module L = Qed.Logic
-module type ModelLoader = sig
+module type ModelWithLoader = sig
include Sigs.Model
val sizeof : c_object -> term
@@ -62,42 +62,16 @@ module type ModelLoader = sig
val init_footprint : c_object -> loc -> Sigma.domain
end
-module Make (R:RegionAnalysis.API) (M:ModelLoader) (* : Sigs.Model *) =
+module Make (R:RegionAnalysis.API) (M:ModelWithLoader) (* : Sigs.Model *) =
struct
type region = R.region
-
- (***************************************************************************)
- (* *)
- (* Extern API *)
- (* *)
- (***************************************************************************)
let datatype = "MemRegion.Make"
(* For projectification. Must be unique among models. *)
- let configure () =
- begin
- let rollback () =
- M.configure () () ;
- in
- rollback
- end
- (* Initializers to be run before using the model.
- Typically push {i Context} values and returns a function to rollback.
- *)
-
- let configure_ia ia = (* TODO *) M.configure_ia ia
- (* Given an automaton, return a vertex's binder.
- Currently used by the automata compiler to bind current vertex.
-
- *)
-
- let hypotheses p = M.hypotheses p
- (* Computes the memory model partitionning of the memory locations.
- This function typically adds new elements to the partition received
- in input (that can be empty).
- ============================> TODO <======================================
- *)
+ let configure = M.configure
+ let configure_ia = M.configure_ia
+ let hypotheses = M.hypotheses
module BChunk = struct
@@ -111,7 +85,6 @@ struct
let self = "MemRegion.Make.RegionChunk"
-
let hash = function
| CVal r -> 0x02 * R.hash r
| CInit r -> 0x100 * R.hash r
@@ -152,7 +125,6 @@ struct
| CGhost _ -> "GhostChunk"
| CVal _ -> "ValueChunk"
| CInit _ -> "InitChunk"
- (* Used when generating fresh variables for a chunk. *)
let is_framed _ = false
@@ -171,7 +143,6 @@ struct
| CRegion of BChunk.t
let self = "MemRegion.Make.Chunk"
- (* Chunk names, for pretty-printing. *)
let hash = function
| CModel c -> M.Chunk.hash c
@@ -200,25 +171,8 @@ struct
let is_framed = function
| CModel c -> M.Chunk.is_framed c
| CRegion _ -> false
- (* Whether the chunk is local to a function call.
- Means the chunk is separated from anyother call side-effects.
- If [true], entails that a function assigning everything can not modify
- the chunk. Only used for optimisation, it would be safe to always
- return [false]. *)
end
- (* Memory Chunks.
-
- The concrete memory is partionned into a vector of abstract data.
- Each component of the partition is called a {i memory chunk} and
- holds an abstract representation of some part of the memory.
-
- Remark: memory chunks are not required to be independant from each other,
- provided the memory model implementation is consistent with the chosen
- representation. Conversely, a given object might be represented by
- several memory chunks.
-
- *)
module Heap = Qed.Collection.Make(Chunk)
@@ -390,11 +344,6 @@ struct
end
- (* ************************************************************************ *)
- (* *** MemLoader instanciation from the implementation of MemTyped *** *)
- (* ************************************************************************ *)
-
-
(***************************************************************************)
(* module Region : MemLoader.Module **)
(***************************************************************************)
@@ -674,8 +623,6 @@ struct
in assert false
in Loc { repr ; region = r }
-
-
(* ---------------------------------------------------------------------- *)
(* --- Store --- *)
(* ---------------------------------------------------------------------- *)
@@ -1027,16 +974,6 @@ struct
let initialized = LOADER.initialized
let domain = LOADER.domain
-(*
- let sloc_oget = function
- | Sloc None -> Sloc M.null, None
- | Sloc (Some { Region.repr = repr }) -> Sloc repr
- | Sarray (None,a,b) ->
- | Srange (None,_,_,_)
- | Sdescr (_,None,_) ->
- |
-*)
-
let assigned seq ty sloc = match sloc with
| Sloc (Region.Null) | Sarray (Region.Null,_,_)
| Srange (Region.Null,_,_,_) | Sdescr (_,Region.Null,_) ->
@@ -1348,7 +1285,7 @@ struct
if R.separated region1 region2 then p_true
else M.separated rl1 rl2
- let chunk_is_well_formed sigma chunk = match chunk with
+ let is_well_formed_chunk sigma chunk = match chunk with
| Chunk.CModel _ | Chunk.CRegion (B.CInit _)
| Chunk.CRegion (B.CGhost _) -> p_true
| Chunk.CRegion (B.CVal region) -> match R.kind region with
@@ -1362,10 +1299,11 @@ struct
| R.Single (R.Int cint) ->
Cint.range cint @@ Sigma.value sigma chunk
-
let is_well_formed sigma =
- p_and (M.is_well_formed sigma.Tuple.model)
- @@ p_conj @@ Sigma.Chunk.Set.fold (fun c l -> chunk_is_well_formed sigma c :: l) (Sigma.domain sigma) []
-
+ p_conj @@
+ Sigma.Chunk.Set.fold
+ (fun c l -> is_well_formed_chunk sigma c :: l)
+ (Sigma.domain sigma)
+ [M.is_well_formed sigma.model]
end
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index 9581a8c56759cebef4747cd6990dc98821608976..79038b5d194a5dd08210a979d54c0b21069642d4 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -29,7 +29,8 @@ open Sigs
(* --- Region Memory Model --- *)
(* -------------------------------------------------------------------------- *)
-module type ModelLoader = sig
+module type ModelWithLoader =
+sig
include Sigs.Model
val sizeof : c_object -> term
@@ -45,18 +46,17 @@ module type ModelLoader = sig
val load_float : sigma -> c_float -> loc -> term
val load_pointer : sigma -> typ -> loc -> loc
- val store_int : sigma -> c_int -> loc -> term -> Chunk.t * term
- val store_float : sigma -> c_float -> loc -> term -> Chunk.t * term
- val store_pointer : sigma -> typ -> loc -> term -> Chunk.t * term
+ val store_int : sigma -> c_int -> loc -> term -> chunk * term
+ val store_float : sigma -> c_float -> loc -> term -> chunk * term
+ val store_pointer : sigma -> typ -> loc -> term -> chunk * term
val set_init_atom : sigma -> c_object -> loc -> term -> chunk * term
val set_init : c_object -> loc -> length:term -> chunk -> current:term -> term
val is_init_atom : sigma -> c_object -> loc -> term
val is_init_range : sigma -> c_object -> loc -> term -> pred
- val value_footprint : c_object -> loc -> Sigma.domain
- val init_footprint : c_object -> loc -> Sigma.domain
+ val value_footprint : c_object -> loc -> domain
+ val init_footprint : c_object -> loc -> domain
end
-
-module Make (_:RegionAnalysis.API) (_:ModelLoader) : Sigs.Model
+module Make : RegionAnalysis.API -> ModelWithLoader -> Sigs.Model