From bec9ca8e1714d9ae2d2f4cd4ca4398012b32de4d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fran=C3=A7ois=20Bobot?= <francois.bobot@cea.fr>
Date: Thu, 24 Sep 2020 19:11:55 +0200
Subject: [PATCH] [MemValue] Add MemValue in the commandline and gui
---
src/plugins/wp/Factory.ml | 1 +
src/plugins/wp/GuiPanel.ml | 7 +++++--
src/plugins/wp/MemValue.ml | 10 +++++++---
3 files changed, 13 insertions(+), 5 deletions(-)
diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml
index 85a6754ed0c..1daa6200a0d 100644
--- a/src/plugins/wp/Factory.ml
+++ b/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 }
diff --git a/src/plugins/wp/GuiPanel.ml b/src/plugins/wp/GuiPanel.ml
index 42a18b86e5b..b0d649a3402 100644
--- a/src/plugins/wp/GuiPanel.ml
+++ b/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 ;
diff --git a/src/plugins/wp/MemValue.ml b/src/plugins/wp/MemValue.ml
index 4e7a77a0073..e597f0d1483 100644
--- a/src/plugins/wp/MemValue.ml
+++ b/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 ->
--
GitLab