Fixes in PowerPC port

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2209 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

3 files changed, 282 insertions, 260 deletions

diff --git a/test/regression/Results/builtins-powerpc b/test/regression/Results/builtins-powerpc
new file mode 100644
index 0000000..b841dc2
--- /dev/null
+++ b/test/regression/Results/builtins-powerpc
@@ -0,0 +1,21 @@
+mulhw(12345678, deadbeef) = fda16776
+mulhwu(12345678, deadbeef) = fd5bdee
+cntlz(12345678) = 3
+bswap(12345678) = 78563412
+bswap16(1234) = 3412
+fmadd(3.141590, 2.718000, 1.414000) = 9.952842
+fmsub(3.141590, 2.718000, 1.414000) = 7.124842
+fabs(3.141590) = 3.141590
+fabs(-3.141590) = 3.141590
+fsqrt(3.141590) = 1.772453
+frsqrte(3.141590) = 0.564198
+fres(3.141590) = 0.318311
+fsel(3.141590, 2.718000, 1.414000) = 2.718000
+fsel(-3.141590, 2.718000, 1.414000) = 1.414000
+fcti(3.141590) = 3
+fcti(2.718000) = 3
+fcti(1.414000) = 1
+read_16_rev = 3412
+read_32_rev = efbeadde
+after write_16_rev: 9a78
+after write_32_rev: 78563412
diff --git a/test/regression/Results/int32 b/test/regression/Results/int32
index 9128297..e0fafc4 100644
--- a/test/regression/Results/int32
+++ b/test/regression/Results/int32
@@ -161,9 +161,9 @@ x >>u i = 67a27166
 x >>s i = 67a27166
 x cmpu y = gt
 x cmps y = gt
-utod x = 59800000
+utod x = 41d9e89c59800000
 dtou f = 2a72d
-stod x = 59800000
+stod x = 41d9e89c59800000
 dtos f = 2a72d
 
 x = 1
@@ -185,9 +185,9 @@ x >>u i = 1
 x >>s i = 1
 x cmpu y = gt
 x cmps y = gt
-utod x = 0
+utod x = 3ff0000000000000
 dtou f = 0
-stod x = 0
+stod x = 3ff0000000000000
 dtos f = 0
 
 x = 1
@@ -209,9 +209,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = eq
 x cmps y = eq
-utod x = 0
+utod x = 3ff0000000000000
 dtou f = 0
-stod x = 0
+stod x = 3ff0000000000000
 dtos f = 0
 
 x = 1
@@ -233,9 +233,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = gt
-utod x = 0
+utod x = 3ff0000000000000
 dtou f = 0
-stod x = 0
+stod x = 3ff0000000000000
 dtos f = 0
 
 x = 1
@@ -257,9 +257,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = lt
-utod x = 0
+utod x = 3ff0000000000000
 dtou f = 0
-stod x = 0
+stod x = 3ff0000000000000
 dtos f = 0
 
 x = 1
@@ -281,9 +281,9 @@ x >>u i = 1
 x >>s i = 1
 x cmpu y = lt
 x cmps y = gt
-utod x = 0
+utod x = 3ff0000000000000
 dtou f = 0
-stod x = 0
+stod x = 3ff0000000000000
 dtos f = 0
 
 x = 1
@@ -305,9 +305,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = gt
-utod x = 0
+utod x = 3ff0000000000000
 dtou f = 0
-stod x = 0
+stod x = 3ff0000000000000
 dtos f = 0
 
 x = 3fb9ebc
@@ -329,9 +329,9 @@ x >>u i = 1fdcf5e
 x >>s i = 1fdcf5e
 x cmpu y = gt
 x cmps y = gt
-utod x = e0000000
+utod x = 418fdcf5e0000000
 dtou f = 1a1a
-stod x = e0000000
+stod x = 418fdcf5e0000000
 dtos f = 1a1a
 
 x = ffffffff
@@ -353,9 +353,9 @@ x >>u i = ffffffff
 x >>s i = ffffffff
 x cmpu y = gt
 x cmps y = lt
-utod x = ffe00000
+utod x = 41efffffffe00000
 dtou f = 68db8
-stod x = 0
+stod x = bff0000000000000
 dtos f = 0
 
 x = ffffffff
@@ -377,9 +377,9 @@ x >>u i = 7fffffff
 x >>s i = ffffffff
 x cmpu y = gt
 x cmps y = lt
-utod x = ffe00000
+utod x = 41efffffffe00000
 dtou f = 68db8
-stod x = 0
+stod x = bff0000000000000
 dtos f = 0
 
 x = ffffffff
@@ -401,9 +401,9 @@ x >>u i = 1
 x >>s i = ffffffff
 x cmpu y = eq
 x cmps y = eq
-utod x = ffe00000
+utod x = 41efffffffe00000
 dtou f = 68db8
-stod x = 0
+stod x = bff0000000000000
 dtos f = 0
 
 x = ffffffff
@@ -425,9 +425,9 @@ x >>u i = 1
 x >>s i = ffffffff
 x cmpu y = gt
 x cmps y = lt
-utod x = ffe00000
+utod x = 41efffffffe00000
 dtou f = 68db8
-stod x = 0
+stod x = bff0000000000000
 dtos f = 0
 
 x = ffffffff
@@ -449,9 +449,9 @@ x >>u i = ffffffff
 x >>s i = ffffffff
 x cmpu y = gt
 x cmps y = gt
-utod x = ffe00000
+utod x = 41efffffffe00000
 dtou f = 68db8
-stod x = 0
+stod x = bff0000000000000
 dtos f = 0
 
 x = ffffffff
@@ -473,9 +473,9 @@ x >>u i = 7fffffff
 x >>s i = ffffffff
 x cmpu y = gt
 x cmps y = gt
-utod x = ffe00000
+utod x = 41efffffffe00000
 dtou f = 68db8
-stod x = 0
+stod x = bff0000000000000
 dtos f = 0
 
 x = 26b98582
@@ -497,9 +497,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = gt
-utod x = c1000000
+utod x = 41c35cc2c1000000
 dtou f = fdc9
