--- layout: fc_discuss_archives title: Message 65 from Frama-C-discuss on April 2010 ---
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. An Nguyen. -- An Nhu Nguyen Faculty of Computer Science and Engineering Class: Honor Program 06 HCM City University of Technology Mobile: 0909048788 Y!M: annguyencs -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100423/a5886407/attachment-0001.htm>