bench/check-ce/result.mlw

   1
   2 module M
   3
   4   use int.Int
   5   use ref.Ref
   6
   7   val a : ref int
   8
   9   let p1 (b : ref int) : int
  10     requires { 0 <= !a <= 10 /\ 3 <= !b <= 17 }
  11     ensures  { 17 <= !a + result <= 42 }
  12   = a := !a + !b;
  13     !a + 1
  14
  15
  16 let f (a [@model] [@model_trace:A]: ref int)
  17   requires { !a = 42 }
  18   ensures { !a = 2 + old !a + result } =
  19   a := 0;
  20   a := 1;
  21   !a+1
  22
  23 end