--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on September 2020 ---
è¤è°·ããã¸ã 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