--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on October 2013 ---
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; }