From 85c0b2e5ac8b6559d2a524b2ca7702a3422627b5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Thu, 15 Oct 2020 11:49:11 +0200
Subject: [PATCH] [wp] simplify pointer type
---
src/plugins/wp/Lang.ml | 4 ++--
src/plugins/wp/Lang.mli | 4 ++--
src/plugins/wp/MemEmpty.ml | 2 +-
src/plugins/wp/MemRegion.ml | 2 +-
src/plugins/wp/MemTyped.ml | 2 +-
src/plugins/wp/MemVar.ml | 1 +
src/plugins/wp/MemZeroAlias.ml | 2 +-
7 files changed, 9 insertions(+), 8 deletions(-)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2c3dbf50588..c4c9997e469 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -186,7 +186,7 @@ let t_int = Logic.Int
let t_bool = Logic.Bool
let t_real = Logic.Real
let t_prop = Logic.Prop
-let t_addr () = Context.get pointer Cil.voidType
+let t_addr () = Context.get pointer
let t_array a = Logic.Array(Logic.Int,a)
let t_farray a b = Logic.Array(a,b)
let t_datatype adt ts = Logic.Data(adt,ts)
@@ -194,8 +194,8 @@ let t_datatype adt ts = Logic.Data(adt,ts)
let rec tau_of_object = function
| C_int _ -> Logic.Int
| C_float f -> Context.get floats f
- | C_pointer t -> Context.get pointer t
| C_comp c -> tau_of_comp c
+ | C_pointer _ -> Context.get pointer
| C_array { arr_element = typ } -> t_array (tau_of_ctype typ)
and tau_of_ctype typ = tau_of_object (Ctypes.object_of typ)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index ac60a977881..d8a13b4ad92 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -177,12 +177,12 @@ val t_int : tau
val t_real : tau
val t_bool : tau
val t_prop : tau
-val t_addr : unit -> tau (** pointer on Void *)
+val t_addr : unit -> tau
val t_array : tau -> tau
val t_farray : tau -> tau -> tau
val t_datatype : adt -> tau list -> tau
-val pointer : (typ -> tau) Context.value (** type of pointers *)
+val pointer : tau Context.value (** type of pointers *)
val floats : (c_float -> tau) Context.value (** type of floats *)
val poly : string list Context.value (** polymorphism *)
val builtin_types: (string -> t_builtin) Context.value (* builtin types *)
diff --git a/src/plugins/wp/MemEmpty.ml b/src/plugins/wp/MemEmpty.ml
index 837d3f28f39..1edfc12dcab 100644
--- a/src/plugins/wp/MemEmpty.ml
+++ b/src/plugins/wp/MemEmpty.ml
@@ -32,7 +32,7 @@ module Logic = Qed.Logic
let datatype = "MemEmpty"
let configure () =
begin
- let orig_pointer = Context.push Lang.pointer (fun _typ -> Logic.Int) in
+ let orig_pointer = Context.push Lang.pointer Logic.Int in
let orig_null = Context.push Cvalues.null (p_equal e_zero) in
let rollback () =
Context.pop Lang.pointer orig_pointer ;
diff --git a/src/plugins/wp/MemRegion.ml b/src/plugins/wp/MemRegion.ml
index eabf76e1090..2f1cdc6a856 100644
--- a/src/plugins/wp/MemRegion.ml
+++ b/src/plugins/wp/MemRegion.ml
@@ -428,7 +428,7 @@ let datatype = "MemRegion"
let configure () =
begin
- let orig_pointer = Context.push Lang.pointer (fun _ -> t_index) in
+ let orig_pointer = Context.push Lang.pointer t_index in
let orig_null = Context.push Cvalues.null p_inull in
let rollback () =
Context.pop Lang.pointer orig_pointer ;
diff --git a/src/plugins/wp/MemTyped.ml b/src/plugins/wp/MemTyped.ml
index b885cd1e214..36c8e0facd5 100644
--- a/src/plugins/wp/MemTyped.ml
+++ b/src/plugins/wp/MemTyped.ml
@@ -45,7 +45,7 @@ let datatype = "MemTyped"
let hypotheses p = p
let configure () =
begin
- let orig_pointer = Context.push Lang.pointer (fun _ -> t_addr) in
+ let orig_pointer = Context.push Lang.pointer t_addr in
let orig_null = Context.push Cvalues.null (p_equal a_null) in
let rollback () =
Context.pop Lang.pointer orig_pointer ;
diff --git a/src/plugins/wp/MemVar.ml b/src/plugins/wp/MemVar.ml
index 4bd0f123fe2..6706a5a6f19 100644
--- a/src/plugins/wp/MemVar.ml
+++ b/src/plugins/wp/MemVar.ml
@@ -1056,6 +1056,7 @@ struct
initialized_loc sigma obj x ofs
in
Lang.F.p_conj (List.map mk_pred ci.cfields)
+
and initialized_range sigma obj x ofs low up =
match obj with
| C_array { arr_element=t } ->
diff --git a/src/plugins/wp/MemZeroAlias.ml b/src/plugins/wp/MemZeroAlias.ml
index 3e185883a6d..ebfae47bf09 100644
--- a/src/plugins/wp/MemZeroAlias.ml
+++ b/src/plugins/wp/MemZeroAlias.ml
@@ -36,7 +36,7 @@ let datatype = "MemZeroAlias"
let configure () =
begin
- let orig_pointer = Context.push Lang.pointer (fun _typ -> Logic.Int) in
+ let orig_pointer = Context.push Lang.pointer Logic.Int in
let orig_null = Context.push Cvalues.null (p_equal e_zero) in
let rollback () =
Context.pop Lang.pointer orig_pointer ;
--
GitLab