bench/infer/support3.mlw

   1 module Example_scan
   2
   3
   4 use export ref.Ref
   5 use export bool.Bool
   6 use export int.Int
   7
   8
   9 val foo (input : bool) (tgt : ref int) : unit
  10 writes { tgt }
  11 (* This does not work *)
  12 ensures { andb input (old !tgt = 42) -> (!tgt = 0) }
  13 (* But this is OK
  14 ensures { (old !tgt = 42) -> (!tgt = 0) }
  15 and this also
  16 ensures { input && (old !tgt = 42) -> (!tgt = 0) }
  17 *)
  18
  19 (**********************************************************************************)
  20
  21 val d0 [@model] [@model_trace:D0] : ref int
  22
  23 let example_scan [@bddinfer] ()
  24   diverges
  25   =
  26   while True do
  27         foo true d0
  28   done
  29
  30 end