--- layout: fc_discuss_archives title: Message 97 from Frama-C-discuss on October 2013 ---
Dear All, the attached file is a simple C program that (perhaps) computes the greatest common divisor of two integers. I have defined a predicate, IsGCD(a, b, val), that is true if val is the GCD of a and b. Frama-C can prove the loop invariant and variant, but cannot prove the ensures clause of the contract: I don't understand why. I am using Frama-C Fluorine-20130601, with Alt-Ergo prover (version 0.95.2), Jessie plug-in (version 2.33), Why 2.33 and Why3 0.81. Any help would be appreciated. Kind regards, Alessio Iotti -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131031/890e032c/attachment-0001.html> -------------- next part -------------- A non-text attachment was scrubbed... Name: gcd.c Type: text/x-csrc Size: 641 bytes Desc: not available URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20131031/890e032c/attachment-0001.c>