val test1: Prims.unit -> SteelT UInt32.t emp (fun _ -> emp)
val test1: Prims.unit -> SteelT UInt32.t emp (fun _ -> emp)
let test1 () : SteelT UInt32.t emp (fun _ -> emp)
= let r = malloc 0ul in
  let x = read r in
  free r;
  x
module Deref2

open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference
/
Steel.Reference.fsti.checked Steel.Effect.Atomic.fsti.checked Steel.Effect.fsti.checked prims.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Int32.fsti.checked
Deref2.fst
_: Prims.unit -> Steel.Effect.SteelT FStar.UInt32.t
Prims.unit FStar.UInt32.t Steel.Reference.free Steel.Reference.read Steel.Reference.ref Steel.Reference.malloc FStar.UInt32.__uint_to_t Steel.Effect.Common.emp Steel.Effect.Common.vprop
let test1 () : SteelT UInt32.t emp (fun _ -> emp) =
  
let r = malloc 0ul in
let x = read r in
free r;
x