bench/infer/precision1.mlw

   1
   2 use int.Int
   3
   4 val randomb () : bool
   5
   6 val id (input: bool) (src: int) (ref tgt: int) : unit
   7 writes { tgt }
   8 ensures { input = True -> tgt = src }
   9 ensures { input = False -> tgt = old tgt }
  10
  11 val ref d0 : int
  12 val ref d1 : int
  13
  14 let s [@bddinfer] ()
  15   diverges
  16   requires { d0 = 0 }
  17   requires { d1 = 0 }
  18   =
  19   while true do
  20     (* gives d1 \in ]-oo,+oo[ instead of the more precise [0] *)
  21      id (randomb()) d0 d1;
  22   done