--- layout: fc_discuss_archives title: Message 50 from Frama-C-discuss on February 2014 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Uncaught exception: Invalid_argument("equal: abstract value")



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