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

[Frama-c-discuss] euklid.c



Here is an old example from Frama-C/Jessie that I tried to re-run using the latest versions of the tools.    An error occurs---just wondering if anyone has any idea why.  It is a neat example.
-Steve


user at cisc614:~/614/frama-c/examples/basic$ frama-c -jessie euklid.c
[kernel] preprocessing with "gcc -C -E -I.  -dD euklid.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir euklid.jessie
[jessie] File euklid.jessie/euklid.jc written.
[jessie] File euklid.jessie/euklid.cloc written.
[jessie] Calling Jessie tool in subdir euklid.jessie
Uncaught exception: Invalid_argument("equal: abstract value")
[jessie] user error: Jessie subprocess failed:   jessie  -why3ml  -v       -locs euklid.cloc euklid.jc

euklid.c:

/*
    Define a predicate div(a,b), meaning "a divides b",
    and declare some basic axiomatic properties.
*/
/*@ axiomatic Euklid {
    predicate div(integer a,integer b) = (0 < a && 0 <= b && b%a == 0);
    axiom A1:
	\forall integer a, b, c;
	     b >= c && div(a,b) && div(a,c) ==> div(a,b-c);
    axiom A2:
	\forall integer a, b, c;
	     b >= c && div(a,c) && div(a,b-c) ==> div(a,b);
}
*/



/*@ 
    requires A > 0 && B > 0;
    ensures  \forall integer i; div(i,A) && div(i,B) <==> div(i,\result);
*/
int gcd(int A,int B)
{
    int const a = A, b = B;

    /*@ loop invariant a > 0 && b > 0;
        loop invariant \forall integer i;
		       div(i,a) && div(i,b) <==> div(i,A) && div(i,B);
        loop variant   a + b;
    */
    while (a != b)
        if (a > b)
             a -= b;
        else
             b -= a;
    return a;
}