-stod x = c1000000
+stod x = 41c35cc2c1000000
 dtos f = fdc9
 
 x = 7fffffff
@@ -521,9 +521,9 @@ x >>u i = 7fffffff
 x >>s i = 7fffffff
 x cmpu y = gt
 x cmps y = gt
-utod x = ffc00000
+utod x = 41dfffffffc00000
 dtou f = 346dc
-stod x = ffc00000
+stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 7fffffff
@@ -545,9 +545,9 @@ x >>u i = 3fffffff
 x >>s i = 3fffffff
 x cmpu y = gt
 x cmps y = gt
-utod x = ffc00000
+utod x = 41dfffffffc00000
 dtou f = 346dc
-stod x = ffc00000
+stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 7fffffff
@@ -569,9 +569,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = gt
-utod x = ffc00000
+utod x = 41dfffffffc00000
 dtou f = 346dc
-stod x = ffc00000
+stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 7fffffff
@@ -593,9 +593,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = eq
 x cmps y = eq
-utod x = ffc00000
+utod x = 41dfffffffc00000
 dtou f = 346dc
-stod x = ffc00000
+stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 7fffffff
@@ -617,9 +617,9 @@ x >>u i = 7fffffff
 x >>s i = 7fffffff
 x cmpu y = lt
 x cmps y = gt
-utod x = ffc00000
+utod x = 41dfffffffc00000
 dtou f = 346dc
-stod x = ffc00000
+stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 7fffffff
@@ -641,9 +641,9 @@ x >>u i = ffff
 x >>s i = ffff
 x cmpu y = lt
 x cmps y = gt
-utod x = ffc00000
+utod x = 41dfffffffc00000
 dtou f = 346dc
-stod x = ffc00000
+stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 3b92bf38
@@ -665,9 +665,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = lt
-utod x = 9c000000
+utod x = 41cdc95f9c000000
 dtou f = 1866b
-stod x = 9c000000
+stod x = 41cdc95f9c000000
 dtos f = 1866b
 
 x = 80000000
@@ -689,9 +689,9 @@ x >>u i = 80000000
 x >>s i = 80000000
 x cmpu y = gt
 x cmps y = lt
-utod x = 0
+utod x = 41e0000000000000
 dtou f = 346dc
-stod x = 0
+stod x = c1e0000000000000
 dtos f = fffcb924
 
 x = 80000000
@@ -713,9 +713,9 @@ x >>u i = 40000000
 x >>s i = c0000000
 x cmpu y = gt
 x cmps y = lt
-utod x = 0
+utod x = 41e0000000000000
 dtou f = 346dc
-stod x = 0
+stod x = c1e0000000000000
 dtos f = fffcb924
 
 x = 80000000
@@ -737,9 +737,9 @@ x >>u i = 1
 x >>s i = ffffffff
 x cmpu y = lt
 x cmps y = lt
-utod x = 0
+utod x = 41e0000000000000
 dtou f = 346dc
-stod x = 0
+stod x = c1e0000000000000
 dtos f = fffcb924
 
 x = 80000000
@@ -761,9 +761,9 @@ x >>u i = 1
 x >>s i = ffffffff
 x cmpu y = gt
 x cmps y = lt
-utod x = 0
+utod x = 41e0000000000000
 dtou f = 346dc
-stod x = 0
+stod x = c1e0000000000000
 dtos f = fffcb924
 
 x = 80000000
@@ -785,9 +785,9 @@ x >>u i = 80000000
 x >>s i = 80000000
 x cmpu y = eq
 x cmps y = eq
-utod x = 0
+utod x = 41e0000000000000
 dtou f = 346dc
-stod x = 0
+stod x = c1e0000000000000
 dtos f = fffcb924
 
 x = 80000000
@@ -809,9 +809,9 @@ x >>u i = 40000
 x >>s i = fffc0000
 x cmpu y = lt
 x cmps y = lt
-utod x = 0
+utod x = 41e0000000000000
 dtou f = 346dc
-stod x = 0
+stod x = c1e0000000000000
 dtos f = fffcb924
 
 x = 7186e15e
@@ -833,9 +833,9 @@ x >>u i = 7186e15e
 x >>s i = 7186e15e
 x cmpu y = lt
 x cmps y = gt
-utod x = 57800000
+utod x = 41dc61b857800000
 dtou f = 2e802
-stod x = 57800000
+stod x = 41dc61b857800000
 dtos f = 2e802
 
 x = a3d2a09b
@@ -857,9 +857,9 @@ x >>u i = a3d
 x >>s i = fffffa3d
 x cmpu y = gt
 x cmps y = gt
-utod x = 13600000
+utod x = 41e47a5413600000
 dtou f = 431a0
-stod x = d9400000
+stod x = c1d70b57d9400000
 dtos f = fffda3e9
 
 x = e3ad9c39
@@ -881,9 +881,9 @@ x >>u i = 38
 x >>s i = fffffff8
 x cmpu y = gt
 x cmps y = gt
-utod x = 87200000
+utod x = 41ec75b387200000
 dtou f = 5d41c
-stod x = c7000000
+stod x = c1bc5263c7000000
 dtos f = ffff4664
 
 x = d40abc87
@@ -905,9 +905,9 @@ x >>u i = d40a
 x >>s i = ffffd40a
 x cmpu y = gt
 x cmps y = lt
-utod x = 90e00000
+utod x = 41ea815790e00000
 dtou f = 56da3
-stod x = bc800000
+stod x = c1c5faa1bc800000
 dtos f = fffedfeb
 
 x = e2a8dd05
@@ -929,9 +929,9 @@ x >>u i = 38a
 x >>s i = ffffff8a
 x cmpu y = lt
 x cmps y = lt
-utod x = a0a00000
+utod x = 41ec551ba0a00000
 dtou f = 5cd6f
-stod x = fb000000
+stod x = c1bd5722fb000000
 dtos f = ffff3fb8
 
 x = 10462533
@@ -953,9 +953,9 @@ x >>u i = 10462
 x >>s i = 10462
 x cmpu y = lt
 x cmps y = gt
-utod x = 33000000
+utod x = 41b0462533000000
 dtou f = 6aa7
