oldify.mlw 525 Bytes
Newer Older
1 2

{
3
  logic q1 int int int
4 5
}

6
parameter r : ref int
7 8

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

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

{
14 15
  logic foo int : int
  logic q int int int
16 17
}

18
parameter f : t:ref int -> x:int -> 
19
             {} unit reads t writes t { q (!t) (old (!t)) x }
20

21
let g (t:ref int) =
22 23
  {}
  f t (foo !t)
24
  { q (!t) (old (!t)) (foo (old (!t))) }
25 26 27 28 29 30 31


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