oldify.mlw 532 Bytes
Newer Older
1 2 3 4 5 6 7 8

{
  logic q1(int, int, int)
}

parameter r : int ref

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 16 17 18

{
  logic foo(int) : int
  logic q(int, int, int)
}

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

let g (t:int ref) =
  {}
  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: 
*)