-stod x = 33000000
+stod x = 41b0462533000000
 dtos f = 6aa7
 
 x = b58be891
@@ -977,9 +977,9 @@ x >>u i = 2d62
 x >>s i = ffffed62
 x cmpu y = gt
 x cmps y = lt
-utod x = 12200000
+utod x = 41e6b17d12200000
 dtou f = 4a5c8
-stod x = dbc00000
+stod x = c1d29d05dbc00000
 dtos f = fffe1810
 
 x = c615869f
@@ -1001,9 +1001,9 @@ x >>u i = c61586
 x >>s i = ffc61586
 x cmpu y = gt
 x cmps y = lt
-utod x = d3e00000
+utod x = 41e8c2b0d3e00000
 dtou f = 51229
-stod x = b0800000
+stod x = c1ccf53cb0800000
 dtos f = fffe8472
 
 x = b7ca4add
@@ -1025,9 +1025,9 @@ x >>u i = 2df29
 x >>s i = fffedf29
 x cmpu y = lt
 x cmps y = lt
-utod x = 5ba00000
+utod x = 41e6f9495ba00000
 dtou f = 4b47c
-stod x = 48c00000
+stod x = c1d20d6d48c00000
 dtos f = fffe26c5
 
 x = fd824ccb
@@ -1049,9 +1049,9 @@ x >>u i = fd824cc
 x >>s i = ffd824cc
 x cmpu y = gt
 x cmps y = gt
-utod x = 99600000
+utod x = 41efb04999600000
 dtou f = 67d65
-stod x = a8000000
+stod x = c183ed99a8000000
 dtos f = ffffefad
 
 x = aaae4fe9
@@ -1073,9 +1073,9 @@ x >>u i = 2aab93
 x >>s i = ffeaab93
 x cmpu y = lt
 x cmps y = lt
-utod x = fd200000
+utod x = 41e555c9fd200000
 dtou f = 45e93
-stod x = 5c00000
+stod x = c1d5546c05c00000
 dtos f = fffdd0db
 
 x = a7aa3b7
@@ -1097,9 +1097,9 @@ x >>u i = a7aa3b7
 x >>s i = a7aa3b7
 x cmpu y = lt
 x cmps y = lt
-utod x = 6e000000
+utod x = 41a4f5476e000000
 dtou f = 44ac
-stod x = 6e000000
+stod x = 41a4f5476e000000
 dtos f = 44ac
 
 x = e7a503b5
@@ -1121,9 +1121,9 @@ x >>u i = 39e940e
 x >>s i = ff9e940e
 x cmpu y = gt
 x cmps y = gt
-utod x = 76a00000
+utod x = 41ecf4a076a00000
 dtou f = 5ee1b
-stod x = 4b000000
+stod x = c1b85afc4b000000
 dtos f = ffff6063
 
 x = a2fd7763
@@ -1145,9 +1145,9 @@ x >>u i = a
 x >>s i = fffffffa
 x cmpu y = lt
 x cmps y = lt
-utod x = ec600000
+utod x = 41e45faeec600000
 dtou f = 42c2c
-stod x = 27400000
+stod x = c1d740a227400000
 dtos f = fffd9e74
 
 x = 354a3241
@@ -1169,9 +1169,9 @@ x >>u i = d528c90
 x >>s i = d528c90
 x cmpu y = lt
 x cmps y = gt
-utod x = 20800000
+utod x = 41caa51920800000
 dtou f = 15d3d
-stod x = 20800000
+stod x = 41caa51920800000
 dtos f = 15d3d
 
 x = 860673cf
@@ -1193,9 +1193,9 @@ x >>u i = 86
 x >>s i = ffffff86
 x cmpu y = gt
 x cmps y = lt
-utod x = 79e00000
+utod x = 41e0c0ce79e00000
 dtou f = 36e58
-stod x = c400000
+stod x = c1de7e630c400000
 dtos f = fffce0a1
 
 x = 4b34678d
@@ -1217,9 +1217,9 @@ x >>u i = 1
 x >>s i = 1
 x cmpu y = gt
 x cmps y = gt
-utod x = e3400000
+utod x = 41d2cd19e3400000
 dtou f = 1ecdc
-stod x = e3400000
+stod x = 41d2cd19e3400000
 dtos f = 1ecdc
 
 x = 9f3a04fb
@@ -1241,9 +1241,9 @@ x >>u i = 9f3
 x >>s i = fffff9f3
 x cmpu y = gt
 x cmps y = lt
-utod x = 9f600000
+utod x = 41e3e7409f600000
 dtou f = 41381
-stod x = c1400000
+stod x = c1d8317ec1400000
 dtos f = fffd85ca
 
 x = d080ef99
@@ -1265,9 +1265,9 @@ x >>u i = 34
 x >>s i = fffffff4
 x cmpu y = gt
 x cmps y = lt
-utod x = f3200000
+utod x = 41ea101df3200000
 dtou f = 55673
-stod x = 33800000
+stod x = c1c7bf8833800000
 dtos f = fffec8bb
 
 x = 535156e7
@@ -1289,9 +1289,9 @@ x >>u i = 5351
 x >>s i = 5351
 x cmpu y = gt
 x cmps y = gt
-utod x = b9c00000
+utod x = 41d4d455b9c00000
 dtou f = 22207
-stod x = b9c00000
+stod x = 41d4d455b9c00000
 dtos f = 22207
 
 x = 611fd665
@@ -1313,9 +1313,9 @@ x >>u i = 184
 x >>s i = 184
 x cmpu y = gt
 x cmps y = gt
-utod x = 99400000
+utod x = 41d847f599400000
 dtou f = 27c83
-stod x = 99400000
+stod x = 41d847f599400000
 dtos f = 27c83
 
 x = 61465593
@@ -1337,9 +1337,9 @@ x >>u i = 61465
 x >>s i = 61465
 x cmpu y = lt
 x cmps y = gt
-utod x = 64c00000
+utod x = 41d8519564c00000
 dtou f = 27d7f
-stod x = 64c00000
+stod x = 41d8519564c00000
 dtos f = 27d7f
 
 x = e5dfe7f1
