Я хочу использовать реализацию sqrt fdlibm .
Эта реализация определяет (в соответствии с порядком байтов) некоторые макросы для доступа к младшему / старшему 32-битному двойному ) следующим образом (здесь: только версия с прямым порядком байтов):
#define __HI(x) *(1+(int*)&x)
#define __LO(x) *(int*)&x
#define __HIp(x) *(1+(int*)x)
#define __LOp(x) *(int*)x
В файле readme из flibm сказано следующее (немного сокращено)
Each double precision floating-point number must be in IEEE 754
double format, and that each number can be retrieved as two 32-bit
integers through the using of pointer bashing as in the example
below:
Example: let y = 2.0
double fp number y: 2.0
IEEE double format: 0x4000000000000000
Referencing y as two integers:
*(int*)&y,*(1+(int*)&y) = {0x40000000,0x0} (on sparc)
{0x0,0x40000000} (on 386)
Note: Four macros are defined in fdlibm.h to handle this kind of
retrieving:
__HI(x) the high part of a double x
(sign,exponent,the first 21 significant bits)
__LO(x) the least 32 significant bits of x
__HIp(x) same as __HI except that the argument is a pointer
to a double
__LOp(x) same as __LO except that the argument is a pointer
to a double
If the behavior of pointer bashing is undefined, one may hack on the
macro in fdlibm.h.
Я хочу использовать эту реализацию и эти макросы с проверщиком модели cbmc , который должен быть совместим с ansi-c .
Я не знаю точно, что не так, но следующий пример показывает, что эти макросы не работают (был выбран little-endian, было выбрано 32-битное машинное слово):
temp=24376533834232348.000000l (0100001101010101101001101001010100000100000000101101110010000111)
high=0 (00000000000000000000000000000000)
low=67296391 (00000100000000101101110010000111)
Кажется, что оба не правы. High кажется пустым для каждого значения temp.
Какие-нибудь новые идеи для доступа к обоим 32 словам с ansi-c?
ОБНОВЛЕНИЕ: Спасибо за все ваши ответы и комментарии. Все ваши предложения сработали для меня. На данный момент я решил использовать версию "R .." и отметил это как любимый ответ, потому что он кажется самым надежным в моем инструменте в отношении порядка байтов.