Follow-up to commit 2288: add test for special case of long division.

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

2 files changed, 502 insertions, 25 deletions

diff --git a/test/regression/Results/int64 b/test/regression/Results/int64
index fff6767..6e536f7 100644
--- a/test/regression/Results/int64
+++ b/test/regression/Results/int64
@@ -195,6 +195,34 @@ stod x = 0
 dtos f = 0
 
 x = 0
+y = 100000003
+-x = 0
+x + y = 100000003
+x - y = fffffffefffffffd
+x * y = 0
+x /u y = 0
+x %u y = 0
+x /s y = 0
+x %s y = 0
+x /u y2 = 0
+x %u y2 = 0
+x /s y3 = 0
+x %s y3 = 0
+~x = ffffffffffffffff
+x & y = 0
+x | y = 100000003
+x ^ y = 100000003
+x << i = 0
+x >>u i = 0
+x >>s i = 0
+x cmpu y = lt
+x cmps y = lt
+utod x = 0
+dtou f = 0
+stod x = 0
+dtos f = 0
+
+x = 0
 y = 14057b7ef767814f
 -x = 0
 x + y = 14057b7ef767814f
@@ -447,6 +475,34 @@ stod x = 3ff0000000000000
 dtos f = 0
 
 x = 1
+y = 100000003
+-x = ffffffffffffffff
+x + y = 100000004
+x - y = fffffffefffffffe
+x * y = 100000003
+x /u y = 0
+x %u y = 1
+x /s y = 0
+x %s y = 1
+x /u y2 = 1
+x %u y2 = 0
+x /s y3 = 1
+x %s y3 = 0
+~x = fffffffffffffffe
+x & y = 1
+x | y = 100000003
+x ^ y = 100000002
+x << i = 8
+x >>u i = 0
+x >>s i = 0
+x cmpu y = lt
+x cmps y = lt
+utod x = 3ff0000000000000
+dtou f = 0
+stod x = 3ff0000000000000
+dtos f = 0
+
+x = 1
 y = 9af678222e728119
 -x = ffffffffffffffff
 x + y = 9af678222e72811a
@@ -699,6 +755,34 @@ stod x = bff0000000000000
 dtos f = 0
 
 x = ffffffffffffffff
+y = 100000003
+-x = 1
+x + y = 100000002
+x - y = fffffffefffffffc
+x * y = fffffffefffffffd
+x /u y = fffffffd
+x %u y = 8
+x /s y = 0
+x %s y = ffffffffffffffff
+x /u y2 = ffffffffffffffff
+x %u y2 = 0
+x /s y3 = ffffffffffffffff
+x %s y3 = 0
+~x = 0
+x & y = 100000003
+x | y = ffffffffffffffff
+x ^ y = fffffffefffffffc
+x << i = fffffffffffffff8
+x >>u i = 1fffffffffffffff
+x >>s i = ffffffffffffffff
+x cmpu y = gt
+x cmps y = lt
+utod x = 43f0000000000000
+dtou f = 68db8bac710cb
+stod x = bff0000000000000
+dtos f = 0
+
+x = ffffffffffffffff
 y = 62354cda6226d1f3
 -x = 1
 x + y = 62354cda6226d1f2
@@ -951,6 +1035,34 @@ stod x = 41dfffffffc00000
 dtos f = 346dc
 
 x = 7fffffff
+y = 100000003
+-x = ffffffff80000001
+x + y = 180000002
+x - y = ffffffff7ffffffc
+x * y = 800000007ffffffd
+x /u y = 0
+x %u y = 7fffffff
+x /s y = 0
+x %s y = 7fffffff
+x /u y2 = 7fffffff
+x %u y2 = 0
+x /s y3 = 7fffffff
+x %s y3 = 0
+~x = ffffffff80000000
+x & y = 3
+x | y = 17fffffff
+x ^ y = 17ffffffc
+x << i = 3fffffff8
+x >>u i = fffffff
+x >>s i = fffffff
+x cmpu y = lt
+x cmps y = lt
+utod x = 41dfffffffc00000
+dtou f = 346dc
+stod x = 41dfffffffc00000
+dtos f = 346dc
+
+x = 7fffffff
 y = 144093704fadba5d
 -x = ffffffff80000001
 x + y = 14409370cfadba5c
@@ -1203,6 +1315,34 @@ stod x = 41e0000000000000
 dtos f = 346dc
 
 x = 80000000