@@ -1361,9 +1361,9 @@ x >>u i = 3977
 x >>s i = fffff977
 x cmpu y = gt
 x cmps y = lt
-utod x = fe200000
+utod x = 41ecbbfcfe200000
 dtou f = 5e281
-stod x = f000000
+stod x = c1ba20180f000000
 dtos f = ffff54c9
 
 x = 843facff
@@ -1385,9 +1385,9 @@ x >>u i = 843fac
 x >>s i = ff843fac
 x cmpu y = lt
 x cmps y = lt
-utod x = 9fe00000
+utod x = 41e087f59fe00000
 dtou f = 362b4
-stod x = c0400000
+stod x = c1def014c0400000
 dtos f = fffcd4fc
 
 x = 4b3ab03d
@@ -1409,9 +1409,9 @@ x >>u i = 12cea
 x >>s i = 12cea
 x cmpu y = lt
 x cmps y = gt
-utod x = f400000
+utod x = 41d2ceac0f400000
 dtou f = 1ed05
-stod x = f400000
+stod x = 41d2ceac0f400000
 dtos f = 1ed05
 
 x = c23cc92b
@@ -1433,9 +1433,9 @@ x >>u i = c23cc92
 x >>s i = fc23cc92
 x cmpu y = gt
 x cmps y = lt
-utod x = 25600000
+utod x = 41e8479925600000
 dtou f = 4f8f4
-stod x = 6a800000
+stod x = c1cee19b6a800000
 dtos f = fffe6b3c
 
 x = 62e07b49
@@ -1457,9 +1457,9 @@ x >>u i = 18b81e
 x >>s i = 18b81e
 x cmpu y = gt
 x cmps y = gt
-utod x = d2400000
+utod x = 41d8b81ed2400000
 dtou f = 287ff
-stod x = d2400000
+stod x = 41d8b81ed2400000
 dtos f = 287ff
 
 x = 1381d617
@@ -1481,9 +1481,9 @@ x >>u i = 1381d617
 x >>s i = 1381d617
 x cmpu y = gt
 x cmps y = gt
-utod x = 17000000
+utod x = 41b381d617000000
 dtou f = 7fd7
-stod x = 17000000
+stod x = 41b381d617000000
 dtos f = 7fd7
 
 x = 7c045515
@@ -1505,9 +1505,9 @@ x >>u i = 1f01154
 x >>s i = 1f01154
 x cmpu y = lt
 x cmps y = gt
-utod x = 45400000
+utod x = 41df011545400000
 dtou f = 32cc1
-stod x = 45400000
+stod x = 41df011545400000
 dtos f = 32cc1
 
 x = cec3bfc3
@@ -1529,9 +1529,9 @@ x >>u i = c
 x >>s i = fffffffc
 x cmpu y = gt
 x cmps y = lt
-utod x = f8600000
+utod x = 41e9d877f8600000
 dtou f = 54b0d
-stod x = 1e800000
+stod x = c1c89e201e800000
 dtos f = fffebd55
 
 x = fe6809a1
@@ -1553,9 +1553,9 @@ x >>u i = 3f9a0268
 x >>s i = ff9a0268
 x cmpu y = gt
 x cmps y = lt
-utod x = 34200000
+utod x = 41efcd0134200000
 dtou f = 68347
-stod x = f0000000
+stod x = c1797f65f0000000
 dtos f = fffff58f
 
 x = 614322f
@@ -1577,9 +1577,9 @@ x >>u i = 6
 x >>s i = 6
 x cmpu y = lt
 x cmps y = lt
-utod x = bc000000
+utod x = 419850c8bc000000
 dtou f = 27d6
-stod x = bc000000
+stod x = 419850c8bc000000
 dtos f = 27d6
 
 x = 142824ed
@@ -1601,9 +1601,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = lt
-utod x = ed000000
+utod x = 41b42824ed000000
 dtou f = 8419
-stod x = ed000000
+stod x = 41b42824ed000000
 dtos f = 8419
 
 x = c08d995b
@@ -1625,9 +1625,9 @@ x >>u i = c08
 x >>s i = fffffc08
 x cmpu y = lt
 x cmps y = lt
-utod x = 2b600000
+utod x = 41e811b32b600000
 dtou f = 4edea
-stod x = 52800000
+stod x = c1cfb93352800000
 dtos f = fffe6032
 
 x = 2e47f2f9
@@ -1649,9 +1649,9 @@ x >>u i = b
 x >>s i = b
 x cmpu y = lt
 x cmps y = gt
-utod x = 7c800000
+utod x = 41c723f97c800000
 dtou f = 12f4e
-stod x = 7c800000
+stod x = 41c723f97c800000
 dtos f = 12f4e
 
 x = bcbf2147
@@ -1673,9 +1673,9 @@ x >>u i = bcbf
 x >>s i = ffffbcbf
 x cmpu y = lt
 x cmps y = lt
-utod x = 28e00000
+utod x = 41e797e428e00000
 dtou f = 4d4f8
-stod x = ae400000
+stod x = c1d0d037ae400000
 dtos f = fffe4740
 
 x = effd7fc5
@@ -1697,9 +1697,9 @@ x >>u i = 3bf
 x >>s i = ffffffbf
 x cmpu y = gt
 x cmps y = gt
-utod x = f8a00000
+utod x = 41edffaff8a00000
 dtou f = 624cc
-stod x = 3b000000
+stod x = c1b002803b000000
 dtos f = ffff9715
 
 x = 27d8b5f3
@@ -1721,9 +1721,9 @@ x >>u i = 27d8b
 x >>s i = 27d8b
 x cmpu y = lt
 x cmps y = gt
-utod x = f9800000
+utod x = 41c3ec5af9800000
 dtou f = 10523
-stod x = f9800000
+stod x = 41c3ec5af9800000
 dtos f = 10523
 
 x = ccbd9751
@@ -1745,9 +1745,9 @@ x >>u i = 332f
 x >>s i = fffff32f
 x cmpu y = gt
 x cmps y = lt
