Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value analysis loss of precision with bitwise XOR

  • Subject: [Frama-c-discuss] Value analysis loss of precision with bitwise XOR
  • From: sergio.feo at gmail.com (Sergio Feo)
  • Date: Thu, 6 Apr 2017 13:27:33 +0200
Dear all,
We have encountered the issue that Frama-C value analysis loses precision
when dealing with bitwise xor operations. Consider the following program:

int isTopBit(unsigned something)
{
unsigned topBitOnly = something & 0x80000000;
something ^= topBitOnly;
if (something & 0x80000000) {
Frama_C_show_each_true(something);
return 0;
}
else {
Frama_C_show_each_false(something);
return 1;
}
}

Here, the _if_ branch is dead code, since the lines before clear the bit
that is tested as the if condition. However, Frama-C outputs the following:

[value] Called Frama_C_show_each_true([0..4294967295])
[value] Called Frama_C_show_each_false([0..4294967295])
[value] Recording results for isTopBit
[value] done for function isTopBit
[value] ====== VALUES COMPUTED ======
[value] Values at end of function isTopBit:
  something ∈ [--..--]
  topBitOnly ∈ {0; 2147483648}
  __retres ∈ {0; 1}

Modifying the program to achieve the same result without the XOR operation
as in:

int isTopBit(unsigned something)
{
something &= 0x7fffffff;
if (something & 0x80000000) {
Frama_C_show_each_true(something);
return 0;
}
else {
Frama_C_show_each_false(something);
return 1;
}
}

then we obtain the following:

[value] Called Frama_C_show_each_false([0..2147483647])
[value] Recording results for isTopBit
[value] done for function isTopBit
[value] ====== VALUES COMPUTED ======
[value] Values at end of function isTopBit:
  something ∈ [0..2147483647]
  __retres ∈ {1}

which is the result we would expect from both versions.

Could you provide a pointer to the reasons why the abstract transformer for
the bitwise XOR behaves in this particular way?

Thanks a lot!

-- Sergio
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170406/5fc7f1b3/attachment.html>