+y = 100000003
+-x = ffffffff80000000
+x + y = 180000003
+x - y = ffffffff7ffffffd
+x * y = 8000000180000000
+x /u y = 0
+x %u y = 80000000
+x /s y = 0
+x %s y = 80000000
+x /u y2 = 80000000
+x %u y2 = 0
+x /s y3 = 80000000
+x %s y3 = 0
+~x = ffffffff7fffffff
+x & y = 0
+x | y = 180000003
+x ^ y = 180000003
+x << i = 400000000
+x >>u i = 10000000
+x >>s i = 10000000
+x cmpu y = lt
+x cmps y = lt
+utod x = 41e0000000000000
+dtou f = 346dc
+stod x = 41e0000000000000
+dtos f = 346dc
+
+x = 80000000
 y = 7b985bc1e7bce4d7
 -x = ffffffff80000000
 x + y = 7b985bc267bce4d7
@@ -1455,6 +1595,34 @@ stod x = 43e0000000000000
 dtos f = 346dc5d638865
 
 x = 7fffffffffffffff
+y = 100000003
+-x = 8000000000000001
+x + y = 8000000100000002
+x - y = 7ffffffefffffffc
+x * y = 7ffffffefffffffd
+x /u y = 7ffffffe
+x %u y = 80000005
+x /s y = 7ffffffe
+x %s y = 80000005
+x /u y2 = 7fffffffffffffff
+x %u y2 = 0
+x /s y3 = 7fffffffffffffff
+x %s y3 = 0
+~x = 8000000000000000
+x & y = 100000003
+x | y = 7fffffffffffffff
+x ^ y = 7ffffffefffffffc
+x << i = fffffffffffffff8
+x >>u i = fffffffffffffff
+x >>s i = fffffffffffffff
+x cmpu y = gt
+x cmps y = gt
+utod x = 43e0000000000000
+dtou f = 346dc5d638865
+stod x = 43e0000000000000
+dtos f = 346dc5d638865
+
+x = 7fffffffffffffff
 y = a220229ec164ffe1
 -x = 8000000000000001
 x + y = 2220229ec164ffe0
@@ -1707,6 +1875,34 @@ stod x = c3e0000000000000
 dtos f = fffcb923a29c779b
 
 x = 8000000000000000
+y = 100000003
+-x = 8000000000000000
+x + y = 8000000100000003
+x - y = 7ffffffefffffffd
+x * y = 8000000000000000
+x /u y = 7ffffffe
+x %u y = 80000006
+x /s y = ffffffff80000002
+x %s y = ffffffff7ffffffa
+x /u y2 = 8000000000000000
+x %u y2 = 0
+x /s y3 = 8000000000000000
+x %s y3 = 0
+~x = 7fffffffffffffff
+x & y = 0
+x | y = 8000000100000003
+x ^ y = 8000000100000003
+x << i = 0
+x >>u i = 1000000000000000
+x >>s i = f000000000000000
+x cmpu y = gt
+x cmps y = lt
+utod x = 43e0000000000000
+dtou f = 346dc5d638865
+stod x = c3e0000000000000
+dtos f = fffcb923a29c779b
+
+x = 8000000000000000
 y = c73aa0d9a415dfb
 -x = 8000000000000000
 x + y = 8c73aa0d9a415dfb
@@ -1762,33 +1958,285 @@ dtou f = a340baa47edc
 stod x = 43b8e9107ab99b8b
 dtos f = a340baa47edc
 
-x = e9bcd26890f095a5
-y = 329cb23ce0f7aa50
--x = 16432d976f0f6a5b
-x + y = 1c5984a571e83ff5
-x - y = b720202baff8eb55
-x * y = 9b6d58a9d0c15590
-x /u y = 4
-x %u y = 1f4a09750d11ec65
+x = 100000003
+y = 0
+-x = fffffffefffffffd
+x + y = 100000003
+x - y = 100000003
+x * y = 0
+x /u y = 0
+x %u y = 0
 x /s y = 0
