--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on February 2014 ---
Can you try again after installing the Zarith library, then recompiling Frama-C [2] and Jessie? Those kind of problems are often caused by comparisons on big integers, which no longer fail with Zarith. [1] http://forge.ocamlcore.org/projects/zarith/ , but it may be packaged by your Linux distrubution, and is packaged by Opam [2] Check that the configure step does not mention a problem about Zarith missing. On Fri, Feb 28, 2014 at 2:32 AM, Zhao, Xingyu <Xingyu.Zhao.1 at city.ac.uk> wrote: > Dear All, > > > I encountered an error today on my 32-bit 13.10 Ubuntu with > > > frama-c-Fluorine-20130601 > Why3 0.81 > Why2.33 > Ocaml 3.12.1 > > The source code, which is directly cited from a tutorial so must be correct, > is: (5.c) > > /*@ requires \valid(i) && \valid(j); > @ requires r == \null || \valid(r); > @ assigns *r; > @ behavior zero: > @ assumes r == \null; > @ assigns \nothing; > @ ensures \result == -1; > @ behavior normal: > @ assumes \valid(r); > @ assigns *r; > @ ensures *r == \max(*i,*j); > @ ensures \result == 0; > @*/ > int max(int *r, int* i, int* j) { > if (!r) return -1; > *r = (*i < *j) ? *j : *i; > return 0; > } > > > then I type in the command line: > > frama-c -jessie 5.c > > then, I got: > > [kernel] preprocessing with "gcc -C -E -I. -dD 5.c" > [jessie] Starting Jessie translation > [jessie] Producing Jessie files in subdir 5.jessie > [jessie] File 5.jessie/5.jc written. > [jessie] File 5.jessie/5.cloc written. > [jessie] Calling Jessie tool in subdir 5.jessie > Uncaught exception: Invalid_argument("equal: abstract value") > [jessie] user error: Jessie subprocess failed: jessie -why3ml -v -locs > 5.cloc 5.jc > > then I slightly modified the source code into: > > /*@ requires \valid(i) && \valid(j); > @ requires r == \null || \valid(r); > @ assigns *r; > @ behavior zero: > @ assumes r == \null; > @ assigns \nothing; > @ ensures \result == -1; > @ behavior normal: > @ assumes \valid(r); > @ assigns *r; > @ ensures *r == \max(*i,*j); > @ ensures \result == 0; > @*/ > int max(int *r, int* i, int* j) { > if (!r) return -1; > r = (*i < *j) ? j : i; > return 0; > } > > That is to avoid codes like *r=*i, then the error gone. > > Can anyone help? I googled this error myself, there are two answers: > > 1. the low version of Ocaml (seems wrong answer) > 2. due to 32-bit Ubuntu, if reinstall 64-bit will be > OK.(http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-October/003951.html) > > Any help will be appreciated? > > Regards, > Xingyu. > > > > > > > > > > _______________________________________________ > 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 -- Boris