From 5749db8fead95329dd020b1f6536cf6bc6ff79e5 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Wed, 22 Nov 2023 17:17:53 +0100
Subject: [PATCH] [doc] update links, fix typos, rewrite some parts
---
CONTRIBUTING.md | 30 +++++++++++++++++-------------
README.md | 24 +++++++++++++-----------
2 files changed, 30 insertions(+), 24 deletions(-)
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
index 2129a56a417..f48ad700d31 100644
--- a/CONTRIBUTING.md
+++ b/CONTRIBUTING.md
@@ -19,7 +19,7 @@ There are several ways to participate in the Frama-C project:
- [Developing external plug-ins](#developing-external-plug-ins)
and sharing it with us through a Gitlab merge request;
-- Joining the [Frama-C team](https://frama-c.com/about.html) (as an intern, a PhD
+- [Joining the Frama-C team](https://frama-c.com/html/jobs.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
@@ -35,6 +35,10 @@ 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
@@ -44,7 +48,7 @@ The detailed steps to submit a contribution to Frama-C are:
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;
+3. Clone the forked Frama-C repository on your computer;
4. Create and switch to a dedicated branch. We suggest the following
naming convention:
@@ -70,33 +74,33 @@ The detailed steps to submit a contribution to Frama-C are:
problems if any.
Use the command `make check-headers` in your terminal from the Frama-C root
- directory to detect bad file license (headache is needed), and `make headers`
- to fix them.
+ directory to detect incorrect file licenses (the `headache` opam package is
+ needed), and `make headers` to fix them.
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);
+ in your terminal (you should be in the Frama-C root directory).
-9. Locally add (if needed) and commit your contribution;
+9. Locally add (if needed) and commit your contribution.
-10. Push your contribution to Gitlab;
+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`
+12. If needed (i.e. it is your first non-trivial contribution in the sense of
+ [this document](TCA.md)), please do not 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 add <file1 file2 ...>
git commit -m "<Commit message>"
git push origin <branch-name>
```
@@ -104,7 +108,7 @@ where:
- `<username>` is your Gitlab username;
- `<branch-name>` is your chosen branch name;
-- `<file1 file2>` are the files to add to the commit;
+- `<file1 file2 ...>` are the files to add to the commit;
- `<Commit message>` is your commit message.
diff --git a/README.md b/README.md
index 667cd216995..910828b3be1 100644
--- a/README.md
+++ b/README.md
@@ -32,7 +32,7 @@ OCaml package manager. If you have it, simply run:
opam install frama-c
-or, for `opam` versions less than 2.1.0:
+or, for `opam` versions less than 2.1:
opam install depext # handles external (non-OCaml) dependencies
opam depext frama-c --install
@@ -70,11 +70,13 @@ Frama-C can be run from the command-line, or via its graphical interface.
The recommended usage for simple files is one of the following lines:
frama-c file.c -<plugin> [options]
- frama-c-gui file.c
+ ivette file.c -<plugin> [options]
Where `-<plugin>` is one of the several Frama-C plug-ins,
e.g. `-eva`, or `-wp`, or `-metrics`, etc.
-Plug-ins can also be run directly from the GUI.
+Plug-ins can also be run directly from the graphical interface,
+`ivette`.
+A legacy version of the GUI (`frama-c-gui`) is also available.
To list all plug-ins, run:
@@ -91,23 +93,23 @@ is available through
#### Complex scenarios
-For more complex usage scenarios (lots of files and directories,
-with several preprocessing directives), we recommend splitting Frama-C's usage
-in two parts:
+For complex usage scenarios (several files and directories,
+preprocessing directives, etc), we recommend the following two-step approach:
1. Parsing the input files and saving the result to a file;
2. Loading the parsing results and then running the analyses or the GUI.
-Parsing typically involves giving extra arguments to the C preprocessor,
-so the `-cpp-extra-args` option is often useful, as in the example below:
+Parsing complex C applications usually involves C preprocessor options
+(e.g. GCC's `-D` and `-I`).
+In Frama-C, they are passed via option `-cpp-extra-args`, as in this example:
- frama-c *.c *.h -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
+ frama-c *.c -cpp-extra-args="-D<define> -I<include>" -save parsed.sav
-The results are then loaded into Frama-C for further analyses or for inspection
+The results can then be loaded into Frama-C for further analyses or for inspection
via the GUI:
frama-c -load parsed.sav -<plugin> [options]
- frama-c-gui -load parsed.sav -<plugin> [options]
+ ivette -load parsed.sav -<plugin> [options]
## Further reference
--
GitLab