bench/infer/bool_cond.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 (0 < d) 0 d *)
  20     (* This gives [0;0] as domain for d *)
  21
  22    cp (1 < d) 0 d
  23     (* This gives [0;0[ as domain for d *)
  24
  25   done