Skip to main content

Browse the archive

Revision 8d027170ca962c648621a88e12184943395f234e authored by Jonathan Protzenko on 02 January 2020, 17:22:42 UTC, committed by Jonathan Protzenko on 02 January 2020, 17:22:42 UTC 
Fix path
1 parent 09e8af1
Raw File
Vale.Arch.Heap.fst 
module Vale.Arch.Heap
open FStar.Mul
open Vale.Interop
open Vale.Arch.HeapImpl
friend Vale.Arch.HeapImpl

let heap_impl = vale_heap_impl

let heap_get hi = hi.mh

let heap_upd hi mh' =
  mi_heap_upd hi mh'

let heap_of_interop ih = ValeHeap (down_mem ih) (Ghost.hide ih)
back to top