--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on May 2012 ---
As a comment to my answer, let me add that assuming that it was a bug of the Boron version is actually false. The (more satisfactory) explanation is simply that the normalization process has changed between Boron and Nitrogen. In your case Nitrogen's normalization behavior is the same as Carbon's. Or-conditions are separated into two branches, and the code is shared through a goto statement. In Boron, the same code is duplicated in both branches, thereby not producing the "unexpected" goto. Therefore, both Frama-C versions are right in your example -- in a certain subtle way. Cheers, -- Richard Bonichon -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120514/a69e56b6/attachment.html>