--- layout: fc_discuss_archives title: Message 66 from Frama-C-discuss on April 2010 ---
On Fri, 23 Apr 2010, An Nguyen wrote: > Dear all, > > I have a problem with Frama-C Bordon + Why 2.24. I'm using Ubuntu 9.10. I > downloaded Frama-C Bordon package (without Jessie) on Frama-C's page. I > installed it using: > ./configure > make > sudo make install > Then, I downloaded Why 2.24 in Why's page and installed, also using: > ./configure > make > sudo make install > After that, I copied 6 executable files of these provers : simplify, > alt-ergo, z3, cvc3, yices, gappa to /bin. I executed why-config, all 6 > provers were accepted. > But when I used this command line "frama-c -jessie -jessie-atp alt-ergo > test.c" (as Frama-C Beryl with Jessie that I had used successfully > before), it failed. > > This is my test.c file : > /*@ ensures \result == ((i < j) ? j : i); */ > int maximum(int i, int j) { > *** return (i < j) ? j : i; > } > > This is which in terminal screen: > [kernel] preprocessing with "gcc -C -E -I.* -dD test.c" > [jessie] Starting Jessie translation > [jessie] Producing Jessie files in subdir test.jessie > [jessie] File test.jessie/test.jc written. > [jessie] File test.jessie/test.cloc written. > [jessie] Calling Jessie tool in subdir test.jessie > Generating Why function maximum > [jessie] Calling VCs generator. > why -alt-ergo [...] why/test.why > Running Alt-Ergo on proof obligations > (. = valid * = invalid ? = unknown # = timeout ! = failure) > why/test_why.why************* : [jessie] user error: Jessie subprocess > failed: make -f test.makefile alt-ergo > > Also with simplify, cvc3, z3, I had the same errors. > I think there's a mistake here. We only have why/test.why file but Jessie > calls to why/test_why.why file ? > > Thank you for reading my email. I'm looking forward to your help. > this sounds just like the problem I had a few days ago and Claude Marche posted a patch that fixed it for me (BTW less than 24h from problem report to patch - not bad !) pleas try this patch. you should be able to find the patch in the archive (Apr 21 Claude Marche) http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2010-April/001918.html respectively the actual attachment at: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/201004 21/675e83e2/attachment.bin thx! hofrat