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



Hello Virgile,

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.

If why3 is now used at compile time, is it then still necessary to call "why3 config --detect" after the installation of provers?
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.")

Regards

Jens