--- layout: fc_discuss_archives title: Message 51 from Frama-C-discuss on February 2014 ---
Dear Boris, Thanks for this, as your suggestions, I have reinstalled Zarith 1.2 and Frama-c, why, why3. but the problem remains. Maybe I should try the 64-bit OS later? Regards, Xingyu. ________________________________________ -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140228/dd9b604f/attachment-0001.html> ------------------------------ Message: 2 Date: Fri, 28 Feb 2014 09:41:23 +0100 From: Boris Yakobowski <boris at yakobowski.org> To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> Subject: Re: [Frama-c-discuss] Uncaught exception: Invalid_argument("equal: abstract value") Message-ID: <CABbVA-AWFqeKhjWC_J+5ZDrM-Q+gi9Rau+=P2f2K650WqOcXag at mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1 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 ------------------------------ _______________________________________________ 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 End of Frama-c-discuss Digest, Vol 69, Issue 22 ***********************************************