Skip to content
Snippets Groups Projects
Commit 5749db8f authored by Andre Maroneze's avatar Andre Maroneze
Browse files

[doc] update links, fix typos, rewrite some parts

parent 68f16977
No related branches found
No related tags found
No related merge requests found
......@@ -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.
......
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment