[wp] Keep only MemVal

src/plugins/wp/Factory.ml

@@ -24,7 +24,7 @@
 (* --- Model Factory                                                      --- *)
 (* -------------------------------------------------------------------------- *)
 
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva1 | Eva2
+type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
 type mvar = Raw | Var | Ref | Caveat
 
 type setup = {
@@ -68,8 +68,7 @@ let descr_mheap d = function
   | ZeroAlias -> main d "zeroalias"
   | Hoare -> main d "hoare"
   | Typed p -> main d "typed" ; descr_mtyped d p
-  | Eva1 -> main d "eva1"
-  | Eva2 -> main d "eva2"
+  | Eva -> main d "eva"
 
 let descr_mvar d = function
   | Var -> ()
@@ -257,7 +256,6 @@ module Comp_MemTyped = MakeCompiler(MemTyped)
 module Comp_Typed_Var = MakeCompiler(Model_Typed_Var)
 module Comp_Typed_Ref = MakeCompiler(Model_Typed_Ref)
 module Comp_Caveat = MakeCompiler(Model_Caveat)
-module Comp_MemValue = MakeCompiler(MemValue)
 module Comp_MemVal = MakeCompiler(MemVal)
 
 
@@ -271,8 +269,7 @@ let compiler mheap mvar : (module Sigs.Compiler) =
   | Typed _ , Raw     -> (module Comp_MemTyped)
   | Typed _ , Var     -> (module Comp_Typed_Var)
   | Typed _ , Ref     -> (module Comp_Typed_Ref)
-  | Eva1, _           -> (module Comp_MemVal)
-  | Eva2, _           -> (module Comp_MemValue)
+  | Eva, _            -> (module Comp_MemVal)
 
 (* -------------------------------------------------------------------------- *)
 (* --- Tuning                                                             --- *)
@@ -282,8 +279,7 @@ let configure_mheap = function
   | Hoare -> MemEmpty.configure ()
   | ZeroAlias -> MemZeroAlias.configure ()
   | Region -> MemRegion.configure ()
-  | Eva1 -> MemVal.configure ()
-  | Eva2 -> MemValue.configure ()
+  | Eva -> MemVal.configure ()
   | Typed p ->
       let rollback_memtyped = MemTyped.configure () in
       let orig_memtyped_pointer = Context.push MemTyped.pointer p in
@@ -368,9 +364,8 @@ 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 }
-  | "EVA1" -> { s with mheap = Eva1 }
+  | "EVA" -> { s with mheap = Eva }
   | "CAVEAT" -> { s with mvar = Caveat }
-  | "EVA2" -> { s with mheap = Eva2 }
   | "RAW" -> { s with mvar = Raw }
   | "REF" -> { s with mvar = Ref }
   | "VAR" -> { s with mvar = Var }

src/plugins/wp/Factory.mli

@@ -24,7 +24,7 @@
 (* --- Model Factory                                                      --- *)
 (* -------------------------------------------------------------------------- *)
 
-type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva1 | Eva2
+type mheap = Hoare | ZeroAlias | Region | Typed of MemTyped.pointer | Eva
 type mvar = Raw | Var | Ref | Caveat
 
 type setup = {

src/plugins/wp/GuiPanel.ml

@@ -128,7 +128,7 @@ let run_and_prove
 (* ---  Model Panel                                                     --- *)
 (* ------------------------------------------------------------------------ *)
 
-type memory = TREE | HOARE | TYPED | REGION | EVA1 | EVA2
+type memory = TREE | HOARE | TYPED | REGION | EVA
 
 class model_selector (main : Design.main_window_extension_points) =
   let dialog = new Wpane.dialog
@@ -136,8 +136,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_eva1  = memory#add_radio ~label:"Eva Memory Model 1" ~value:EVA1 () in
-  let r_eva2  = memory#add_radio ~label:"Eva Memory Model 2" ~value:EVA2 () in
+  let r_eva    = memory#add_radio ~label:"Eva Memory Model" ~value:EVA () 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
@@ -150,8 +149,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_eva1#coerce ;
-        dialog#add_row r_eva2#coerce ;
+        dialog#add_row r_eva#coerce ;
         dialog#add_row c_casts#coerce ;
         dialog#add_row c_byref#coerce ;
         dialog#add_row c_ctxt#coerce ;
@@ -179,8 +177,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)
-         | Eva1 -> memory#set EVA1
-         | Eva2 -> memory#set EVA2
+         | Eva -> memory#set EVA
         ) ;
         c_byref#set (s.mvar = Ref) ;
         c_ctxt#set (s.mvar = Caveat) ;
@@ -195,8 +192,7 @@ class model_selector (main : Design.main_window_extension_points) =
         | HOARE -> Hoare
         | TYPED -> Typed
                      (if c_casts#get then MemTyped.Unsafe else MemTyped.Fits)
-        | EVA1 -> Eva1
-        | EVA2 -> Eva2
+        | EVA -> Eva
       in {
         mheap = m ;
         mvar = if c_ctxt#get then Caveat else if c_byref#get then Ref else Var ;

src/plugins/wp/Makefile.in

@@ -81,7 +81,7 @@ PLUGIN_CMO:= \
 	LogicSemantics LogicAssigns  \
 	Sigma MemLoader MemDebug \
 	MemEmpty MemZeroAlias MemVar \
-	MemMemory MemTyped MemRegion MemValue MemVal \
+	MemMemory MemTyped MemRegion MemVal \
 	wpReached wpRTE wpAnnot wpTarget \
 	CfgCompiler StmtSemantics \
 	VCS script proof wpo wpReport \
@@ -246,7 +246,7 @@ WP_API_BASE= \
 	Plang.mli Pcfg.mli Pcond.mli \
 	CodeSemantics.mli \
 	LogicCompiler.mli LogicSemantics.mli \
-	Sigma.mli MemVar.mli MemTyped.mli MemVal.mli MemValue.mli \
+	Sigma.mli MemVar.mli MemTyped.mli MemVal.mli \
 	CfgCompiler.mli StmtSemantics.mli \
 	Factory.mli driver.mli VCS.mli Tactical.mli Strategy.mli Auto.mli \
 	VC.mli wpo.mli ProverTask.mli prover.mli

src/plugins/wp/MemValue.mli

-(* module Make(M : Memory.Model) : Memory.Model *)
-
-include Sigs.Model

src/plugins/wp/wp_parameters.ml

@@ -205,7 +205,8 @@ module Model =
                   * '+raw' no logic variable\n\
                   * '+ref' by-reference-style pointers detection\n\
                   * '+nat/+int' natural / machine-integers arithmetics\n\
-                  * '+real/+float' real / IEEE floating point arithmetics"
+                  * '+real/+float' real / IEEE floating point arithmetics\n\
+                  * 'Eva' (experimental) based on the results from Eva plugin"
     end)
 
 let () = Parameter_customize.set_group wp_model