Commit 85c0b2e5 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[wp] simplify pointer type

parent 89681265
......@@ -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)
......
......@@ -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 *)
......
......@@ -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 ;
......
......@@ -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 ;
......
......@@ -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 ;
......
......@@ -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 } ->
......
......@@ -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 ;
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment