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

[Frama-c-discuss] Frama-C Bordon and Why 2.24



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>