-x %s y = e9bcd26890f095a5
-x /u y2 = 49e436778
-x %u y2 = 1e12e585
-x /s y3 = ffffffff8f651a9c
-x %s y3 = fffffffff9ade115
-~x = 16432d976f0f6a5a
-x & y = 209c922880f08000
-x | y = fbbcf27cf0f7bff5
-x ^ y = db20605470073ff5
-x << i = d26890f095a50000
-x >>u i = e9bcd26890f0
-x >>s i = ffffe9bcd26890f0
+x %s y = 0
+x /u y2 = 0
+x %u y2 = 0
+x /s y3 = 0
+x %s y3 = 0
+~x = fffffffefffffffc
+x & y = 0
+x | y = 100000003
+x ^ y = 100000003
+x << i = 100000003
+x >>u i = 100000003
+x >>s i = 100000003
+x cmpu y = gt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = 1
+-x = fffffffefffffffd
+x + y = 100000004
+x - y = 100000002
+x * y = 100000003
+x /u y = 100000003
+x %u y = 0
+x /s y = 100000003
+x %s y = 0
+x /u y2 = 0
+x %u y2 = 0
+x /s y3 = 0
+x %s y3 = 0
+~x = fffffffefffffffc
+x & y = 1
+x | y = 100000003
+x ^ y = 100000002
+x << i = 200000006
+x >>u i = 80000001
+x >>s i = 80000001
+x cmpu y = gt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = ffffffffffffffff
+-x = fffffffefffffffd
+x + y = 100000002
+x - y = 100000004
+x * y = fffffffefffffffd
+x /u y = 0
+x %u y = 100000003
+x /s y = fffffffefffffffd
+x %s y = 0
+x /u y2 = 1
+x %u y2 = 4
+x /s y3 = fffffffefffffffd
+x %s y3 = 0
+~x = fffffffefffffffc
+x & y = 100000003
+x | y = ffffffffffffffff
+x ^ y = fffffffefffffffc
+x << i = 8000000000000000
+x >>u i = 0
+x >>s i = 0
+x cmpu y = lt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = 7fffffff
+-x = fffffffefffffffd
+x + y = 180000002
+x - y = 80000004
+x * y = 800000007ffffffd
+x /u y = 2
+x %u y = 5
+x /s y = 2
+x %s y = 5
+x /u y2 = 0
+x %u y2 = 0
+x /s y3 = 0
+x %s y3 = 0
+~x = fffffffefffffffc
+x & y = 3
+x | y = 17fffffff
+x ^ y = 17ffffffc
+x << i = 8000000000000000
+x >>u i = 0
+x >>s i = 0
+x cmpu y = gt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = 80000000
+-x = fffffffefffffffd
+x + y = 180000003
+x - y = 80000003
+x * y = 8000000180000000
+x /u y = 2
+x %u y = 3
+x /s y = 2
+x %s y = 3
+x /u y2 = 0
+x %u y2 = 0
+x /s y3 = 0
+x %s y3 = 0
+~x = fffffffefffffffc
+x & y = 0
+x | y = 180000003
+x ^ y = 180000003
+x << i = 100000003
+x >>u i = 100000003
+x >>s i = 100000003
 x cmpu y = gt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = 7fffffffffffffff
+-x = fffffffefffffffd
+x + y = 8000000100000002
+x - y = 8000000100000004
+x * y = 7ffffffefffffffd
+x /u y = 0
+x %u y = 100000003
+x /s y = 0
+x %s y = 100000003
+x /u y2 = 2
+x %u y2 = 5
+x /s y3 = 2
+x %s y3 = 5
+~x = fffffffefffffffc
+x & y = 100000003
+x | y = 7fffffffffffffff
+x ^ y = 7ffffffefffffffc
+x << i = 8000000000000000
+x >>u i = 0
+x >>s i = 0
+x cmpu y = lt
 x cmps y = lt
