Skip to content

Latest commit

 

History

History
165 lines (122 loc) · 6.52 KB

CONTRIBUTING.md

File metadata and controls

165 lines (122 loc) · 6.52 KB
Raw

Contributing to Frama-C

We always welcome technical as well as non-technical contributions from the community. There are several ways to participate in the Frama-C project:

We give below some guidelines in order to ease the submission of a merge request and optimize its integration with the Frama-C existing codebase.

Submitting bug fixes, improvements, and features

External contributions can be proposed via the public Frama-C gitlab repository, by following the recommended workflow in git development: fork the frama-c repository, develop in a dedicated branch and submit a merge request.

Note: these steps assume that you have an account in Frama-C's Gitlab instance. This can be done by signing in via Github (which, in turn, requires a Github account; if you do not have a Github account, please contact us by e-mail).

The detailed steps to submit a contribution to Frama-C are:

  1. If you plan to make a significant contribution to Frama-C, please open an issue describing your ideas, to discuss it with the Frama-C development team.

  2. Fork the public Frama-C repository (choosing your Gitlab account as a destination);

  3. Clone the forked Frama-C repository on your computer;

  4. Create and switch to a dedicated branch. We suggest the following naming convention:

    • fix/short-description for bug fixes (correcting an incorrect behavior);
    • feature/short-description for features (adding a new behavior).

  5. Locally make your contribution by adding/editing/deleting files and following the coding conventions;

  6. (Optional) Locally add non-regression test cases to the appropriate subdirectory in ./tests/ or ./src/plugins/<plugin>/tests/. Consult the plug-in developer manual for details on how to run tests inside Frama-C. You can also provide the non-regression test case in the Gitlab issue discussion and we will integrate it.

  7. Check for unexpected changes. Use the command make check-lint in your terminal from the Frama-C root directory to detect trailing spaces, tabulations or incorrect indentation (ocp-indent = 1.8.1, camomile, clang-format and black (Python linter) are needed), and make lint to fix problems if any.

Use the command make check-headers in your terminal from the Frama-C root directory to detect incorrect file licenses (the headache opam package is needed), and make headers to fix them.

  1. Locally run the test framework of Frama-C by typing make default-tests in your terminal (you should be in the Frama-C root directory).

  2. Locally add (if needed) and commit your contribution.

  3. Push your contribution to Gitlab.

  4. Make a Gitlab merge request. The target should remain as repository pub/frama-c and branch master while the source should be your personal project and your chosen branch name.

  5. If needed (i.e. it is your first non-trivial contribution in the sense of this document), please do not forget to fill and sign the Contributor Licence Agreement and send us the signed version at cla AT frama-c DOT com.

For convenience, we recall the typical git commands to be used through these steps:

git clone https://git.frama-c.com/<username>/frama-c.git
git checkout -b <branch-name>
git diff --check
git add <file1 file2 ...>
git commit -m "<Commit message>"
git push origin <branch-name>

where:

  • <username> is your Gitlab username;
  • <branch-name> is your chosen branch name;
  • <file1 file2 ...> are the files to add to the commit;
  • <Commit message> is your commit message.

Developing external plug-ins

Frama-C is a modular platform for which it is possible to develop external plug-ins as documented in the Plug-In development guide. Such plug-ins normally do not require changes to the Frama-C source code and can be developed completely independently, for instance in a separate Git repository.

However, to make it easier for your users to compile and use your plug-in, even as newer releases are made available, we recommend the following workflow:

  1. Write your external plug-in as indicated in the Plug-In development guide;

  2. Create an opam package by pinning your local plug-in and editing the opam file. You can have a look at the opam file of the Hello plug-in if necessary.

  3. Optionally publish your plug-in in the official OPAM packages repository.

  4. Announce your contribution to the Frama-C ecosystem on the Frama-C-discuss mailing list. Well done!

The main advantage of this procedure is that opam will perform several consistency checks of your plug-in, with respect to several Frama-C versions and OCaml dependencies.

Coding conventions

  • Use ocp-indent, v1.8.1 to indent OCaml source files (available from opam);

  • Use black to indent Python source files;

  • Use clang-format to indent C files (mostly for E-ACSL, and possibly tests);

  • Avoid trailing whitespaces;

  • Avoid using tabs;

  • Strive to keep within 80 characters per line.