bench/infer/pbinfer2.mlw

   1
   2 module Test2
   3
   4 use int.Int
   5 use bool.Bool
   6 use ref.Ref
   7
   8 let to_true (ii : bool) (arg : bool) : bool
   9     writes { }
  10     ensures { if ii then result = true else result = arg}
  11     = if ii then true else arg
  12
  13 val x0 : ref bool
  14 val x1 : ref bool
  15 val x2 : ref bool
  16 val x3 : ref bool
  17
  18 let pgmtest [@infer] [@bddinfer] () : unit = [@vc:divergent]
  19     let a = ref false in
  20     let b = ref false in
  21     let c = ref false in
  22     let d = ref false in
  23     let e = ref false in
  24         while (!x3 && not !x1 && not !x2) do
  25
  26               label Init in
  27               (* ****** *)
  28               let tmp1 = (!x0 || !a) && not !e in
  29               let a1 = tmp1 in
  30               let tmp2 = tmp1 && !x1 && !x3 in
  31               let d1 = tmp2 in
  32               let b1 = to_true tmp1 !b in
  33               let tmp3 = tmp1 && !b && !x2 in
  34               let c1 = to_true tmp3 !c in
  35               (* ****** *)
  36               a := a1 ;
  37               b := b1 ;
  38               c := c1 ;
  39               d := d1 ;
  40               (* ****** *)
  41               [@bddinfer:Assert] assert {  !x0 \/ (!a at Init) -> !a } ;
  42
  43         done ;
  44
  45 end