diff options
Diffstat (limited to 'src/Compilers/Z/HexNotationConstants.v')
| -rw-r--r-- | src/Compilers/Z/HexNotationConstants.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/src/Compilers/Z/HexNotationConstants.v b/src/Compilers/Z/HexNotationConstants.v index e0670fa26..27a235d35 100644 --- a/src/Compilers/Z/HexNotationConstants.v +++ b/src/Compilers/Z/HexNotationConstants.v @@ -69,7 +69,9 @@ nums = tuple(sorted(set(systematic_nums + [ 8388599, 8388605, 8388606, + 11599871, 16711679, + 16775935, 16776959, 16777189, 16777191, @@ -115,6 +117,7 @@ nums = tuple(sorted(set(systematic_nums + [ 1073741822, 1332920885, 1749801491, + 2147483631, 2147483647, 2863311531, 2969567231, @@ -1297,10 +1300,18 @@ Notation "'0x800001'" (* 8388609 (0x800001) *) := (Const 8388609%Z). Notation "'0x800001'" (* 8388609 (0x800001) *) := (Const WO~0~0~0~0~0~0~0~0~1~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~0~1). +Notation "'0xb0ffff'" (* 11599871 (0xb0ffff) *) + := (Const 11599871%Z). +Notation "'0xb0ffff'" (* 11599871 (0xb0ffff) *) + := (Const WO~0~0~0~0~0~0~0~0~1~0~1~1~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). Notation "'0xfeffff'" (* 16711679 (0xfeffff) *) := (Const 16711679%Z). Notation "'0xfeffff'" (* 16711679 (0xfeffff) *) := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1). +Notation "'0xfffaff'" (* 16775935 (0xfffaff) *) + := (Const 16775935%Z). +Notation "'0xfffaff'" (* 16775935 (0xfffaff) *) + := (Const WO~0~0~0~0~0~0~0~0~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~0~1~1~1~1~1~1~1~1). Notation "'0xfffeff'" (* 16776959 (0xfffeff) *) := (Const 16776959%Z). Notation "'0xfffeff'" (* 16776959 (0xfffeff) *) @@ -1565,6 +1576,10 @@ Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *) := (Const 1749801491%Z). Notation "'0x684bda13'" (* 1749801491 (0x684bda13) *) := (Const WO~0~1~1~0~1~0~0~0~0~1~0~0~1~0~1~1~1~1~0~1~1~0~1~0~0~0~0~1~0~0~1~1). +Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *) + := (Const 2147483631%Z). +Notation "'0x7fffffef'" (* 2147483631 (0x7fffffef) *) + := (Const WO~0~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~1~0~1~1~1~1). Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *) := (Const 2147483647%Z). Notation "'0x7fffffff'" (* 2147483647 (0x7fffffff) *) |