oldify.mlw 530 Bytes
Newer Older
1
module M
2

3
  logic q1 int int int
4

5
parameter r : ref int
6 7

parameter f1 : y:int ->
8
             {} unit writes r { q1 (!r) (old (!r)) y }
9

10
let g1 () = {} f1 !r { q1 (!r) (old (!r)) (old (!r)) }
11

12 13
  logic foo int : int
  logic q int int int
14

15
parameter f : t:ref int -> x:int -> 
16
             {} unit reads t writes t { q (!t) (old (!t)) x }
17

18
let g (t:ref int) =
19 20
  {}
  f t (foo !t)
21
  { q (!t) (old (!t)) (foo (old (!t))) }
22

23
end
24 25 26 27 28 29

(*
Local Variables: 
compile-command: "unset LANG; make -C ../../.. bench/programs/good/oldify"
End: 
*)