--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on April 2017 ---
Dear Sergio, The loss of precision is normal: abstract-interpretation based analyzers compute only over-approximations of the possible values of a program, as computing the exact set of these values is undecidable. Here, the specific issue comes from the default abstractions of the Frama-C Value analysis, which is an interval of value. In the second example, we can deduce that: 0 <= something & 0x7FFFFFFF < 0x80000000 i.e. that the highest 5 bits are cleared. And thus that (something & 0x7FFFFFFFFF) & 0x80000000 is false. The first example is much more complex to prove, because it relies on a relation between topBitOnly and something (i.e. that a specific bit has the same value on both variables). The default abstraction of Values cannot prove this. One way to work around this problem would be to perform a case split at the beginning of the function on the value of this bit in something, and use another abstraction that records the possible values for each bit in a bitvector -- but I don't remember if this abstraction was incorporated in Eva. Best, Matthieu Sergio Feo <sergio.feo at gmail.com> writes: > 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 > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss