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")

  • Subject: [Frama-c-discuss] Uncaught exception: Invalid_argument("equal: abstract value")
  • From: Xingyu.Zhao.1 at city.ac.uk (Zhao, Xingyu)
  • Date: Fri, 28 Feb 2014 01:32:05 +0000
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>