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-discuss Digest, Vol 137, Issue 1

Hi Jens,

> thank you very much for the hint with 'native:coq".
> 
> By calling 'frama-c -wp-help' I have found out that '-wp-script' is now probably '-wp-coq-script'.
> This is certainly a better name but this change should be better documented.

Yes, you are absolutely right.

> If why3 is now used at compile time, is it then still necessary to call "why3 config --detect" after the installation of provers?

Definitively yes ! Frama-C is reading why3 configuration *at runtime* to find out prover configs, not at compile time.

> I also received a couple of warning for various provers along the lines of
> 
>  Eprover 2.4: Failed
>               [Why3 Error] anomaly: Why3.Whyconf.StepsCommandNotSpecified("The solver is used with a step limit and the command for running the solver with a step limit is not specified.")
>  Coq 8.9.1: Failed
>             [Why3 Error] anomaly: Why3.Whyconf.StepsCommandNotSpecified("The solver is used with a step limit and the command for running the solver with a step limit is not specified.")

Thanks for the report, we would look into it.
Side remark : using coq _via_ why3 is about to fail, since we have no script available for running the proof.
We probably should warn about this.

	L.