--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on November 2013 ---
Using a bit-vector logic avoids the modulo operations, but also, I suspect, introduces difficulties in mapping to and from integer variables. Has that been tried in practice in Frama-C? - David On 11/7/2013 4:54 PM, Pascal Cuoq wrote: > On Thu, Nov 7, 2013 at 10:26 PM, John Regehr <regehr at cs.utah.edu > <mailto:regehr at cs.utah.edu>> wrote: > > > If I understand correctly, Jessie's three integer models are: > > - math -- infinite range > - modulo -- both signed and unsigned behave as if two's complement > - strict -- no overflow permitted > > The problem is that none of these is a match for C. In C, unsigned > integers follow the modulo rules and signed integers follow the > strict rules. Is there a way to get the C integer model in Jessie? > Otherwise it seems like I might be stuck with some strange tradeoffs. > > > I second the wish for a C mode ---as a user. However, here is what I > think a hypothetical weakest precondition plug-in implementor might say: > > "math" is not sound for any serious definition of sound. Instead of > weakening the definition of "sound" to the point of ridiculousness > (http://soundiness.org/documents/InDefenseOfUnsoundness.pdf ---damn, > another blog post to write), we can choose the honorable path and > forget that "math" even exists. > > "modulo" inserts modulo operations everywhere, making proof > obligations impossibly hard for existing automatic provers. That it is > unusable in practice might actually be good news, as it too is ---as > you rightly point out--- unsound with respect to the C standard > (although it may be sound with respect to a specific compiler, perhaps > used with specific options). > > If a function happens to be verifiable with "strict", that is, if for > the inputs it expects, it never relies on the wrap-around behavior of > unsigned overflow, then it should be verified with "strict". With > respect to the "C" mode that regretfully does not exist, this only > adds additional proof obligations, which should individually be easy > to prove, instead of sprinkling existing proof obligations with modulo > operations that make them extremely difficult to tackle for existing > automatic provers. Any function verified with "strict" works when > executed in C. The only issue is that some functions that work > according to the C standard cannot be verified with "strict", because > they rely on unsigned overflow behavior. > > Something that would be better than "modulo", and better than the "C" > mode you request, is a mode similar to "strict" but that would let the > operator specify only the few unsigned operations that are supposed to > wrap around, and would only insert modulo operations for these ones. > The other overflows, that wouldn't harm according to the standard, > would still be assumed not to happen (no modulo inserted) and proved > not to happen (but as long as it is true that they do not happen, why > not prove it as a useful intermediate lemma?). This would likely work > quite well in practice. > > Perhaps real implementors of weakest precondition Frama-C plug-ins > will want to differ. This is only the opinion of a hypothetical character. > > Pascal > > > _______________________________________________ > Frama-c-discuss mailing list > Frama-c-discuss at lists.gforge.inria.fr > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131107/e4e9a088/attachment-0001.html>