--- layout: fc_discuss_archives title: Message 46 from Frama-C-discuss on April 2010 ---
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