tests/extract_ghost.mlw

   1
   2
   3 module M
   4
   5   use int.Int
   6
   7   let f (x:int) (ghost y:int) : int
   8     ensures { x = y }
   9   = x
  10
  11   let g (z:int) = f z 0
  12
  13 end