需要帮助理解"静态分析仪的种类:与ASTREE的比较"中提出的浮点舍入

Tom*_*Tom 2 c floating-point

% cat double-float1.c

 int main () {
 double x; float a, y, z, r1, r2;
 a = 1.0; x = 1125899973951488.0; y = (x + a); z = (x - a);
 r1 = y - z; r2 = 2 * a;
 printf("(x + a) - (x - a) = %f\n", r1);
 printf("2a = %f\n", r2);
 }



% gcc double-float1.c >& /dev/null; ./a.out
 (x + a) - (x - a) = 134217728.000000
 2a = 2.000000
Run Code Online (Sandbox Code Playgroud)

更改最低有效数字后

% cat double-float2.c



int main () {
 double x; float a, y, z, r1, r2;
 a = 1.0; x = 1125899973951487.0; y = (x + a); z = (x - a);
 r1 = y - z; r2 = 2 * a;
 printf("(x + a) - (x - a) = %f\n", r1);
 printf("2a = %f\n", r2);
 }



% gcc double-float2.c >& /dev/null; ./a.out
 (x + a) - (x - a) = 0.000000
 2a = 2.000000
Run Code Online (Sandbox Code Playgroud)

任何人都可以帮助我理解第一个例子中的内部表示如何舍入到不同的值并在第二个示例中舍入到相同的值.链接到论文,我在上面找到了上面给出的例子.

各种静态分析仪:与ASTREE的比较

Gro*_*roo 5

原因是内部的浮点数必须使用精度有限的尾数来表示.首先,如果您存储的实际十进制数不能使用实际二进制数表示,则根据某些IEEE-754规则将其四舍五入到下一个最接近的二进制值.接下来,如果实际十进制数的位数多于浮点类型允许的精度,则即使使用十进制浮点类型,也必须进行舍入.

请注意,在这种情况下,根本原因是精度,而不是二进制格式,尽管二进制格式会增加额外的混淆,因为它四舍五入到可用24位二进制数字表示的最接近的数字.如果您的语言具有10位精度的本机十进制浮点类型,则仍需要在内存中舍入数字:

Decimal number     | Nearest decimal with 10 digits precision 
------------------ | ---------------------------------------
123450000149997.0  | 123450000100000
123450000149998.0  | 123450000100000
123450000149999.0  | 123450000100000
123450000150000.0  | 123450000200000
123450000150001.0  | 123450000200000
123450000150002.0  | 123450000200000

在您的情况下,舍入点恰好在1125899973951488和之间1125899973951489.由于32位浮点数具有24位精度(为尾数保留23位+隐式前导位设置为1),因此它可以具有~7.22十进制数的近似小数精度.这是数字存储在您的示例中的方式:

Decimal number     | Actual IEEE-754 value | IEEE-754 bits (sign, exponent, mantissa)
------------------ | ----------------------|-----------------------------------------
1125899973951486.0 | 1125899906842624      | 0 10110001 00000000000000000000000
1125899973951487.0 | 1125899906842624      | 0 10110001 00000000000000000000000
1125899973951488.0 | 1125899906842624      | 0 10110001 00000000000000000000000
1125899973951489.0 | 1125900041060352      | 0 10110001 00000000000000000000001
1125899973951490.0 | 1125900041060352      | 0 10110001 00000000000000000000001
1125899973951491.0 | 1125900041060352      | 0 10110001 00000000000000000000001

所以(x - 1),(x + 1)并将圆到相同的值,直到你达到1125899973951488.0.要探索如何使用IEEE-754在内部存储浮点数,您可以使用一个有用的在线计算器.