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] [Why3-club] why3-0.88.0 and CVC4 1.4/1.5

  • Subject: [Frama-c-discuss] [Why3-club] why3-0.88.0 and CVC4 1.4/1.5
  • From: Claude.Marche at inria.fr (Claude Marché)
  • Date: Mon, 23 Oct 2017 13:25:42 +0200
  • In-reply-to: <DEE01F38-E4E2-4FB9-A24F-EC4112C5790E@fokus.fraunhofer.de>
  • References: <DEE01F38-E4E2-4FB9-A24F-EC4112C5790E@fokus.fraunhofer.de>
Hello,

[forwarding to Frama-C list since other users of WP plug-in may help]	


Le 20/10/2017 à 14:07, Gerlach, Jens a écrit :
> A while ago I experimented with why3-0.87.3 and cvc4.
> 
> At that time I reported that version 1.5 of cvc4 performed considerable
> worse than version 1.4.
> 
> This issue was later explained that cvc4_15.drv
> 
> “… was made  before the actual release of cvc4 1.5. Even cvc4_15.drv
> from Why3 master would not give optimal results yet …”
> 
> Now, why3-0.88.0 has been released.
> 
> During configuration why3 suggests to upgrade from cvc4-1.4 :
> Found prover CVC4 version 1.4 (old version, please consider upgrading).
> I have evaluated therefore again version 1.5 of cvc4 against version 1.4.
> 
> This time, however, version 1.5 could not prove any proof obligation
> from “ACSL by Example”!


This is not at all what we observed on the collection of examples
directly written in Why3, on examples processed by Frama-C/Jessie and on
examples in SPARK/Ada.

It is likely that there is a misconfiguration somewhere in the tool
chain WP -> Why3.

To debug, the first thing you should look at is the output of the call
to cvc4. within Why3 it can be done with

why3 prove -D CVC4,1.5 file.mlw (or file.why)

so you need to get the intermediate file generated by WP sent to Why3.

Also, you should be sure you use the same Why3 config as WP, so may be

why3 prove -C <why3 config file> ...

Going further, you may have more details using

why3 prove --debug call_prover ...


Don't know how to help further. If you can send the C source code or the
.mlw intermediate file I may try to have a look.

- Claude


> 
> Again, I wonder, if there is anything on my side that we should have
> taken into account.
> 
>  
> 
> Regards
> 
>  
> 
> Jens
> 
>  
> 
> 
> 
> _______________________________________________
> Why3-club mailing list
> Why3-club at lists.gforge.inria.fr
> https://lists.gforge.inria.fr/mailman/listinfo/why3-club
> 

-- 
Claude Marché                          | tel: +33 1 69 15 66 08
INRIA Saclay - ÃŽle-de-France           |
Université Paris-sud, Bat. 650         | http://www.lri.fr/~marche/
F-91405 ORSAY Cedex                    |