[MemValue] Add MemValue in the commandline and gui

src/plugins/wp/Factory.ml

@@ -355,6 +355,7 @@ let update_config ~warning m s = function
   | "TYPED" -> { s with mheap = Typed MemTyped.Fits }
   | "CAST" -> { s with mheap = Typed MemTyped.Unsafe }
   | "NOCAST" -> { s with mheap = Typed MemTyped.NoCast }
+  | "VALUE" -> { s with mheap = Value }
   | "CAVEAT" -> { s with mvar = Caveat }
   | "RAW" -> { s with mvar = Raw }
   | "REF" -> { s with mvar = Ref }

src/plugins/wp/GuiPanel.ml

@@ -93,7 +93,7 @@ let run_and_prove
 (* ---  Model Panel                                                     --- *)
 (* ------------------------------------------------------------------------ *)
 
-type memory = TREE | HOARE | TYPED | REGION
+type memory = TREE | HOARE | TYPED | REGION | VALUE
 
 class model_selector (main : Design.main_window_extension_points) =
   let dialog = new Wpane.dialog
@@ -101,6 +101,7 @@ class model_selector (main : Design.main_window_extension_points) =
   let memory = new Widget.group HOARE in
   let r_hoare  = memory#add_radio ~label:"Hoare Memory Model" ~value:HOARE () in
   let r_typed  = memory#add_radio ~label:"Typed Memory Model" ~value:TYPED () in
+  let r_value  = memory#add_radio ~label:"Value Memory Model" ~value:VALUE () in
   let c_casts  = new Widget.checkbox ~label:"Unsafe casts" () in
   let c_byref  = new Widget.checkbox ~label:"Reference Arguments" () in
   let c_ctxt   = new Widget.checkbox ~label:"Context Arguments (Caveat)" () in
@@ -113,6 +114,7 @@ class model_selector (main : Design.main_window_extension_points) =
       begin
         dialog#add_row r_hoare#coerce ;
         dialog#add_row r_typed#coerce ;
+        dialog#add_row r_value#coerce ;
         dialog#add_row c_casts#coerce ;
         dialog#add_row c_byref#coerce ;
         dialog#add_row c_ctxt#coerce ;
@@ -140,7 +142,7 @@ class model_selector (main : Design.main_window_extension_points) =
          | Region -> memory#set REGION
          | Hoare -> memory#set HOARE
          | Typed m -> memory#set TYPED ; c_casts#set (m = MemTyped.Unsafe)
-         | Value -> ()) ;
+         | Value -> memory#set VALUE) ;
         c_byref#set (s.mvar = Ref) ;
         c_ctxt#set (s.mvar = Caveat) ;
         c_cint#set (s.cint = Cint.Machine) ;
@@ -154,6 +156,7 @@ class model_selector (main : Design.main_window_extension_points) =
         | HOARE -> Hoare
         | TYPED -> Typed
                      (if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
+        | VALUE -> Value
       in {
         mheap = m ;
         mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;

src/plugins/wp/MemValue.ml

@@ -111,7 +111,7 @@ module VState =
 struct
   module M = Cvalue.Model
   let current : M.t ref = ref M.bottom
-  let _update () =
+  let update () =
     try
       match WpContext.get_scope () with
       | Global -> assert false
@@ -260,7 +260,7 @@ struct
     | M_float -> L.Array (t_addr, L.Real)
     | M_base _ -> L.Array (L.Int, t_addr)
   let basename_of_chunk c = match c with
-    | M_int -> "Mint"
+    | M_int -> "Mint00"
     | M_char -> "Mchar"
     | M_float -> "Mfloat"
     | M_base b -> match b with
@@ -361,7 +361,10 @@ let imval c = Sigs.Mchunk (Pretty_utils.to_string Chunk.pretty c, KValue)
 
 let lookup_lv _c _e = assert false (* TODO *)
 
-let lookup s e = imval (Tmap.find e s)
+let lookup s e =
+  match Tmap.find e s with
+  | exception Not_found -> Mterm
+  | v -> imval v
 
 let apply f s =
   let m = ref Tmap.empty in
@@ -670,6 +673,7 @@ let scope : sigma sequence -> scope -> varinfo list -> pred list = fun seq scope
   | Enter ->
       alloc_pred seq xs ALLOC
   | Leave ->
+      VState.update ();
       alloc_pred seq xs FREE
 
 let global : sigma -> term (*addr*) -> pred = fun _sigma p ->