--- layout: fc_discuss_archives title: Message 66 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



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