diff --git a/dokuwiki/compiling_from_source.md b/dokuwiki/compiling_from_source.md deleted file mode 100755 index f8060bf18212bd20f3a6d6cec7908a3fe4f9d79d..0000000000000000000000000000000000000000 --- a/dokuwiki/compiling_from_source.md +++ /dev/null @@ -1,410 +0,0 @@ ---- -layout: clean_page ---- -# Compiling Frama-C from source - -This page explains how to build Frama-C from source, for the platforms -on which no binaries are available. If a binary is available at -<http://frama-c.com/download.html>, we suggest you use it instead. - -## Compiling under Linux - -If you are using Linux, your distribution may package Frama-C. This is -currently the case for (at least) Ubuntu, Debian and Fedora. - -If you want to compile a distribution more recent than the one packaged -with your system, you will find detailed compilation instructions in the -INSTALL file of the Frama-C tarballs. - -## Compiling under Windows (Cygwin + MinGW) - -**If you already know how to use OPAM, simply install the `frama-c` -package. The instructions below are for users who have never used OPAM + -Cygwin.** - -Although Frama-C is **not** officially supported on Windows (that is, -the Frama-C team cannot guarantee that it will always work on Windows -environments), it it possible to compile and use it. In case of errors, -you can refer to StackOverflow questions tagged `frama-c` (or ask them -yourself). - -The recommended procedure is to use OPAM for MinGW OCaml: - -1. Install [OCaml for Windows](https://fdopen.github.io/opam-repository-mingw/) (the - graphical installer should be fine). Note that newer releases of - OCaml are not always backwards-compatible with Frama-C releases. -2. Follow fdopen's instructions, in particular: -3. Install depext (''opam install depext'') and [depext-cygwinports](http://fdopen.github.io/opam-repository-mingw/depext-cygwin/). This is necessary especially for the Frama-C GUI, which uses lablgtk. -4. Do not forget to update your PATH variable as indicated, or use ''ocaml-env''. -5. Install Frama-C dependencies: <code>opam depext frama-c</code> -6. Install Frama-C itself: <code>opam install frama-c</code> - - -And it's done\! - -**Note:** By default, Cygwin defines the `CPP` variable in its -environment. If you are using Frama-C 14 (Silicon) or older, append `-C --I.` to the value of that variable. For instance, by adding the -following line to your `.bashrc` file: - - export CPP="x86_64-w64-mingw32-cpp.exe -C -I." - -The snippet above is for the 64-bit version. - -You also need to systematically add `-pp-annot` to your command-line, -otherwise annotations in source files may not be processed. - -## Obsolete procedures - should NOT be necessary (only presented for historical reasons) - -An obsolete procedure using WODI is also presented but only for -historical reasons. It is unlikely to work with recent lablgtk and -Frama-C releases. - -**Note**: the procedure below is not 100% robust, but it has been tested -on a few different configurations. We recommend referring to the [GitHub -OPAM repository for -MinGW](https://github.com/fdopen/opam-repository-mingw) or asking a -question on [StackOverflow](http://stackoverflow.com) if you have -problems compiling it (e.g. if your Windows username contains spaces, -[this Cygwin FAQ](https://www.cygwin.com/faq.html#faq.setup.name-with-space) -referenced by fdopen indicates how to fix it). - -##### Old procedure - -1\. Download (but do not run yet\!) the [Cygwin setup -file](https://cygwin.com/install.html) to your Desktop. - - - Both 32-bit and 64-bit versions should work; we tested in particular - the 32-bit version, which is the one used in the commands below. - -2\. Open a Command Prompt and run the command below to install Cygwin -with necessary Frama-C dependencies. - - - The command below will use the downloaded Cygwin setup file. - - You just have to keep clicking Next (using the default provided - paths) and choose the Cygwin mirror of your preference. Then keep - pressing Next and wait for the installation to finish. - -<!-- end list --> - - %USERPROFILE%/Desktop/setup-x86.exe --root=C:/cygwin32 --local-package-dir C:/cygwin32/packages --no-startmenu --quiet-mode --packages=make,mingw64-i686-gcc-core,m4,patch,unzip,procmail,rsync,wget,diffutils,git,perl,curl,autoconf - -3\. Cygwin will create a Desktop shortcut. Open it and you will be -presented a terminal. Use it to run the code below. Please note that -this code downloads the [OPAM for MinGW OCaml](https://github.com/fdopen/opam-repository-mingw) binaries from -Dropbox. - - - You can copy the code below and paste it on the Cygwin terminal. - - You can also click on `frama-c-install-windows.sh` to download the - code. In that case, save it to your **cygwin** home directory (i.e. - `C:\cygwin32\home\<username>`), and execute it on your Cygwin - terminal: `bash frama-c-install-windows.sh`). - -<!-- end list --> - -``` bash -#!/bin/bash -eu - -# Download the OPAM 32-bit archive for MinGW (https://github.com/fdopen/opam-repository-mingw) -wget "https://dl.dropboxusercontent.com/s/eo4igttab8ipyle/opam32.tar.xz" -O opam32.tar.xz - -# Uncompress and install OPAM -tar -xf 'opam32.tar.xz' -bash opam32/install.sh - -# Use OPAM to install a 4.02.3 OCaml compiler -opam init mingw 'https://github.com/fdopen/opam-repository-mingw.git' --comp 4.02.3+mingw32 --switch 4.02.3+mingw32 --yes - -# This variable is important for installing lablgtk -# If installing a 64-bit OCaml, replace "i686" with "x86_64" -export PATH=/usr/i686-w64-mingw32/sys-root/mingw/bin:$PATH -echo 'export PATH=/usr/i686-w64-mingw32/sys-root/mingw/bin:$PATH' >> .bashrc - -# This is necessary for configuring OPAM -eval `opam config env` -echo 'eval `opam config env`' >> ~/.bashrc - -# To apply a more modern-looking GTK theme -echo 'gtk-theme-name = "MS-Windows"' > ~/.gtkrc-2.0 - -# Install depext and depext-cygwinports, which will allow dependencies to be -# automatically installed -opam install depext depext-cygwinports --yes - -# Install the latest available Frama-C and its dependencies using depext -OPAMYES=yes opam depext -i frama-c - -echo "Done!" -echo "Do not forget to close and re-open your terminal to ensure that" -echo "environment variables are properly refreshed." -``` - -4\. It's done\! You can now run Frama-C from the command line -(`frama-c`) or the GUI (`frama-c-gui`). - -#### Old procedure based on WODI (GODI for Windows) + Cygwin + MinGW - -**Note:** This procedure is now **obsolete**\! Using OPAM should be -easier (and also allows easier installation of optional Frama-C -dependencies such as external solvers). - -These steps were tested on a Sodium release with Cygwin 32 bits + WODI -32 bits, and then tested again on a Magnesium release with Cygwin 64 -bits + WODI 64 bits. Similar combinations should work as well. They were -tested on Windows 7 and on Windows 8.1. - -These are thorough instructions to install Frama-C and its dependencies -including the GUI. Some steps are not necessary if you do not need the -GUI. These instructions are very detailed to help you troubleshoot if -something unexpected happens. - -The instructions below assume the 64-bit version in some commands; -replace `64` with `32` when appropriate if using the 32-bit version. - -1. Install a native Windows OCaml compiler using Jonathan Protzenko's - [Ocaml on Windows](http://protz.github.io/ocaml-installer/) - installer. During OCaml installation, check the option to install - Cygwin. It will put Cygwin's setup file in your Desktop. - - Frama-C Sodium was tested using - [OCaml 4.02.1, 32-bit](http://gallium.inria.fr/~protzenk/caml-installer/ocaml-4.02.1-i686-mingw64-installer3.exe) - while Magnesium was tested using - [OCaml 4.02.3, 64-bit](http://gallium.inria.fr/~protzenk/caml-installer/ocaml-4.02.3-x86_64-mingw64-installer4-opam.exe). - - **Note:** The link to the 64-bit version includes OPAM, but we - did not use it in our tests (issues with lablgtk prevented us - from successfully running Frama-C's GUI). -2. Install Cygwin (32-bit or 64-bit). You can use the setup file from - Ocaml on Windows' installation. This will configure Cygwin's - installation directory (e.g. `C:\cygwin64`) and a working - mirror. This configuration will be later used to install required - Cygwin packages. - - Note that Cygwin's setup remember previous settings when run - again; it works similarly to a graphical package manager on - Debian systems, such as `synaptic`: you must run it again - whenever you need to install or remove a package. After the - first installation, you just have to click Next until the - package selection screen is presented again. -3. Using Cygwin's setup, install package `mingw64-i686-gcc-core` (for - the 32-bit version) or `mingw64-x86_64-gcc-core` (for the 64-bit - version). - - Note that **both** use `mingw64` in their name (this is not a - typo). - - Also note that these packages install cross-compilers, therefore - there will be no `gcc` executable, but instead you'll have - either `i686-w64-mingw32-gcc` on 32 bits or - `x86_64-w64-mingw32-gcc` on 64 bits. -4. Open a Cygwin terminal. Export the location of your Cygwin setup - file under variable `CYGSETUP_BIN`, e.g. using this command: `export - CYGSETUP_BIN=/cygdrive/C/Users/Public/Desktop/cygwin-setup-x86_64.exe` - -<!-- end list --> - -``` - * (This step is not necessary per se, but it simplifies these instructions.) - * Remember that this variable will not be saved across Cygwin sessions, so if you close and reopen your Cygwin terminal you'll need to export it again. -- Before installing [[http://wodi.forge.ocamlcore.org/|WODI]] (for Frama-C dependencies), you'll need to install a few additional Cygwin packages. Using the ''CYGSETUP_BIN'' variable defined previously, you can run: <code>"$CYGSETUP_BIN" --quiet-mode --no-desktop --no-startmenu --packages=dos2unix,diffutils,cpio,make,patch,rlwrap</code> - * If you have issues or need more information, follow the instructions [[http://wodi.forge.ocamlcore.org/|in WODI's page]]. -- Install [[http://wodi.forge.ocamlcore.org/|WODI]] by downloading and uncompressing its tar.xz archives. - * WODI has been discontinued, but its installer and a tar.xz containing its binary packages are still available on its website. - * The 32-bit version has been tested with Frama-C Sodium and the 64-bit version has been tested with Frama-C Magnesium. - * Here are direct links to the files: - * [[https://dl.dropbox.com/sh/t9ozci9rso9gij4/AABS0ZGie-RdZDxyRaDKImWVa/wodi32.tar.xz|WODI (32 bits)]] + [[https://dl.dropbox.com/sh/feldcwshtinmdo8/AAAaEK0cJoB1h6UDh4Vbvpaaa/packages32.tar.xz|all packages (32 bits)]]. - * [[https://dl.dropbox.com/sh/t9ozci9rso9gij4/AADtoDkuFC9ALiLduQ73VOzla/wodi64.tar.xz|WODI (64 bits)]] + [[https://dl.dropbox.com/sh/feldcwshtinmdo8/AADlqehWQ17xVWCW2GGHIo_za/packages64.tar.xz|all packages (64 bits)]]. - * Quick installation: uncompress WODI (''tar xvf wodi64.tar.xz''), run ''cd wodi64'' and then ''./install.sh''. This should copy WODI's files to ''/opt/wodi64''. - * Run ''tar xvf packages64.tar.xz'' and put its files (all files inside the directory, without the directory name itself) into your Cygwin's ''/opt/wodi64/var/cache/godi'' directory (e.g. ''C:\cygwin64\opt\wodi64\var\cache\godi''). This can be done by running: <code>mv packages64/* /opt/wodi64/var/cache/godi/</code> - * Note that installing WODI in another directory may require patching configuration files, otherwise it may not recognize the installed packages. -- Close the terminal and open a new Cygwin terminal to refresh the environment variables. Test if WODI was properly installed, by running a command such as ''godi_list''. - * WODI may complain about spaces in your ''PATH'' variable (make sure they do not occur in Cygwin/GODI/OCaml-related directories, or things may not work), but it should display a huge list of packages (with a few of them installed). -- Install packages zarith, lablgtk, and optionally ocamlgraph: <code>godi_add godi-zarith godi-lablgtk2 godi-ocamlgraph</code> - * This command may take a while and will not output anything if successful, other than a possible warning about spaces in your PATH variable. -- Download Frama-C's source release (tested with [[http://frama-c.com/download/frama-c-Sodium-20150201.tar.gz|Sodium]] and [[http://frama-c.com/download/frama-c-Magnesium-20151002.tar.gz|Magnesium]]) -- Using the Cygwin shell, uncompress Frama-C's sources, ''cd'' into it, and run configure as follows: <code>CC=x86_64-w64-mingw32-gcc configure --prefix="C:/path/to/final/framac"</code> - * Where ''path/to/final/framac'' is the directory where you want Frama-C to be installed. - * **Important**: this path **must** be written using a Windows-based path and **not** a Cygwin-based one such as '/home/user/framac'. Also, use forward slashes (''/'') instead of backslashes, otherwise Frama-C will install but not run properly. - * Use ''CC=i686-w64-mingw32-gcc'' instead if you're installing the 32-bit version. - * Here's an example command-line to install Frama-C to a local ''build'' directory: <code>CC=x86_64-w64-mingw32-gcc ./configure --prefix="$(cygpath -a -m $PWD)"/build</code> -- Check that the ''./configure'' script found the required dependencies (e.g. for the GUI). The GUI may be partially disabled if ''dot'' is not installed, but otherwise it should have detected lablgtk correctly. - * If you want the GUI and the callgraph to be fully enabled, install Cygwin package ''graphviz''. -- (Magnesium only) Frama-C Magnesium requires a patch to the ''Makefile'', otherwise the following error may occur: <code>[...] -``` - -Generating .depend /bin/sh: /opt/wodi64/bin/ocamldep.opt: Argument list -too long\</code\> - -``` - * This is the patch to be applied: [[https://bts.frama-c.com/dokuwiki/lib/exe/fetch.php?media=wiki:makefile-ocamldep-argument-too-long.patch|Makefile-ocamldep-argument-too-long.patch]] - * Download the patch file to your Frama-C source directory, and apply it using e.g.: <code>patch -i makefile-ocamldep-argument-too-long.patch</code> -- Run ''make'' using the special value for variable ''FRAMAC_TOP_SRCDIR'' below: <code>make FRAMAC_TOP_SRCDIR="$(cygpath -a -m $PWD)"</code> - * This will fix the path during execution of the Makefile, using a Windows-based absolute path instead of a Cygwin-based one. Without this fix, compilation will fail after some time (when compiling plugin files). - * Note that the first time ''make'' runs, it may emit some warnings about missing files such as the ones below, but this is normal and should not affect compilation: <code>C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: share/Makefile.kernel: No such file or directory -``` - -C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: -share/Makefile.kernel: No such file or directory -C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: -share/Makefile.kernel: No such file or directory -C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: -share/Makefile.kernel: No such file or directory -C:/cygwin64/home/user/frama-c-Magnesium-20151002/share/Makefile.dynamic:195: -share/Makefile.kernel: No such file or directory Makefile:2434: .depend: -No such file or directory\</code\> - -1. Get a coffee while waiting for Frama-C to compile, it may take a - while. -2. Run `make install`. Your Frama-C is now ready to be used\! - - If you installed Frama-C in a directory which is not in the - PATH, remember to prefix it with - `/path/to/installed_framac/bin/`. -3. Try parsing a simple program, e.g. `frama-c file.c` or - `frama-c-gui file.c`, to ensure that all necessary paths are - correct (such as `__fc_builtin_for_normalization.i`). - - You can also try one of Frama-C's tests, e.g. `frama-c-gui - tests/idct/*.c`. Note that the `tests/idct` contains a single - test split in two C files, but most other test directories - contain unit tests which should be run individually. Also note - that several tests do not constitute valid C programs. - -##### Note - -There is a Windows-specific issue in Frama-C Sodium/Magnesium that -prevents Windows absolute paths with backslashes from being correctly -parsed. In the command-line, you can use forward slashes (`frama-c -'C:/Temp/file.c'`) or double backslashes (`frama-c -'C:\\Temp\\file.c'`), but in the GUI you cannot load files using -absolute paths. There is however a patch in the OPAM-MinGW version of -Magnesium that fixes this issue. - -## Recommended versions to use - - - GNU make version \>= 3.81 - - Objective Caml \>= 4.02.3; - -<!-- end list --> - - - Gtk (\>= 2.4) - - GtkSourceView 2.x - - GnomeCanvas 2.x - - LablGtk \>= 2.18.3 - -<!-- end list --> - - - Frama-C Magnesium 20151002 - - Why3 0.86.2 - - Why 2.33 (for Jessie, need a tweak on Why: - <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2013-August/003714.html>) - - Coq 8.4 - - Alt-Ergo 0.99.1 - -Sources: - - - <http://frama-c.com/install-magnesium-20151002.html> - - <http://krakatoa.lri.fr/> - -# Older versions - -## Nitrogen - -### Compiling under Cygwin with Mingw, with Zarith - -The following is taken directly from Dillon Pariente's informative -message -<http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2011-October/002837.html> -. - -You might like to also have a look at -<http://blog.frama-c.com/index.php?post/2011/10/09/Zarith> and -<http://blog.frama-c.com/index.php?post/2011/10/17/Features-in-Nitrogen-1> -to check the advantages you can draw from using Zarith. - -The description for the Zarith library reads as follows: - -"The Zarith library implements arithmetic and logical operations over -arbitrary-precision integers. It uses GMP to efficiently implement -arithmetic over big integers. Small integers are represented as Caml -unboxed integers, for speed and space economy." - -It is available from <http://forge.ocamlcore.org/projects/zarith/> and -expected to improve performances up 50% in the best cases. - -What follow are some informal hints for the ones interested in using -this new experimental Zarith feature under Mingw (or Cygwin+Mingw). - -##### Requirements - -Prior to reproducing the steps below, check that you have the following - - - Ocaml's mingw port, version 3.12.0 or higher; - - flexlink (from <http://alain.frisch.fr/flexdll.html>); - - Zarith lib, whose last version one can obtain with a simple : - -<!-- end list --> - - <code>svn checkout svn://scm.ocamlcore.org/svn/zarith/trunk) </code> - * GMP for Mingw (see http://www.mingw.org/wiki/InstallationHOWTOforMinGW). Do not forget to remove any previous GMP installation coming with Cygwin to avoid using cygwin1.dll; - * and all other requirements expressed in Frama-C's INSTALL file. - -##### Zarith's configuration and compilation - -Now, configure and compile Zarith (under the zarith installation dir), -following the command lines below: - - export FLEXLINKFLAGS="-LX:/path/to/mingw/libraries" - - CPPFLAGS="-IX:/path/to/mingw/includes -IX:/path/to/ocaml_mingw_port/includes -D__MINGW32__ -mno-cygwin" ./configure --installdir X:/path/to/ocaml_mingw_port/libraries - - make clean && make depend && make - make test && ./test - # to check whether zarith compilation is OK! - - make install - -If the last command does not work properly, due to .so/.dll mismatch ... -then try instead: - - ocamlfind install -destdir X:/path/to/ocaml_mingw/libraries zarith META zarith.cma libzarith.a z.mli q.mli big_int_Z.mli z.cmi q.cmi big_int_Z.cmi zarith.a zarith.cmxa zarith.cmxs dllzarith.dll - -##### Compiling Frama-C with Zarith support - -Now, you can define some required environment variables: - - export HAS_ZARITH=yes - export ZARITH_INC="-I X:/path/to/ocaml_mingw/libraries/zarith/" - -And compile Frama-C (go to the Frama-C dir) ... as usual: - - ./configure ... - make && make install - -The instructions below refer to previous versions of Frama-C, and may -not apply to the most current one. If you succeed in compiling a more -recent version than the one for which the instructions were originally -written, do not hesitate to update this page. - -## Beryllium installation - -#### Compiling Beryllium for Mac OS X - -To compile Frama-C for Mac OS X Leopard yourself, see [this -message](http://lists.gforge.inria.fr/pipermail/frama-c-discuss/2009-September/001390.html). - -#### Compiling Beryllium for FreeBSD - -To compile Frama-C on FreeBSD, use `env MAKE=gmake bash ./configure -CFLAGS="-I/usr/local/include" LDFLAGS="-L/usr/local/lib" && gmake` - -#### Compiling the Jessie plugin coming with Why 2.22 under Windows? - -``` - - Install the Windows binary 20090902 Beryllium Frama-C version - - Set the following environment variables (using the Windows Control Panel): - * prepend ''C:\Frama-C\bin'' to ''PATH'' - * set ''OCAMLLIB'' to ''C:\Frama-C\lib'' - * set ''CAML_LD_LIBRARY_PATH'' to ''C:\Frama-C\lib\stublibs'' \\ Replace ''C:\Frama-C'' by your installation path if you customized it. - - Install a Cygwin version (1.7 beta has been verified to work) with at least the ''gcc-mingw'' and ''autoconf'' packages - - If ''C:\Cygwin\bin\gcc.exe'' is a symbolic link, remove it and replace it by its full expansion e.g. ''gcc-3.exe'' under Cygwin 1.7 beta. - - Download the source tar.gz of Why 2.22 - - untar it in your cygwin home directory - - configure it with ''./configure --prefix C:/Frama-C'' (forward slash must be used!) - - compile it with ''make'' - - install it with ''make FRAMAC_LIBDIR="C:\\\Frama-C\\\lib\\\frama-c" install'' (triple backward slashes must be used!) - - then proceed to the installation of provers -``` diff --git a/dokuwiki/start.md b/dokuwiki/start.md index 4766fa9ec4549b3a4cf38624a241ea1b2f9e8d20..f962278cda7acc264842888f8ac53fdf167d0134 100755 --- a/dokuwiki/start.md +++ b/dokuwiki/start.md @@ -1,63 +1,80 @@ --- layout: clean_page --- -# Welcome to the Frama-C Wiki. - -Is on-topic in this wiki anything that may be of help to others users of -Frama-C and related tools: tips, changes that you have noticed, -workarounds, etc. If it should have been in the manual, put it here. If -it's too minute, platform-specific, or temporary to be a good fit for -the manual, put it here. Your goal should be to make a wiki so clear and -functional that it puts the authors of Frama-C's various manuals to -shame. - -Do not be afraid to reorganize the words of others if you feel that -makes the wiki more useful as a whole. They agreed to let you do that -when they chose to participate, and so do you. - -To edit the wiki, you can submit a merge request on the corresponding gitlab repository [](insert link). - -For plug-ins documentation, some pages can be found here but all of them are otherwise available [/html/kernel-plugin.html](on the dedicated page). - ------ - -# Compilation and Installation - -Current and old releases of Frama-C are available on [this -page](http://frama-c.com/download.html). It contains the official -installation instructions for supported systems. - -Otherwise, [this Frama-C wiki -page](/dokuwiki/compiling_from_source.html) contains extra instructions -for compiling from source on non-supported platforms. It also contains -instructions for compiling older releases. - -# FAQ, Tips and Tricks - -See [this page](/dokuwiki/faq.html), or this [slightly older -one](/dokuwiki/frequently_asked_questions.html). - -# External plug-ins - -[External plug-ins](/dokuwiki/external_plugins.html) that you may find -useful are available. The plug-ins currently described are **Jessie**, -**Celia** and **Werror**. - -# Known issues - - - The BTS has a [list of known - issues](http://bts.frama-c.com/view_all_bug_page.php). - - See [bug reporting guidelines](/dokuwiki/bug_reporting_guidelines.html) to - report a bug. - -# Open positions - -[Open positions](/dokuwiki/positions.html) in the Frama-C team are -available. - -# Works about Frama-C - - - [List of publications](/dokuwiki/publications.html) - - [Exercises](/dokuwiki/exercises.html) - - [Teaching](/dokuwiki/teaching.html) - - [Tutorials](/dokuwiki/tutorial.html) +# Documentation + +<!-- Is on-topic in this wiki anything that may be of help to others users of --> +<!-- Frama-C and related tools: tips, changes that you have noticed, --> +<!-- workarounds, etc. If it should have been in the manual, put it here. If --> +<!-- it's too minute, platform-specific, or temporary to be a good fit for --> +<!-- the manual, put it here. Your goal should be to make a wiki so clear and --> +<!-- functional that it puts the authors of Frama-C's various manuals to --> +<!-- shame. --> + +Modification for this documentation, as for all this site, can be proposed by +submitting a merge requests at the corresponding +[https://git.frama-c.com/frama-c/frama-c.frama-c.com](gitlab repository). + +For plug-ins documentation, some pages can be found here but all of them are +otherwise available [/html/kernel-plugin.html](on the dedicated page). + +Is on-topic anything that may be of help to others users of +Frama-C and related tools: tips, changes that you have noticed, +workarounds, etc. + +<!-- If it should have been in the manual, put it here. If --> +<!-- it's too minute, platform-specific, or temporary to be a good fit for --> +<!-- the manual, put it here. Your goal should be to make a wiki so clear and --> +<!-- functional that it puts the authors of Frama-C's various manuals to --> +<!-- shame. --> + +----- + +# Compilation and Installation + +Current and old releases of Frama-C are available on [this +page](html/get-frama-c.html). It contains the official +installation instructions for supported systems. + +Otherwise, [each releases](https://git.frama-c.com/pub/frama-c/blob/master/INSTALL.md) contains extra instructions +for compiling from source. + +<!-- We could copy INSTALL.md to this repo --> + +# Contributing + +Frama-C is an open-source project which could be contrinuted through merge +requests at this [Gitlab repository](https://git.frama-c.com/pub/frama-c/). The +modalities are described in this [document](https://git.frama-c.com/pub/frama-c/CONTRIBUTING.md) + +<!-- We could copy CONTRIBUTING.md to this repo --> + +# FAQ, Tips and Tricks + +See [this page](/dokuwiki/faq.html), or this [slightly older +one](/dokuwiki/frequently_asked_questions.html). + +# External plug-ins + +[External plug-ins](/dokuwiki/external_plugins.html) that you may find +useful are available. The plug-ins currently described are **Jessie**, +**Celia** and **Werror**. + +# Known issues + + - The BTS has a [list of known + issues](http://bts.frama-c.com/view_all_bug_page.php). + - See [bug reporting guidelines](/dokuwiki/bug_reporting_guidelines.html) to + report a bug. + +# Open positions + +[Open positions](/dokuwiki/positions.html) in the Frama-C team are +available. + +# Works about Frama-C + + - [List of publications](/dokuwiki/publications.html) + - [Exercises](/dokuwiki/exercises.html) + - [Teaching](/dokuwiki/teaching.html) + - [Tutorials](/dokuwiki/tutorial.html)