[wp] Moves the notion of update init from model to MemLoader

src/plugins/wp/MemLoader.ml

@@ -455,7 +455,8 @@ struct
   (* -------------------------------------------------------------------------- *)
 
   let updated_init_atom seq loc value =
-    let chunk_init,mem_init = M.set_init_atom seq.pre loc value in
+    let new_value = e_or [M.is_init_atom seq.pre loc ; value ] in
+    let chunk_init,mem_init = M.set_init_atom seq.pre loc new_value in
     Set(Sigma.value seq.post chunk_init,mem_init)
 
   let updated_atom seq obj loc value =

src/plugins/wp/MemTyped.ml

@@ -993,11 +993,7 @@ struct
   let store_float sigma f l v = updated sigma (m_float f) l v
   let store_pointer sigma _ty l v = updated sigma M_pointer l v
 
-  let set_init_atom sigma l v = (* updated sigma T_init l v *)
-    let value = Sigma.value sigma T_init in
-    let current = F.e_get value l in
-    T_init, F.e_set value l (F.e_if current e_true v)
-
+  let set_init_atom sigma l v = updated sigma T_init l v
   let is_init_atom sigma l = F.e_get (Sigma.value sigma T_init) l
 
 end