--- layout: fc_discuss_archives title: Message 53 from Frama-C-discuss on July 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Value Analysis and the modulo operator



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>