Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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