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

  • Subject: [Frama-c-discuss] Frama-c-discuss Digest, Vol 137, Issue 1
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Thu, 7 Nov 2019 14:10:33 +0000
  • In-reply-to: <mailman.13.1573124411.13672.frama-c-discuss@lists.gforge.inria.fr>
  • References: <mailman.13.1573124411.13672.frama-c-discuss@lists.gforge.inria.fr>
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