--- layout: fc_discuss_archives title: Message 1 from Frama-C-discuss on April 2017 ---
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>