val main: Prims.unit -> SteelT Int32.t emp (fun _ -> emp)
val main: Prims.unit -> SteelT Int32.t emp (fun _ -> emp)
let main () : SteelT Int32.t emp (fun _ -> emp) = return 0l
module Deref2

open Steel.Effect.Atomic
open Steel.Effect
open Steel.Reference

let test1 () : SteelT UInt32.t emp (fun _ -> emp)
= let r = malloc 0ul in
  let x = read r in
  free r;
  x
/
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.Int32.t
Prims.unit Steel.Effect.Atomic.return FStar.Int32.t FStar.Ghost.hide FStar.Set.set Steel.Memory.iname FStar.Set.empty FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__mult Steel.Effect.Common.vprop Steel.Effect.Common.req Steel.Effect.Common.rm FStar.Algebra.CommMonoid.Equiv.__proj__CM__item__unit Steel.Effect.Common.emp FStar.Int32.__int_to_t
let main () : SteelT Int32.t emp (fun _ -> emp) =
  
return 0l