bench/check-ce/int_overflow.mlw

   1 theory ModelInt
   2
   3 use int.Int
   4
   5 (* PASS *)
   6 goal test0 : forall x:int. not (0 < x < 1)
   7
   8 (* CE *)
   9 goal test1 : forall x:int. not (0 <= x <= 1)
  10
  11 use int.EuclideanDivision
  12
  13 (* CE *)
  14 goal test2 : forall x:int. div x x = 1
  15
  16 (* CE *)
  17 goal test_overflow:
  18   forall x y :  int.
  19      0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535
  20
  21 (* CE *)
  22 goal test_overflow2:
  23   forall x y :  int.
  24      -2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535
  25
  26 predicate is_int16 (x:int) = -65536 <= x <= 65535
  27
  28 (* CE *)
  29 goal test_overflow_int16:
  30   forall x y :  int.
  31      is_int16 x /\ is_int16 y -> is_int16 (x + y)
  32
  33 (* CE *)
  34 goal test_overflow_int16_alt:
  35   forall x y :  int.
  36       -65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535
  37
  38 (* CE *)
  39 goal test_overflow_int16_bis:
  40   forall x y :  int.
  41      is_int16 x /\ is_int16 y /\
  42      (0 <= x) /\ (x <= y) -> is_int16 (x + y)
  43
  44 predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647
  45
  46 (* CE *)
  47 goal test_overflow_int32:
  48   forall x y :  int.
  49      is_int32 x /\ is_int32 y -> is_int32 (x + y)
  50
  51 (* CE *)
  52 goal test_overflow_int32_bis:
  53   forall x y :  int.
  54      is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)
  55
  56 (* CE *)
  57 goal test_overflow_int32_bis_inline:
  58   forall x y :  int.
  59      -2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647
  60
  61 end