--- layout: fc_discuss_archives title: Message 97 from Frama-C-discuss on October 2013 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Problems with ensures



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>