From 18bbf6d3cfb15219c87ebc79a5dd58bf75f2b4c4 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 3 Jul 2013 11:32:06 +0000 Subject: 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 --- test/regression/Results/int64 | 524 ++++++++++++++++++++++++++++++++++++++++-- test/regression/int64.c | 3 +- 2 files changed, 502 insertions(+), 25 deletions(-) (limited to 'test') 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 @@ -194,6 +194,34 @@ dtou f = 0 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 @@ -446,6 +474,34 @@ dtou f = 0 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 @@ -698,6 +754,34 @@ dtou f = 68db8bac710cb 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 @@ -950,6 +1034,34 @@ dtou f = 346dc 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 @@ -1202,6 +1314,34 @@ dtou f = 346dc 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 @@ -1454,6 +1594,34 @@ dtou f = 346dc5d638865 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 @@ -1706,6 +1874,34 @@ dtou f = 346dc5d638865 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 @@ -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)) -- cgit v1.2.3