Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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>