--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on September 2020 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to set WP and Why provers



藤谷さんへ、

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