bench/check-ce/records_label.mlw

   1
   2
   3 module Old
   4
   5   use int.Int
   6
   7   type r = {mutable f : int; mutable g : bool}
   8
   9   val y : r
  10
  11   let record_old_test1 (x : r) : unit
  12     ensures { old (x.f + y.f) = x.f }
  13   =
  14     x.f <- 6
  15
  16   let record_at_test2 (x : r) : unit
  17   =
  18     label L in
  19     x.f <- 6;
  20     label M in
  21     x.f <- 12;
  22     assert { x.f at L = ((x.f + x.f + 1) at M + x.f + y.f)}
  23
  24   let several_hats (x : r): unit
  25   =
  26     label L in
  27     label M in
  28     x.f <- 6;
  29     (* Here, the counterexample variable should mention both M and L *)
  30     assert { x.f at L  = x.f at M + 1}
  31
  32 end