--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on November 2019 ---
[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.