--- layout: fc_discuss_archives title: Message 49 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")



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>