-utod x = ea200000
+utod x = 41e997b2ea200000
 dtou f = 53dc9
-stod x = 57800000
+stod x = c1c9a13457800000
 dtos f = fffeb011
 
 x = 7597035f
@@ -1769,9 +1769,9 @@ x >>u i = 759703
 x >>s i = 759703
 x cmpu y = lt
 x cmps y = gt
-utod x = d7c00000
+utod x = 41dd65c0d7c00000
 dtou f = 302a3
-stod x = d7c00000
+stod x = 41dd65c0d7c00000
 dtos f = 302a3
 
 x = 6507c59d
@@ -1793,9 +1793,9 @@ x >>u i = 1941f
 x >>s i = 1941f
 x cmpu y = gt
 x cmps y = gt
-utod x = 67400000
+utod x = 41d941f167400000
 dtou f = 2961c
-stod x = 67400000
+stod x = 41d941f167400000
 dtos f = 2961c
 
 x = 44ef758b
@@ -1817,9 +1817,9 @@ x >>u i = 44ef758
 x >>s i = 44ef758
 x cmpu y = lt
 x cmps y = gt
-utod x = 62c00000
+utod x = 41d13bdd62c00000
 dtou f = 1c3c6
-stod x = 62c00000
+stod x = 41d13bdd62c00000
 dtos f = 1c3c6
 
 x = 6df256a9
@@ -1841,9 +1841,9 @@ x >>u i = 1b7c95
 x >>s i = 1b7c95
 x cmpu y = lt
 x cmps y = gt
-utod x = aa400000
+utod x = 41db7c95aa400000
 dtou f = 2d08b
-stod x = aa400000
+stod x = 41db7c95aa400000
 dtos f = 2d08b
 
 x = fd7c3877
@@ -1865,9 +1865,9 @@ x >>u i = fd7c3877
 x >>s i = fd7c3877
 x cmpu y = gt
 x cmps y = gt
-utod x = ee00000
+utod x = 41efaf870ee00000
 dtou f = 67d3d
-stod x = 48000000
+stod x = c1841e3c48000000
 dtos f = ffffef85
 
 x = af765675
@@ -1889,9 +1889,9 @@ x >>u i = 2bdd959
 x >>s i = febdd959
 x cmpu y = lt
 x cmps y = lt
-utod x = cea00000
+utod x = 41e5eecacea00000
 dtou f = 47de8
-stod x = 62c00000
+stod x = c1d4226a62c00000
 dtos f = fffdf031
 
 x = 91a83823
@@ -1913,9 +1913,9 @@ x >>u i = 9
 x >>s i = fffffff9
 x cmpu y = gt
 x cmps y = lt
-utod x = 4600000
+utod x = 41e2350704600000
 dtou f = 3ba94
-stod x = f7400000
+stod x = c1db95f1f7400000
 dtos f = fffd2cdc
 
 x = 657b9101
@@ -1937,9 +1937,9 @@ x >>u i = 195ee440
 x >>s i = 195ee440
 x cmpu y = gt
 x cmps y = gt
-utod x = 40400000
+utod x = 41d95ee440400000
 dtou f = 29913
-stod x = 40400000
+stod x = 41d95ee440400000
 dtos f = 29913
 
 x = 919b208f
@@ -1961,9 +1961,9 @@ x >>u i = 91
 x >>s i = ffffff91
 x cmpu y = lt
 x cmps y = lt
-utod x = 11e00000
+utod x = 41e2336411e00000
 dtou f = 3ba3e
-stod x = dc400000
+stod x = c1db9937dc400000
 dtos f = fffd2c86
 
 x = fa4924d
@@ -1985,9 +1985,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = lt
-utod x = 9a000000
+utod x = 41af49249a000000
 dtou f = 6684
-stod x = 9a000000
+stod x = 41af49249a000000
 dtos f = 6684
 
 x = 7ae55dbb
@@ -2009,9 +2009,9 @@ x >>u i = 7ae
 x >>s i = 7ae
 x cmpu y = gt
 x cmps y = gt
-utod x = 6ec00000
+utod x = 41deb9576ec00000
 dtou f = 32569
-stod x = 6ec00000
+stod x = 41deb9576ec00000
 dtos f = 32569
 
 x = 7bdaa659
@@ -2033,9 +2033,9 @@ x >>u i = 1e
 x >>s i = 1e
 x cmpu y = lt
 x cmps y = gt
-utod x = 96400000
+utod x = 41def6a996400000
 dtou f = 32bb0
-stod x = 96400000
+stod x = 41def6a996400000
 dtos f = 32bb0
 
 x = f0ec1ba7
@@ -2057,9 +2057,9 @@ x >>u i = f0ec
 x >>s i = fffff0ec
 x cmpu y = gt
 x cmps y = lt
-utod x = 74e00000
+utod x = 41ee1d8374e00000
 dtou f = 62ae8
-stod x = b2000000
+stod x = c1ae27c8b2000000
 dtos f = ffff9d30
 
 x = 9799d925
@@ -2081,9 +2081,9 @@ x >>u i = 25e
 x >>s i = fffffe5e
 x cmpu y = gt
 x cmps y = lt
-utod x = 24a00000
+utod x = 41e2f33b24a00000
 dtou f = 3e188
-stod x = b6c00000
+stod x = c1da1989b6c00000
 dtos f = fffd53d0
 
 x = 4a154653
@@ -2105,9 +2105,9 @@ x >>u i = 4a154
 x >>s i = 4a154
 x cmpu y = lt
 x cmps y = gt
-utod x = 94c00000
+utod x = 41d2855194c00000
 dtou f = 1e582
-stod x = 94c00000
+stod x = 41d2855194c00000
 dtos f = 1e582
 
 x = 53fcf6b1
@@ -2129,9 +2129,9 @@ x >>u i = 14ff
 x >>s i = 14ff
 x cmpu y = gt
 x cmps y = gt
-utod x = ac400000
+utod x = 41d4ff3dac400000
 dtou f = 2266c
-stod x = ac400000
+stod x = 41d4ff3dac400000
 dtos f = 2266c
 
 x = 9db389bf
