--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on July 2012 ---
Le jeudi 26 juillet 2012, Pariente Dillon < Dillon.Pariente at dassault-aviation.com> a ?crit : > > > > > Maybe the explanation is that the relation between y==27 and b==1 is not stored by the analyzer after the if/else instr and the call to f in the main function, but only the intervals are kept (the domain of VA is interval abstract domain). > Hello, This explanation is completely correct, but you should be able to prove the original assertion with value, by adding another one before the if: //@ assert y < 27 ?? y == 27 ?? y > 27; Detailed explanation is hidden somewhere on the blog, but it boils down to the fact that y!=27 is not representable as an interval: you have to explicitely split the else branch in two parts (less and greater) which is done by the assert -- E tutto per oggi, a la prossima volta Virgile -------------- section suivante -------------- Une pi?ce jointe HTML a ?t? nettoy?e... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20120726/2fc59262/attachment.html>