Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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