bench/check-ce/jlamp_projections.mlw

   1
   2 module Abstract
   3
   4 use int.Int
   5
   6 type byte
   7 function to_int byte : int
   8 meta "model_projection" function to_int
   9 predicate in_range (x : int) = -128 <= x <= 127
  10 axiom range_axiom : forall x:byte. in_range (to_int x)
  11
  12
  13 val of_int (x:int) : byte
  14   requires { in_range x }
  15   ensures { to_int result = x }
  16
  17 val add (x y : byte) : byte
  18   requires { [@expl:integer overflow] in_range (to_int x + to_int y) }
  19   ensures { to_int result = to_int x + to_int y }
  20
  21 end
  22
  23 module AbstractAlone
  24
  25 use int.Int
  26 use Abstract
  27
  28 let p3 (a : byte) : byte =
  29   add a (of_int 1)
  30
  31 end
  32
  33
  34
  35 module AbstractWithRef
  36
  37 use int.Int
  38 use ref.Ref
  39 use Abstract
  40
  41 let p3 (a : ref byte) =
  42   a := add !a (of_int 1)
  43
  44 end
  45
  46 module Record
  47
  48 use int.Int
  49 use Abstract
  50
  51 type r = {mutable f : byte; mutable g : bool}
  52
  53 let p4 (b : r) =
  54   if b.g then b.f <- add b.f (of_int 1)
  55
  56 end