@@ -2153,9 +2153,9 @@ x >>u i = 9db389
 x >>s i = ff9db389
 x cmpu y = lt
 x cmps y = lt
-utod x = 37e00000
+utod x = 41e3b67137e00000
 dtou f = 40982
-stod x = 90400000
+stod x = c1d8931d90400000
 dtos f = fffd7bcb
 
 x = a8898afd
@@ -2177,9 +2177,9 @@ x >>u i = 2a226
 x >>s i = fffea226
 x cmpu y = gt
 x cmps y = lt
-utod x = 5fa00000
+utod x = 41e511315fa00000
 dtou f = 45086
-stod x = 40c00000
+stod x = c1d5dd9d40c00000
 dtos f = fffdc2ce
 
 x = 3eb251eb
@@ -2201,9 +2201,9 @@ x >>u i = 3eb251e
 x >>s i = 3eb251e
 x cmpu y = lt
 x cmps y = gt
-utod x = f5800000
+utod x = 41cf5928f5800000
 dtou f = 19ae3
-stod x = f5800000
+stod x = 41cf5928f5800000
 dtos f = 19ae3
 
 x = 80bbe209
@@ -2225,9 +2225,9 @@ x >>u i = 202ef8
 x >>s i = ffe02ef8
 x cmpu y = lt
 x cmps y = lt
-utod x = 41200000
+utod x = 41e0177c41200000
 dtou f = 34bab
-stod x = 7dc00000
+stod x = c1dfd1077dc00000
 dtos f = fffcbdf3
 
 x = 4f01cad7
@@ -2249,9 +2249,9 @@ x >>u i = 4f01cad7
 x >>s i = 4f01cad7
 x cmpu y = gt
 x cmps y = gt
-utod x = b5c00000
+utod x = 41d3c072b5c00000
 dtou f = 205c7
-stod x = b5c00000
+stod x = 41d3c072b5c00000
 dtos f = 205c7
 
 x = 205307d5
@@ -2273,9 +2273,9 @@ x >>u i = 814c1f
 x >>s i = 814c1f
 x cmpu y = lt
 x cmps y = lt
-utod x = ea800000
+utod x = 41c02983ea800000
 dtou f = d3d7
-stod x = ea800000
+stod x = 41c02983ea800000
 dtos f = d3d7
 
 x = d7c2e083
@@ -2297,9 +2297,9 @@ x >>u i = d
 x >>s i = fffffffd
 x cmpu y = gt
 x cmps y = gt
-utod x = 10600000
+utod x = 41eaf85c10600000
 dtou f = 58603
-stod x = be800000
+stod x = c1c41e8fbe800000
 dtos f = fffef84b
 
 x = 4a5cc861
@@ -2321,9 +2321,9 @@ x >>u i = 12973218
 x >>s i = 12973218
 x cmpu y = gt
 x cmps y = gt
-utod x = 18400000
+utod x = 41d2973218400000
 dtou f = 1e757
-stod x = 18400000
+stod x = 41d2973218400000
 dtos f = 1e757
 
 x = 92333eef
@@ -2345,9 +2345,9 @@ x >>u i = 92
 x >>s i = ffffff92
 x cmpu y = lt
 x cmps y = lt
-utod x = dde00000
+utod x = 41e24667dde00000
 dtou f = 3be23
-stod x = 44400000
+stod x = c1db733044400000
 dtos f = fffd306b
 
 x = 3701afad
@@ -2369,9 +2369,9 @@ x >>u i = 0
 x >>s i = 0
 x cmpu y = lt
 x cmps y = gt
-utod x = d6800000
+utod x = 41cb80d7d6800000
 dtou f = 1687d
-stod x = d6800000
+stod x = 41cb80d7d6800000
 dtos f = 1687d
 
 x = 4d59521b
@@ -2393,9 +2393,9 @@ x >>u i = 4d5
 x >>s i = 4d5
 x cmpu y = lt
 x cmps y = gt
-utod x = 86c00000
+utod x = 41d3565486c00000
 dtou f = 1fae9
-stod x = 86c00000
+stod x = 41d3565486c00000
 dtos f = 1fae9
 
 x = 241109b9
@@ -2417,9 +2417,9 @@ x >>u i = 9
 x >>s i = 9
 x cmpu y = lt
 x cmps y = gt
-utod x = dc800000
+utod x = 41c20884dc800000
 dtou f = ec5d
-stod x = dc800000
+stod x = 41c20884dc800000
 dtos f = ec5d
 
 x = 9c704607
@@ -2441,9 +2441,9 @@ x >>u i = 9c70
 x >>s i = ffff9c70
 x cmpu y = gt
 x cmps y = lt
-utod x = c0e00000
+utod x = 41e38e08c0e00000
 dtou f = 4013c
-stod x = 7e400000
+stod x = c1d8e3ee7e400000
 dtos f = fffd7384
 
 x = c4ce285
@@ -2465,9 +2465,9 @@ x >>u i = 31
 x >>s i = 31
 x cmpu y = lt
 x cmps y = gt
-utod x = a000000
+utod x = 41a899c50a000000
 dtou f = 509c
-stod x = a000000
+stod x = 41a899c50a000000
 dtos f = 509c
 
 x = 3a1406b3
@@ -2489,9 +2489,9 @@ x >>u i = 3a140
 x >>s i = 3a140
 x cmpu y = lt
 x cmps y = gt
-utod x = 59800000
+utod x = 41cd0a0359800000
 dtou f = 17c9f
-stod x = 59800000
+stod x = 41cd0a0359800000
 dtos f = 17c9f
 
 x = d1760611
@@ -2513,9 +2513,9 @@ x >>u i = 345d
 x >>s i = fffff45d
 x cmpu y = gt
 x cmps y = gt
-utod x = c2200000
+utod x = 41ea2ec0c2200000
 dtou f = 55cb9
-stod x = f7800000
+stod x = c1c744fcf7800000
 dtos f = fffecf01
 
 x = 4c2d401f
@@ -2537,9 +2537,9 @@ x >>u i = 4c2d40
 x >>s i = 4c2d40
 x cmpu y = lt
 x cmps y = gt
