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] How to set WP and Why provers

  • Subject: [Frama-c-discuss] How to set WP and Why provers
  • From: jens.gerlach at fokus.fraunhofer.de (Gerlach, Jens)
  • Date: Thu, 17 Sep 2020 10:23:44 +0000
  • In-reply-to: <3AA9914846C28F4BA8158AF599B6C0C902CACCEFF6@jspex01.jtekt.local>
  • References: <3AA9914846C28F4BA8158AF599B6C0C902CACCEFF6@jspex01.jtekt.local>
藤谷さんへ、

Fraunhofer Fokusのイェンスです。

Installing Frama-C can sometimes be tricky but in general it has greatly improved over the last years.

Here are the installation instructions that we use to work with Frama-C/WP on „ACSL by Example“
	https://github.com/fraunhoferfokus/acsl-by-example

These instructions work both on recent ubuntu releases and macOS
First you must install opam (something like „sudo apt install opam“ on ubuntu).

$ opam init --yes --comp=4.09.1
$ opam install --yes depext
$ opam depext --yes frama-c
$ opam pin add --yes coqide 8.9.1   
	(I am not sure you want to use Coq but I have added it anyway.)
$ opam install --yes frama-c alt-ergo why3 why3-coq
$ why3 config --full-config

(You can of course add more provers such as z3 or cvc4).

Regarding your swap.c example, I could not see the source code.
Therefore, I cannot give you specific tips.
But I guess it looks a bit like here
	https://github.com/fraunhoferfokus/acsl-by-example/tree/master/StandardAlgorithms/mutating/swap
Maybe this can help you.

ほかの質問があったらぜひ聞いてください。

Jens Gerlach