diff --git a/src/plugins/wp/MemBytes.ml b/src/plugins/wp/MemBytes.ml
index 39bf08ddf99638abeb4bbe8e7bcb099eae66cf20..da54a47b5d7ac3621202044296020f96339bb34c 100644
--- a/src/plugins/wp/MemBytes.ml
+++ b/src/plugins/wp/MemBytes.ml
@@ -41,10 +41,17 @@ struct
| Some l :: _ -> l
| _ -> raise Not_found
let l_havoc = Qed.Engine.F_call "havoc"
- let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
+ let f_havoc =
+ Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
let havoc fresh current loc n =
Lang.F.e_fun f_havoc [fresh;current;loc;n]
+ let l_memcpy = Qed.Engine.F_call "memcpy"
+ let f_memcpy =
+ Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
+ let memcpy mdst msrc ldst lsrc n =
+ Lang.F.e_fun f_memcpy [mdst;msrc;ldst;lsrc;n]
+
let p_cinits = Lang.extern_fp ~coloring:true ~library "cinits"
let cinits m = p_call p_cinits [m]
let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst"
@@ -673,6 +680,12 @@ module Model = struct
Why3.havoc fresh current loc n
else fresh
+ let memcpy obj ~lsrc ~ldst ~length chunk ~msrc ~mdst =
+ if chunk <> Chunk.Alloc then
+ let n = e_mul (e_int @@ sizeof_object obj) length in
+ Why3.memcpy mdst msrc ldst lsrc n
+ else msrc
+
let eqmem_forall obj loc _chunk m1 m2 =
let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
let p = e_var xp in
@@ -1138,3 +1151,4 @@ let is_init_range = Model.is_init_range
let value_footprint = Model.value_footprint
let init_footprint = Model.init_footprint
let havoc = Model.havoc
+let memcpy = Model.memcpy
diff --git a/src/plugins/wp/MemLoader.ml b/src/plugins/wp/MemLoader.ml
index 55ed3be3ff08ee79d2f13eec8c10fba383b1bd48..b450512c3bf49b87a5c39a2c4aa715198a538f27 100644
--- a/src/plugins/wp/MemLoader.ml
+++ b/src/plugins/wp/MemLoader.ml
@@ -65,6 +65,8 @@ sig
val havoc : c_object -> loc -> length:term ->
Chunk.t -> fresh:term -> current:term -> term
+ val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
+ Chunk.t -> msrc:term -> mdst:term -> term
val eqmem_forall :
c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
@@ -576,11 +578,31 @@ struct
let load_init = INIT_LOADER.load
let () = INIT_LOAD_INFO.load_rec := load_init
+ (* -------------------------------------------------------------------------- *)
+ (* --- Memcpy --- *)
+ (* -------------------------------------------------------------------------- *)
+
+ (*let gen_memcpy_length get_domain s obj ~lsrc ~ldst length =
+ let ps = ref [] in
+ Domain.iter
+ (fun chunk ->
+ let pre = Sigma.value s.pre chunk in
+ let post = Sigma.value s.post chunk in
+ let tau = Chunk.tau_of_chunk chunk in
+ let basename = Chunk.basename_of_chunk chunk ^ "_undef" in
+ let mdst = F.e_var (Lang.freshvar ~basename tau) in
+ let havoc = M.memcpy obj ~ldst ~lsrc ~length chunk ~mdst ~msrc:pre in
+ ps := Set(post,havoc) :: !ps
+ ) (get_domain obj ldst) ; !ps
+ *)
(* -------------------------------------------------------------------------- *)
(* --- Havocs --- *)
(* -------------------------------------------------------------------------- *)
let gen_havoc_length get_domain s obj loc length =
+(*
+ gen_memcpy_length get_domain s obj ~ldst:loc ~lsrc:loc length
+*)
let ps = ref [] in
Domain.iter
(fun chunk ->
diff --git a/src/plugins/wp/MemLoader.mli b/src/plugins/wp/MemLoader.mli
index 4af63f304bf109469c031dc32e7e45936b08ff39..3d56fa90c97503e8b64bd28b7993961d5865de02 100644
--- a/src/plugins/wp/MemLoader.mli
+++ b/src/plugins/wp/MemLoader.mli
@@ -61,6 +61,8 @@ sig
val havoc : c_object -> loc -> length:term ->
Chunk.t -> fresh:term -> current:term -> term
+ val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
+ Chunk.t -> msrc:term -> mdst:term -> term
val eqmem_forall :
c_object -> loc -> Chunk.t -> term -> term -> var list * pred * pred
diff --git a/src/plugins/wp/MemMemory.ml b/src/plugins/wp/MemMemory.ml
index 3272f7f9dbdee6c37f63f20941b9d00df3269351..1882b4b4fe25e4eab020a1a0a8a449b054015553 100644
--- a/src/plugins/wp/MemMemory.ml
+++ b/src/plugins/wp/MemMemory.ml
@@ -36,10 +36,12 @@ let ty_fst_arg = function
| _ -> raise Not_found
let l_havoc = Qed.Engine.F_call "havoc"
+let l_memcpy = Qed.Engine.F_call "memcpy"
let l_set_init = Qed.Engine.F_call "set_init"
let p_eqmem = Lang.extern_fp ~library "eqmem"
let f_havoc = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_havoc "havoc"
+let f_memcpy = Lang.extern_f ~library ~typecheck:ty_fst_arg ~link:l_memcpy "memcpy"
let p_framed = Lang.extern_fp ~coloring:true ~library "framed" (* m-pointer -> prop *)
let p_sconst = Lang.extern_fp ~coloring:true ~library "sconst" (* int-memory -> prop *)
let f_set_init =
diff --git a/src/plugins/wp/MemMemory.mli b/src/plugins/wp/MemMemory.mli
index b3a51ba5741471d92e9f22c9ec85a0dce60ff1e4..3e5cb9ad732bcead4b17d951a67e027bd4783ca2 100644
--- a/src/plugins/wp/MemMemory.mli
+++ b/src/plugins/wp/MemMemory.mli
@@ -36,6 +36,7 @@ val t_init : tau (** initialization tables *)
val t_mem : tau -> tau (** t_addr indexed array *)
val f_havoc : lfun
+val f_memcpy : lfun
val f_set_init : lfun
val p_is_init_r : lfun
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index 9f19ab4a33b1115f8392506b381534179d5d803d..3d33335c0a76ca32c2ea0fc87147b3986ad1631f 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -83,6 +83,8 @@ module type ModelWithLoader = sig
val frames : c_object -> loc -> chunk -> frame list
val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
+ val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
+ chunk -> msrc:term -> mdst:term -> term
val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
@@ -369,6 +371,16 @@ struct
| Value _ | ValInit -> fresh
| Array _ | ArrInit -> e_fun f_havoc [fresh;current;to_addr l;length]
+ let memcpy ty ~lsrc ~ldst ~length chunk ~msrc ~mdst =
+ match chunk with
+ | M c ->
+ M.memcpy ty ~lsrc:(loc lsrc) ~ldst:(loc ldst) ~length c ~msrc ~mdst
+ | R c ->
+ match c.mu with
+ | Value _ | ValInit -> msrc
+ | Array _ | ArrInit ->
+ e_fun f_memcpy [mdst;msrc;to_addr ldst;to_addr lsrc;length]
+
let eqmem_forall ty l chunk m1 m2 =
match chunk with
| M c -> M.eqmem_forall ty (loc l) c m1 m2
diff --git a/src/plugins/wp/MemRegion.mli b/src/plugins/wp/MemRegion.mli
index dc3ce4a0e103ed40d6f0b948b4aa5640063938cf..e35fedf766bd58b0a0a1ed41a8591d7a8336560b 100644
--- a/src/plugins/wp/MemRegion.mli
+++ b/src/plugins/wp/MemRegion.mli
@@ -59,7 +59,10 @@ sig
val last : sigma -> c_object -> loc -> term
val frames : c_object -> loc -> chunk -> frame list
- val havoc : c_object -> loc -> length:term -> chunk -> fresh:term -> current:term -> term
+ val havoc : c_object -> loc -> length:term ->
+ chunk -> fresh:term -> current:term -> term
+ val memcpy : c_object -> lsrc:loc -> ldst:loc -> length:term ->
+ chunk -> msrc:term -> mdst:term -> term
val eqmem_forall : c_object -> loc -> chunk -> term -> term -> var list * pred * pred
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index 22fbe398905c310bffba7c979501d39b3e37d7e2..146cce9b681a6c97418c2f12008485db207ea521 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -1048,6 +1048,12 @@ struct
F.e_fun f_havoc [fresh;current;loc;n]
else fresh
+ let memcpy obj ~lsrc ~ldst ~length chunk ~msrc ~mdst =
+ if chunk <> T_alloc then
+ let n = F.e_mul (length_of_object obj) length in
+ F.e_fun f_memcpy [mdst;msrc;ldst;lsrc;n]
+ else msrc
+
let eqmem_forall obj loc _chunk m1 m2 =
let xp = Lang.freshvar ~basename:"p" MemAddr.t_addr in
let p = F.e_var xp in
diff --git a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
index a5ffa059552627285f167d1c8c9a6425c4edbdb1..f0baf1c96d4bdf638bfeacbae3e9c0ffd1adf0a3 100644
--- a/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
+++ b/src/plugins/wp/share/why3/frama_c_wp/memory.mlw
@@ -36,7 +36,16 @@ theory Memory
predicate eqmem (m1 m2 : map addr 'a) (p:addr) (a:int) =
forall q:addr [m1[p]|m2[q]]. included q 1 p a -> m1[q] = m2[q]
- function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a
+
+ (* copies the [s] bytes from [m1].[b1] into [m0].[m0] *)
+ function memcpy (m0 m1: map addr 'a) (b0 b1:addr) (s:int) : map addr 'a =
+ fun (p:addr) ->
+ if separated p 1 b0 s then m0 p else
+ let offset = b1.offset - b0.offset + p.offset in
+ m1 { b1 with offset = offset }
+
+ function havoc (m0 m1 : map addr 'a) (p:addr) (a:int) : map addr 'a =
+ memcpy m1 m0 p p a
lemma eqmem_included :
forall m1 m2 : map addr 'a.
@@ -51,7 +60,7 @@ theory Memory
forall a : int.
eqmem m1 m2 p a -> eqmem m2 m1 p a
- axiom havoc_access :
+ lemma havoc_access :
forall m0 m1 : map addr 'a.
forall q p : addr.
forall a : int.