-utod x = 7c00000
+utod x = 41d30b5007c00000
 dtou f = 1f33b
-stod x = 7c00000
+stod x = 41d30b5007c00000
 dtos f = 1f33b
 
 x = e518005d
@@ -2561,9 +2561,9 @@ x >>u i = 39460
 x >>s i = ffff9460
 x cmpu y = gt
 x cmps y = gt
-utod x = ba00000
+utod x = 41eca3000ba00000
 dtou f = 5dd63
-stod x = a3000000
+stod x = c1bae7ffa3000000
 dtos f = ffff4fab
 
 x = 749d5e4b
@@ -2585,9 +2585,9 @@ x >>u i = 749d5e4
 x >>s i = 749d5e4
 x cmpu y = lt
 x cmps y = gt
-utod x = 92c00000
+utod x = 41dd275792c00000
 dtou f = 2fc3f
-stod x = 92c00000
+stod x = 41dd275792c00000
 dtos f = 2fc3f
 
 x = 3c151d69
@@ -2609,9 +2609,9 @@ x >>u i = f0547
 x >>s i = f0547
 x cmpu y = lt
 x cmps y = lt
-utod x = b4800000
+utod x = 41ce0a8eb4800000
 dtou f = 189c1
-stod x = b4800000
+stod x = 41ce0a8eb4800000
 dtos f = 189c1
 
 x = 5aaa8d37
@@ -2633,9 +2633,9 @@ x >>u i = 5aaa8d37
 x >>s i = 5aaa8d37
 x cmpu y = lt
 x cmps y = gt
-utod x = 4dc00000
+utod x = 41d6aaa34dc00000
 dtou f = 25230
-stod x = 4dc00000
+stod x = 41d6aaa34dc00000
 dtos f = 25230
 
 x = 18f26935
@@ -2657,9 +2657,9 @@ x >>u i = 63c9a4
 x >>s i = 63c9a4
 x cmpu y = lt
 x cmps y = gt
-utod x = 35000000
+utod x = 41b8f26935000000
 dtou f = a37d
-stod x = 35000000
+stod x = 41b8f26935000000
 dtos f = a37d
 
 x = 192bb8e3
@@ -2681,9 +2681,9 @@ x >>u i = 1
 x >>s i = 1
 x cmpu y = lt
 x cmps y = lt
-utod x = e3000000
+utod x = 41b92bb8e3000000
 dtou f = a4f5
-stod x = e3000000
+stod x = 41b92bb8e3000000
 dtos f = a4f5
 
 x = f8e3afc1
@@ -2705,9 +2705,9 @@ x >>u i = 3e38ebf0
 x >>s i = fe38ebf0
 x cmpu y = gt
 x cmps y = gt
-utod x = f8200000
+utod x = 41ef1c75f8200000
 dtou f = 65f1f
-stod x = fc000000
+stod x = c19c7140fc000000
 dtos f = ffffd167
 
 x = bd748d4f
@@ -2729,9 +2729,9 @@ x >>u i = bd
 x >>s i = ffffffbd
 x cmpu y = gt
 x cmps y = lt
-utod x = a9e00000
+utod x = 41e7ae91a9e00000
 dtou f = 4d99d
-stod x = ac400000
+stod x = c1d0a2dcac400000
 dtos f = fffe4be5
 
 x = af977d0d
@@ -2753,9 +2753,9 @@ x >>u i = 2
 x >>s i = fffffffe
 x cmpu y = lt
 x cmps y = lt
-utod x = a1a00000
+utod x = 41e5f2efa1a00000
 dtou f = 47ec2
-stod x = bcc00000
+stod x = c1d41a20bcc00000
 dtos f = fffdf10a
 
 x = c301767b
@@ -2777,9 +2777,9 @@ x >>u i = c30
 x >>s i = fffffc30
 x cmpu y = gt
 x cmps y = gt
-utod x = cf600000
+utod x = 41e8602ecf600000
 dtou f = 4fdfd
-stod x = c2800000
+stod x = c1ce7f44c2800000
 dtos f = fffe7045
 
 x = 7dc31d19
@@ -2801,9 +2801,9 @@ x >>u i = 1f
 x >>s i = 1f
 x cmpu y = lt
 x cmps y = gt
-utod x = 46400000
+utod x = 41df70c746400000
 dtou f = 33831
-stod x = 46400000
+stod x = 41df70c746400000
 dtos f = 33831
 
 x = 37e3a067
@@ -2825,9 +2825,9 @@ x >>u i = 37e3
 x >>s i = 37e3
 x cmpu y = lt
 x cmps y = gt
-utod x = 33800000
+utod x = 41cbf1d033800000
 dtou f = 16e46
-stod x = 33800000
+stod x = 41cbf1d033800000
 dtos f = 16e46
 
 x = ae6e9be5
@@ -2849,9 +2849,9 @@ x >>u i = 2b9
 x >>s i = fffffeb9
 x cmpu y = lt
 x cmps y = lt
-utod x = 7ca00000
+utod x = 41e5cdd37ca00000
 dtou f = 47728
-stod x = 6c00000
+stod x = c1d4645906c00000
 dtos f = fffde970
 
 x = f5ecf713
@@ -2873,9 +2873,9 @@ x >>u i = f5ecf
 x >>s i = ffff5ecf
 x cmpu y = gt
 x cmps y = gt
-utod x = e2600000
+utod x = 41eebd9ee2600000
 dtou f = 64bb2
-stod x = da000000
+stod x = c1a42611da000000
 dtos f = ffffbdfb
 
 x = 700c571
@@ -2897,9 +2897,9 @@ x >>u i = 1c0
 x >>s i = 1c0
 x cmpu y = lt
 x cmps y = lt
-utod x = c4000000
+utod x = 419c0315c4000000
 dtou f = 2de5
-stod x = c4000000
+stod x = 419c0315c4000000
 dtos f = 2de5
 
 x = 1c9c267f
@@ -2921,9 +2921,9 @@ x >>u i = 1c9c26
 x >>s i = 1c9c26
 x cmpu y = lt
 x cmps y = gt