-utod x = 43ed379a4d121e13
-dtou f = 5fbd298972a9d
-stod x = c3b6432d976f0f6a
-dtos f = ffff6e19ddd019d2
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = 8000000000000000
+-x = fffffffefffffffd
+x + y = 8000000100000003
+x - y = 8000000100000003
+x * y = 8000000000000000
+x /u y = 0
+x %u y = 100000003
+x /s y = 0
+x %s y = 100000003
+x /u y2 = 2
+x %u y2 = 3
+x /s y3 = fffffffffffffffe
+x %s y3 = 3
+~x = fffffffefffffffc
+x & y = 0
+x | y = 8000000100000003
+x ^ y = 8000000100000003
+x << i = 100000003
+x >>u i = 100000003
+x >>s i = 100000003
+x cmpu y = lt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = 100000003
+-x = fffffffefffffffd
+x + y = 200000006
+x - y = 0
+x * y = 600000009
+x /u y = 1
+x %u y = 0
+x /s y = 1
+x %s y = 0
+x /u y2 = 100000003
+x %u y2 = 0
+x /s y3 = 100000003
+x %s y3 = 0
+~x = fffffffefffffffc
+x & y = 100000003
+x | y = 100000003
+x ^ y = 0
+x << i = 800000018
+x >>u i = 20000000
+x >>s i = 20000000
+x cmpu y = eq
+x cmps y = eq
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 100000003
+y = e9bcd26890f095a5
+-x = fffffffefffffffd
+x + y = e9bcd26990f095a8
+x - y = 16432d986f0f6a5e
+x * y = 4e270cdeb2d1c0ef
+x /u y = 0
+x %u y = 100000003
+x /s y = 0
+x %s y = 100000003
+x /u y2 = 1
+x %u y2 = 16432d9b
+x /s y3 = fffffffffffffff5
+x %s y3 = b1d0a7b
+~x = fffffffefffffffc
+x & y = 1
+x | y = e9bcd26990f095a7
+x ^ y = e9bcd26990f095a6
+x << i = 6000000000
+x >>u i = 0
+x >>s i = 0
+x cmpu y = lt
+x cmps y = gt
+utod x = 41f0000000300000
+dtou f = 68db8
+stod x = 41f0000000300000
+dtos f = 68db8
+
+x = 329cb23ce0f7aa50
+y = 100000003
+-x = cd634dc31f0855b0
+x + y = 329cb23de0f7aa53
+x - y = 329cb23be0f7aa4d
+x * y = 78cdc106a2e6fef0
+x /u y = 329cb23c
+x %u y = 4921939c
+x /s y = 329cb23c
+x %s y = 4921939c
+x /u y2 = 329cb23ce0f7aa50
+x %u y2 = 0
+x /s y3 = 329cb23ce0f7aa50
+x %s y3 = 0
+~x = cd634dc31f0855af
+x & y = 0
+x | y = 329cb23de0f7aa53
+x ^ y = 329cb23de0f7aa53
+x << i = 94e591e707bd5280
+x >>u i = 65396479c1ef54a
+x >>s i = 65396479c1ef54a
+x cmpu y = gt
+x cmps y = gt
+utod x = 43c94e591e707bd5
+dtou f = 14bb101261e18
+stod x = 43c94e591e707bd5
+dtos f = 14bb101261e18
 
 x = 8362aa9340fe215f
 y = f986342416ec8002
@@ -4562,3 +5010,31 @@ dtou f = 57fdb3ba1ae09
 stod x = c3c496ce1b5230d4
 dtos f = fffef22280da9d3f
 
+x = 1b76f070b21414ad
+y = c3a4c9e29fe1f6b8
+-x = e4890f8f4debeb53
+x + y = df1bba5351f60b65
+x - y = 57d2268e12321df5
+x * y = 59fa2e56e95a1a58
+x /u y = 0
+x %u y = 1b76f070b21414ad
+x /s y = 0
+x %s y = 1b76f070b21414ad
+x /u y2 = 23effdd7
+x %u y2 = 272c2ddf
+x /s y3 = ffffffff8b8269ef
+x %s y3 = 39a9e8af
+~x = e4890f8f4debeb52
+x & y = 324c060920014a8
+x | y = dbf6f9f2bff5f6bd
+x ^ y = d8d239922df5e215
+x << i = ad00000000000000
+x >>u i = 1b
+x >>s i = 1b
+x cmpu y = lt
+x cmps y = gt
+utod x = 43bb76f070b21415
+dtou f = b3fdf698d581
+stod x = 43bb76f070b21415
+dtos f = b3fdf698d581
+
diff --git a/test/regression/int64.c b/test/regression/int64.c
index c0b6e56..5b32ccd 100644
--- a/test/regression/int64.c
+++ b/test/regression/int64.c
@@ -85,7 +85,8 @@ u64 special_values[] = {
   0x7FFFFFFFLLU,
   0x80000000LLU,
   0x7FFFFFFFFFFFFFFFLLU,
-  0x8000000000000000LLU
+  0x8000000000000000LLU,
+  0x100000003LLU
 };
 
 #define NUM_SPECIAL_VALUES (sizeof(special_values) / sizeof(u64))