diff --git a/.gitlab/issue_templates/bug_report.md b/.gitlab/issue_templates/bug_report.md new file mode 100644 index 0000000000000000000000000000000000000000..b01c0a798eea16182a8c10988dd03d4c870a5e32 --- /dev/null +++ b/.gitlab/issue_templates/bug_report.md @@ -0,0 +1,35 @@ +Thank you for submitting an issue to the Frama-C team. +We propose the following template to ease the process. +Please directly edit it inline to provide the required information. + +Before submitting the issue, please confirm (by adding a X in the [ ]): + +- [ ] the issue has not yet been reported on [Gitlab](https://git.frama-c.com/pub/frama-c/issues); +- [ ] the issue has not yet been reported on our [BTS](https://bts.frama-c.com); +- [ ] you installed Frama-C as prescribed in the [instructions](INSTALL.md). + +# Contextual information + +- Frama-C installation mode: *Opam, Homebrew, package from distribution, from source, ...* +- Frama-C version: *Frama-C version* (as reported by `frama-c -version`) +- Plug-in used: *Plug-in used* +- OS name: *OS name* +- OS version: *OS version* + +*Please add specific information deemed relevant with regard to this issue.* + +# Steps to reproduce the issue + +*Please indicate here steps to follow to get a [minimal, complete, and verifiable example](https://stackoverflow.com/help/mcve) which reproduces the issue.* + +# Expected behaviour + +*Please explain here what is the expected behaviour.* + +# Actual behaviour + +*Please explain here what is the actual (faulty) behaviour.* + +# Fix ideas + +*Please tell us if you already tried some work-arounds or have some ideas to solve this issue.* diff --git a/.gitlab/merge_request_templates/external_contribution.md b/.gitlab/merge_request_templates/external_contribution.md new file mode 100644 index 0000000000000000000000000000000000000000..e7586d07962708f8e7abec8c04a7f8223a3291f7 --- /dev/null +++ b/.gitlab/merge_request_templates/external_contribution.md @@ -0,0 +1,9 @@ +Thank you for submitting a merge request to the Frama-C team. +We propose the following template to ease the process. +Please directly edit it inline to provide the required information. + +Before submitting the merge request, please confirm (by adding a X in the [ ]): + +- [ ] you contributed to Frama-C as prescribed in the [instructions](CONTRIBUTING.md). +- [ ] if the size of the PR requires it, you have signed the + [Contributor Licensing Agreement](CLA.md) diff --git a/CLA.md b/CLA.md new file mode 100644 index 0000000000000000000000000000000000000000..7ecfa70238427e38c1f86c7fba9a3744c2d428cb --- /dev/null +++ b/CLA.md @@ -0,0 +1,234 @@ +--- +geometry: +- top=15mm +- bottom=15mm +- margin=10mm +--- +Contributor Agreement +===================== + +Thank you for your interest in contributing to Frama-C, distributed by +the Commissariat à l'Energie Atomique et aux Energies Alternatives +(\"We\" or \"Us\"). + +The purpose of this Contributor Non-Exclusive License Agreement +(\"Agreement\") is to clarify and document the rights granted by +contributors to Us. To make this document effective and get started, +please sign the Contributor License Agreement. + +Please read this document carefully before signing and keep a copy for +your records. + +**1. DEFINITIONS** + +**\"You\" (/"Your")** means the Individual Copyright owner or Entity as +defined hereunder who submits a Contribution to Us. If You are an +employee and submit the Contribution as part of your employment, You +represent that you have the authority and/or required authorization in +binding the Entity to this Agreement, and to sign this version of this +document. In such case "You" (/"Yours") shall refer to such Entity. + +**\"Documentation\"** means any non-software portion of a Contribution. + +**"Entity"** shall mean the copyright owner or legal entity (including +but not limited to any institution, company, corporation, partnership, +government agency or university) authorized by the copyright owner that +is making this Agreement with Us and all other entities that control, +are controlled by, or are under common control with that entity are +considered to be a single Contributor. For the purposes of this +definition, \"control\" means (i) the power, direct or indirect, to +cause the direction or management of such entity, whether by contract or +otherwise, or (ii) ownership of fifty percent (50%) or more of the +outstanding shares, or (iii) beneficial ownership of such entity. + +**\"Contribution\"** means any original work of authorship (software +and/or documentation) including any modifications or additions to an +existing work, Submitted by You to Us, in which You own the Copyright. + +**\"Copyright\"** means all rights protecting works of authorship owned +or controlled by You, including copyright, moral and neighboring rights, +as appropriate, for the full term of their existence including any +extensions by You. + +**\"Submit\"** means any form of physical, electronic, or written +communication sent to Us, including but not limited to electronic +mailing, source code control systems, and issue tracking systems that +are managed by, or on behalf of, Us, but excluding communication that is +clearly designated in writing by You as \"Not a Contribution.\" + +\"**Work**\" means any software or documentation made available by Us to +third parties. Any Contribution You Submit may be included in the +Material. + +**2. GRANT OF LICENSE** + +> **2.1 Grant of Copyright License.** + +Subject to the terms and conditions of this Agreement, You hereby grant +to Us a worldwide, royalty-free, no-charge, non-exclusive, perpetual and +irrevocable Copyright license, with the right to transfer an unlimited +number of non-exclusive licenses or to grant non-exclusive sublicenses +to third parties, to use the Contribution by all means, including but +not limited to, the right to : + +- Publish the Contribution in original or modified form ; + +- Modify the Contribution, prepare derivative works based upon or + containing the Contribution and combine the Contribution with other + works; + +- Reproduce the Contribution in original or modified form; + +- Distribute, make the Contribution available to the public, display + and publicly perform the Contribution in original or modified form + under the terms of any license approved by Us. + +> **2.2 Moral Rights** + +Moral Rights remain unaffected to the extent they are recognized and not +waivable by applicable law. Notwithstanding, You may add your name in +the header of the source code files of Your Contribution and We will +respect this attribution when using Your Contribution. + +**3. GRANT OF PATENT LICENSE** + +Subject to the terms and conditions of this Agreement, You hereby grant +to Us a perpetual, worldwide, non-exclusive, no-charge, royalty-free, +irrevocable patent license, with the right to transfer an unlimited +number of non-exclusive licenses or to grant sublicenses to third +parties, to make, have made, use, offer to sell, sell, import, and +otherwise transfer the Contribution, where such license applies only to +those patent claims licensable by You that are necessarily infringed by +Your Contribution(s) alone or by combination of Your Contribution(s) +with the Work to which such Contribution(s) was submitted. + +This license applies to all patents owned or controlled by You, whether +already acquired or hereafter acquired, that would be infringed by +making, having made, using, selling, offering for sale, importing or +otherwise transferring of Your Contribution(s) alone or by combination +of Your Contribution(s) with the Material. + +You furthermore agree to notify Us of any patents that you know or come +to know which are likely infringed by the Contribution and/or are not +licensable by You. + +If any entity institutes patent litigation against You or any other +entity alleging that the Contribution, or the Work with which it has +been combined, constitutes direct or contributory patent infringement, +then any patent licenses granted to that entity under this Agreement for +that Contribution or Material shall terminate as of the date such +litigation is filed. + +If the litigation is withdrawn or otherwise settled, then any patent +licenses granted to that entity under this agreement shall be reinstated +as of the date the litigation was settled or withdrawn. + +**4. REPRESENTATIONS** + +a\. If You are entering this Agreement as an individual, You represent +that You are legally entitled to grant the licenses set forth in +Sections 2 and 3. If Your employer(s) has rights to intellectual +property that You create, such as your Contributions, You represent that +You have received permission to make Contributions on behalf of that +employer and that Your employer has waived such rights for Your +Contributions to the Work. + +b\. If You are entering this Agreement on behalf of an Entity, You +represent that You are legally entitled to grant the licenses set forth +in Sections 2 and 3 and that each employee of the Entity that submits +Contributions is authorized to submit such Contributions on behalf of +the Entity. + +In any case, You represent that: + +i\. The Contribution is Your original creation. If You do not, entirely +or partially, own the Copyright in work of authorship comprising a +Contribution, please contact Us before Submitting such Contribution. + +ii\. to the extent that Your Contribution is computer code, it includes +complete details of any third-party license or other restriction +(including, but not limited to, related patents and trademarks) of which +You are personally aware and which are associated with any part of Your +Contributions. + +iii\. to the extent that Your Contribution is computer code, it contains +no viruses, Trojan horses, backdoors, malicious code or other program +that would allow anyone, including Us, to gain access to a computer or +network other than what is fully documented and disclosed by Us. + +**5. DISCLAIMER OF WARRANTIES** + +Except as set forth in section 4, the contribution is provided \"as +is\". More particularly, all express or implied warranties including, +without limitation, any implied warranty of merchantability, fitness for +a particular purpose and non-infringement are expressly disclaimed by +You to Us and by Us to You. To the extent that any such warranties +cannot be disclaimed, such warranty is limited in duration to the +minimum period permitted by law. + +**6. CONSEQUENTIAL, APPROXIMATION OF DISCLAIMER AND DAMAGE WAIVER** + +To the maximum extent permitted by applicable law, in no event will You +or Us be liable for any loss of profits, loss of anticipated savings, +loss of data, indirect, special, incidental, consequential and exemplary +damages arising out of this Agreement regardless of the legal or +equitable theory (contract, tort or otherwise) upon which the claim is +based. + +If the disclaimer and damage waiver mentioned in section 5 and section 6 +cannot be given legal effect under applicable local law, reviewing +courts shall apply local law that most closely approximates an absolute +waiver of all civil liability in connection with the contribution. + +**7. TERM** + +This Agreement shall come into effect upon Your acceptance of the terms +and conditions. + +In the event of a termination of this Agreement Sections 5, 6 and 8 +shall survive such termination and shall remain in full force +thereafter. For the avoidance of doubt, Contributions that are already +licensed under a free and open source license at the date of the +termination shall remain in full force after the termination of this +Agreement. + +**8. MISCELLANEOUS** + +8.1 You are not expected to provide support for Your Contributions, +except to the extent You desire to provide support. You may provide +support for free, for a fee, or not at all. Unless required by +applicable law or agreed to in writing, You provide Your Contributions +on an \"as is\" basis, without warranties or conditions of any kind, +either express or implied, including, without limitation, any warranties +or conditions of title, non-infringement, merchantability, or fitness +for a particular purpose. + +8.2 This Agreement and all disputes, claims, actions, suits or other +proceedings arising out of this agreement or relating in any way to it +shall be governed by the laws of France excluding its private +international law provisions. + +8.3 This Agreement sets out the entire agreement between You and Us for +Your Contributions to Us and overrides all other agreements or +understandings. + +8.4 If any provision of this Agreement is found void and unenforceable, +such provision will be replaced to the extent possible with a provision +that comes closest to the meaning of the original provision and that is +enforceable. The terms and conditions set forth in this Agreement shall +apply notwithstanding any failure of essential purpose of this Agreement +or any limited remedy to the maximum extent possible under law. + +8.5 You agree to notify Us of any facts or circumstances of which you +become aware that would make this Agreement inaccurate in any respect. + +**Signature** + +- Full Name: +- Entity (if applicable): +- Country/Town: +- (optional) Full address: +- Email: +- Gitlab login: +- Date: +- Signature: diff --git a/CLA.pdf b/CLA.pdf new file mode 100644 index 0000000000000000000000000000000000000000..c3435b49a207be715c8a67b45c2d28eec39c2e37 Binary files /dev/null and b/CLA.pdf differ diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md new file mode 100644 index 0000000000000000000000000000000000000000..5c3a674ee5aca48c0a5f864812cad2aafe461e0b --- /dev/null +++ b/CONTRIBUTING.md @@ -0,0 +1,152 @@ +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: + +- Asking questions and discussing at + [StackOverflow](https://stackoverflow.com/tags/frama-c) and through + the + [Frama-C-discuss mailing list](https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss); + +- Reporting bugs via + [Gitlab issues](https://git.frama-c.com/pub/frama-c/issues); + +- [Submitting bug fixes, improvements and features](#submitting-bug-fixes-improvements-and-features) + via Gitlab merge requests; + +- [Developing external plug-ins](#developing-external-plug-ins) + and sharing it with us through a Gitlab merge request; + +- Joining the [Frama-C team](http://frama-c.com/about.html) (as an intern, a PhD + student, a postdoctoral researcher, or a research engineer). + +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](https://git.frama-c.com/pub/frama-c), +by following the recommended workflow in git development: +fork the frama-c repository, develop in a dedicated branch +and submit a merge request. + +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](https://git.frama-c.com/pub/frama-c/issues/new) + describing your ideas, to discuss it with the Frama-C development team. + +2. [Fork the public Frama-C repository](https://git.frama-c.com/pub/frama-c/-/forks/new) + (choosing your Gitlab account as a destination); + +3. Clone the forked Frama-C snapshot 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](#coding-conventions); + +6. (Optional) Locally add non-regression test cases to the appropriate + subdirectory in `./tests/`. The `hello` tutorial in the + [plug-in developer manual](http://frama-c.com/download/frama-c-plugin-development-guide.pdf) + provides an example of the use of the dedicated `ptests` + tool used by Frama-C developers. The full documentation for `ptests` is also + present later in the same manual. + 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 lint` + in your terminal from the Frama-C root directory to detect trailing spaces, + tabulations or incorrect indentation (ocp-ident >= 1.7.0 is needed). + +8. Locally run the test framework of Frama-C by typing + `make tests` + in your terminal (you should be in the Frama-C root directory); + +9. Locally add (if needed) and commit your contribution; + +10. Push your contribution to Gitlab; + +11. [Make a Gitlab merge request](https://git.frama-c.com/pub/frama-c/merge_requests). + 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. + +12. If needed (i.e. you didn't already do that and your contribution is + not trivial in the sense of [this document](TCA.md)), please don't forget + to fill and sign the [Contributor Licence Agreement](CLA.pdf) 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: +```shell +git clone https://git.frama-c.com/<username>/frama-c.git +git checkout -b <branch-name> +git diff --check +git add <file1 file 2> +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](http://frama-c.com/download/frama-c-plugin-development-guide.pdf). +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 as exemplified by the [Hello plug-in](https://github.com/Frama-C/frama-c-hello). + +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](http://frama-c.com/download/frama-c-plugin-development-guide.pdf); + +2. Create an `opam` package by + [pinning your local plug-in](http://opam.ocaml.org/doc/Packaging.html#Opam-pin) and + [editing the `opam` file](http://opam.ocaml.org/doc/Packaging.html#The-quot-opam-quot-file). + You can have a look at the + [`opam` file of the Hello plug-in](https://github.com/Frama-C/frama-c-hello/blob/master/opam) + if necessary. + +3. Optionally + [publish your plug-in](http://opam.ocaml.org/doc/Packaging.html#Publishing) + in the official OPAM packages repository. + +4. Announce your contribution to the Frama-C ecosystem on the + [Frama-C-discuss mailing list](https://lists.gforge.inria.fr/mailman/listinfo/frama-c-discuss). + 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](https://github.com/OCamlPro/ocp-indent), v1.7.0 + to indent OCaml source files; + +- Avoid trailing whitespaces; + +- Avoid using tabs; + +- Strive to keep within 80 characters per line. diff --git a/TCA.md b/TCA.md new file mode 100644 index 0000000000000000000000000000000000000000..7c28ab8e534241bbb31c4c73657a7b2ee189b0b0 --- /dev/null +++ b/TCA.md @@ -0,0 +1,78 @@ +**Trivial Contribution Policy** + +The purpose of this Policy is to clarify and document the circumstances +in which a Contribution, deemed as Trivial, does not fall within the +scope of the Contributor License Agreement. + +As a general rule, Contributions that do not involve creative decisions +or which are not substantial will be considered to be Trivial. + +As a guideline, a Contribution may be qualified according to the +following: + ++-----------------------+-----------------------+-----------------------+ +| *Type of | *≤ 10 lines* | *\> 10 lines* | +| contribution* | | | ++=======================+=======================+=======================+ +| Feature | | | +| | • Not trivial | • Not trivial | +| (add new functional | | | +| behavior) | | | ++-----------------------+-----------------------+-----------------------+ +| Improvement | | | +| | • Probably | • Not trivial | +| (improve | not trivial | | +| non-functional | | | +| behavior) | | | ++-----------------------+-----------------------+-----------------------+ +| | • Not trivial if | • Not trivial if | +| | creative code | creative code | +| Bug fix | | | +| | • Not trivial if | • Not trivial if | +| (fix incorrect | comprises a creative | comprises a creative | +| behavior) | comment | comment | +| | | | +| | • Probably trivial | • Probably not | +| | otherwise | trivial otherwise | ++-----------------------+-----------------------+-----------------------+ + +(1) - - - + +<!-- --> + +(1) + +Without prejudice to the above, and for all intents and purposes, the +following Contributions are deemed to be Trivial: + +- Spelling / grammar fixes / correcting typos + +- Formatting / cleaning up comments in the code. + +- Contributions that are purely deletions, such as removal of + duplicate information or code that never executes. + +- Bug fixes that change default return values or error codes stored in + constants, literals, or simple variable types. + +- Adding logging messages or debugging output. + +- Changes to 'metadata' files. + +- Renaming a build directory or changing a constant. + +- Configuration changes. + +- Changes in build or installation scripts. + +- Re-ordering of objects or subroutines. + +- Moving source files from one directory or package to another, with + no changes in code. + +- Breaking a source file into multiple source files, or consolidating + multiple source files into one source file, with no code changes. + +However, there are many gray areas. Please reach us at `cla AT frama-c DOT com` +should you have any questions on the nature of your +intended Contribution.