--- layout: fc_discuss_archives title: Message 74 from Frama-C-discuss on November 2013 ---
On 11/07/2013 11:15 PM, David Cok wrote: > 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? "in Frama-C" is not precise enough. Surely Value plugin supports mixing bitwise and arithmetic operators. For the Jessie plugin the answer is no. > - 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 > > > > _______________________________________________ > 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 >