int_overflow.mlw 1.34 KB
Newer Older
1 2
theory ModelInt

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 17

(* CE *)
goal test_overflow:
18
  forall x y :  int.
19 20 21 22
     0 <= x <= 65535 /\ 0 <= y <= 65535 -> 0 <= x + y <= 65535

(* CE *)
goal test_overflow2:
23
  forall x y :  int.
24 25 26 27 28 29
     -2 <= x <= 65535 /\ -2 <= y <= 65535 -> -2 <= x + y <= 65535

predicate is_int16 (x:int) = -65536 <= x <= 65535

(* CE *)
goal test_overflow_int16:
30
  forall x y :  int.
31 32 33 34
     is_int16 x /\ is_int16 y -> is_int16 (x + y)

(* CE *)
goal test_overflow_int16_alt:
35
  forall x y :  int.
36 37 38 39
      -65536 <= x <= 65535 /\ -65536 <= y <= 65535 -> -65536 <= x+y <= 65535

(* CE *)
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 45 46 47

predicate is_int32 (x:int) = -2147483648 <= x <= 2147483647

(* CE *)
goal test_overflow_int32:
48
  forall x y :  int.
49 50 51 52
     is_int32 x /\ is_int32 y -> is_int32 (x + y)

(* CE *)
goal test_overflow_int32_bis:
53
  forall x y :  int.
54 55 56 57
     is_int32 x /\ is_int32 y /\ 0 <= x <= y -> is_int32 (x + y)

(* CE *)
goal test_overflow_int32_bis_inline:
58
  forall x y :  int.
59 60 61
     -2147483648 <= x <= 2147483647 /\ -2147483648 <= y <= 2147483647 /\ 0 <= x <= y -> -2147483648 <= x + y <= 2147483647

end