--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on April 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] why-2.24 install question



On Wed, 21 Apr 2010, Claude Marche wrote:

>
> Here is a patch that should fix the problem. apply using
>
> patch -p0 < why-2.24.patch
>
> in the main directory where you uncompressed why-2.24.tar.gz
>
> Sorry for the inconvenience.
> I'm waiting for a while, if other problems like that show up, and then  
> we will make a new release
>

cd why-2.24
patch -p0 < why-2.24.patch
make clean
./configure
make
make install

the make problem is gone for alt-ergo,z3,cvc3,simplify - Thanks !

from the makefile - I guess for isabelle you also would need
Isabelle -> Isabelle.output_file (fwe ^ "_why.thy") ??

and... a new one poped up (max example from tutorial):

/*@ 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 == ((*i < *j) ? *j : *i);
  @   ensures \result == 0;
  @*/
int max(int *r, int* i, int* j) {
        if (!r) return -1;
        *r = (*i < *j) ? *j : *i;
        return 0;
}

...
max1.c:2:[kernel] user error: Error during annotations analysis: unbound logic variable NULL
...

if I remove the respective statements its "ok" - did not look into this in detail though.

/*@ requires \valid(i) && \valid(j);
  @ requires \valid(r);
  @ assigns *r;
  @ behavior zero:
  @   assigns \nothing;
  @   ensures \result ==  -1;
  @ behavior normal:
  @   assumes \valid(r);
  @   assigns *r;
  @   ensures *r == ((*i < *j) ? *j : *i);
  @   ensures \result == 0;
  @*/
int max(int *r, int* i, int* j) {
        if (!r) return -1;
        *r = (*i < *j) ? *j : *i;
        return 0;
}

[kernel] preprocessing with "gcc -C -E -I.  -dD max.c"
[jessie] Starting Jessie translation
[jessie] Producing Jessie files in subdir max.jessie
[jessie] File max.jessie/max.jc written.
[jessie] File max.jessie/max.cloc written.
[jessie] Calling Jessie tool in subdir max.jessie
Generating Why function max
[jessie] Calling VCs generator.
why -alt-ergo [...] why/max.why
Running Alt-Ergo on proof obligations
(. = valid * = invalid ? = unknown # = timeout ! = failure)
why/max_why.why               : ......?..?....?/bin/sh: line 1: 23245 CPU time limit exceeded why-cpulimit 10 alt-ergo /tmp/41f327ergo.why 2>&1
#?/bin/sh: line 1: 23249 CPU time limit exceeded why-cpulimit 10 alt-ergo /tmp/b00464ergo.why 2>&1
#........ (20/0/4/2/0)
total   :  26
valid   :  20 ( 77%)
invalid :   0 (  0%)
unknown :   4 ( 15%)
timeout :   2 (  8%)
failure :   0 (  0%)
total wallclock time : 21.17 sec
total CPU time       : 20.91 sec
valid VCs:
    average CPU time : 0.04
    max CPU time     : 0.05
invalid VCs:
    average CPU time : nan
    max CPU time     : 0.00
unknown VCs:
    average CPU time : 0.05
    max CPU time     : 0.06

thx!
hofrat