new module null.Null for nullable values

safely extracted to OCaml using obj.magic
parent 9899f840
......@@ -264,3 +264,13 @@ module io.StdIO
syntax val print_int "Why3__BigInt.print"
syntax val print_newline "Pervasives.print_newline"
end
module null.Null
syntax type t "%1"
syntax val create_null "(fun () -> Obj.magic (ref 0))"
syntax val eq_null "(==)"
syntax val create "(fun x -> x)"
syntax val get "(fun x -> x)"
end
(** {1 A possibly null, yet safe, value}
The OCaml driver does optimize this into the identity.
To permit the implementation of eq_null, null is implemented is a
heap-allocated value in OCaml, e.g., Obj.magic [|0|]
*)
module Null
type null = int
type t_model 'a = Null null | Value 'a
type t 'a model { v: t_model 'a }
predicate is_null (t: t 'a) =
match t.v with Null _ -> true | Value _ -> false end
val create_null () : t 'a
ensures { is_null result }
val eq_null (n x: t 'a) : bool
requires { is_null n }
ensures { result <-> x.v = n.v }
val create (x: 'a) : t 'a
ensures { result.v = Value x }
val get (t: t 'a) : 'a
requires { not (is_null t) }
ensures { t.v = Value result }
end
\ No newline at end of file
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