--- layout: fc_discuss_archives title: Message 49 from Frama-C-discuss on February 2014 ---
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. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20140228/dd9b604f/attachment.html>