-utod x = 7f000000
+utod x = 41bc9c267f000000
 dtou f = bb7f
-stod x = 7f000000
+stod x = 41bc9c267f000000
 dtos f = bb7f
 
 x = 160b25bd
@@ -2945,9 +2945,9 @@ x >>u i = 582c
 x >>s i = 582c
 x cmpu y = lt
 x cmps y = lt
-utod x = bd000000
+utod x = 41b60b25bd000000
 dtou f = 9076
-stod x = bd000000
+stod x = 41b60b25bd000000
 dtos f = 9076
 
 x = b7c89aab
@@ -2969,9 +2969,9 @@ x >>u i = b7c89aa
 x >>s i = fb7c89aa
 x cmpu y = lt
 x cmps y = lt
-utod x = 55600000
+utod x = 41e6f91355600000
 dtou f = 4b471
-stod x = 55400000
+stod x = c1d20dd955400000
 dtos f = fffe26ba
 
 x = 2cd608c9
@@ -2993,9 +2993,9 @@ x >>u i = b3582
 x >>s i = b3582
 x cmpu y = lt
 x cmps y = gt
-utod x = 64800000
+utod x = 41c66b0464800000
 dtou f = 125d6
-stod x = 64800000
+stod x = 41c66b0464800000
 dtos f = 125d6
 
 x = 3f0e7f97
@@ -3017,9 +3017,9 @@ x >>u i = 3f0e7f97
 x >>s i = 3f0e7f97
 x cmpu y = lt
 x cmps y = gt
-utod x = cb800000
+utod x = 41cf873fcb800000
 dtou f = 19d3f
-stod x = cb800000
+stod x = 41cf873fcb800000
 dtos f = 19d3f
 
 x = 8fac7a95
@@ -3041,9 +3041,9 @@ x >>u i = 23eb1ea
 x >>s i = fe3eb1ea
 x cmpu y = gt
 x cmps y = lt
-utod x = 52a00000
+utod x = 41e1f58f52a00000
 dtou f = 3ad94
-stod x = 5ac00000
+stod x = c1dc14e15ac00000
 dtos f = fffd1fdc
 
 x = 59fac143
@@ -3065,9 +3065,9 @@ x >>u i = 5
 x >>s i = 5
 x cmpu y = lt
 x cmps y = gt
-utod x = 50c00000
+utod x = 41d67eb050c00000
 dtou f = 24db0
-stod x = 50c00000
+stod x = 41d67eb050c00000
 dtos f = 24db0
 
 x = 28e84721
@@ -3089,9 +3089,9 @@ x >>u i = a3a11c8
 x >>s i = a3a11c8
 x cmpu y = lt
 x cmps y = gt
-utod x = 90800000
+utod x = 41c4742390800000
 dtou f = 10c17
-stod x = 90800000
+stod x = 41c4742390800000
 dtos f = 10c17
 
 x = 14f70baf
@@ -3113,9 +3113,9 @@ x >>u i = 14
 x >>s i = 14
 x cmpu y = lt
 x cmps y = lt
-utod x = af000000
+utod x = 41b4f70baf000000
 dtou f = 8965
-stod x = af000000
+stod x = 41b4f70baf000000
 dtos f = 8965
 
 x = cabdfa6d
@@ -3137,9 +3137,9 @@ x >>u i = 3
 x >>s i = ffffffff
 x cmpu y = lt
 x cmps y = lt
-utod x = 4da00000
+utod x = 41e957bf4da00000
 dtou f = 530b0
-stod x = c9800000
+stod x = c1caa102c9800000
 dtos f = fffea2f9
 
 x = 72f5cadb
@@ -3161,9 +3161,9 @@ x >>u i = 72f
 x >>s i = 72f
 x cmpu y = gt
 x cmps y = gt
-utod x = b6c00000
+utod x = 41dcbd72b6c00000
 dtou f = 2f167
-stod x = b6c00000
+stod x = 41dcbd72b6c00000
 dtos f = 2f167
 
 x = cbc8e079
@@ -3185,9 +3185,9 @@ x >>u i = 32
 x >>s i = fffffff2
 x cmpu y = gt
 x cmps y = lt
-utod x = f200000
+utod x = 41e9791c0f200000
 dtou f = 53785
-stod x = c3800000
+stod x = c1ca1b8fc3800000
 dtos f = fffea9ce
 
 x = 7de2ac7
@@ -3209,9 +3209,9 @@ x >>u i = 7de
 x >>s i = 7de
 x cmpu y = lt
 x cmps y = gt
-utod x = 1c000000
+utod x = 419f78ab1c000000
 dtou f = 3390
-stod x = 1c000000
+stod x = 419f78ab1c000000
 dtos f = 3390
 
 x = 8a570545
@@ -3233,8 +3233,8 @@ x >>u i = 229
 x >>s i = fffffe29
 x cmpu y = gt
 x cmps y = lt
-utod x = a8a00000
+utod x = 41e14ae0a8a00000
 dtou f = 38a9f
-stod x = aec00000
+stod x = c1dd6a3eaec00000
 dtos f = fffcfce8
 
diff --git a/test/regression/int32.c b/test/regression/int32.c
index 254d0f8..bec50f0 100644
--- a/test/regression/int32.c
+++ b/test/regression/int32.c
@@ -4,6 +4,7 @@
 
 typedef unsigned int u32;
 typedef signed int s32;
+typedef unsigned long long u64;
 
 static u32 rnd32(void)
 {
@@ -60,11 +61,11 @@ static void test1(u32 x, u32 y)
   printf("x cmps y = %s\n",
          x == y ? "eq" : (s32)x < (s32)y ? "lt" : "gt");
   f = (double) x;
-  printf("utod x = %x\n", *((u32*) &f));
+  printf("utod x = %llx\n", *((u64*) &f));
   f = f * 0.0001;
   printf("dtou f = %x\n", (u32) f);
   f = (double) ((s32) x);
-  printf("stod x = %x\n", *((u32*) &f));
+  printf("stod x = %llx\n", *((u64*) &f));
   f = f * 0.0001;
   printf("dtos f = %x\n", (s32) f);
   printf("\n");