bench/infer/auto_ref0.mlw

   1
   2 module Test
   3         use array.Array
   4         use ref.Ref
   5         use int.Int
   6
   7         let b [@bddinfer] [@infer](_:unit): unit
   8         =
   9                 let k = ref 0 in
  10                 while (true) do
  11                 variant { 0 }
  12                 invariant { !k = 0 }
  13                 ()
  14                 done; ()
  15
  16         let b2 [@bddinfer] [@infer:oct](_:unit): unit
  17         =
  18                 let k = ref 0 in
  19                 while (true) do
  20                 variant { 0 }
  21                 invariant { !k = 0 }
  22                 ()
  23                 done; ()
  24
  25         let b3 [@bddinfer] [@infer:box](_:unit): unit
  26         =
  27                 let k = ref 0 in
  28                 while (true) do
  29                 variant { 0 }
  30                 invariant { !k = 0 }
  31                 ()
  32                 done; ()
  33
  34 end