bench/infer/precision3.mlw

   1
   2
   3 use int.Int
   4
   5 val cp (input : bool) (src : int) (ref tgt : int) : unit
   6 writes { tgt }
   7 ensures { (input = True /\ tgt = src) \/ ((input = False) /\ tgt = old tgt)}
   8
   9 val ref d : int
  10
  11 let e [@bddinfer] ()
  12   diverges
  13   requires { d = 0 }
  14   =
  15   while True
  16   do
  17    d <- d+1;
  18
  19    cp (1 < d) 0 d
  20    (* This gives [0;+oo[ as domain for d, we would like [0;1] *)
  21
  22   done