Home
Welcome to the sonar-frama-c-plugin wiki!
Sonar-frama-c-plugin is a SonarQube plugin integrating frama-c results into SonarQube dashboard.
Required : git, Java 8 and maven 3.5.0 (or latest)
- Clone github repository :
git clone https://github.com/lequal/sonar-frama-c-plugin.git - Build using maven from the project directory :
mvn clean install - The generated plugin can be found into the target directory
(<sonar-frama-c-plugin_dir>/target)
- Copy the generated jar into
<SonarQube_installation_directory>/extensions/plugins. - Restart SonarQube :
sonar restartorservice sonar restart - Check SonarQube logs :
tail -f <SonarQube_installation_directory>/logs/web.log
- Open SonarQube web interfaces
http://<SonarQube_installation_host_ip>:9000orhttp://localhost:9000if your are on the host machine - Select "FramaC Quality Profile" and add selected Frama-c rules to the Profile.
For all project source files, run:frama-c -val ./<source_file.c> -report-csv ./<report_dir>/result.csv 2>&1 > ./<report_dir>/result.out
Where:
- The parameter
-valor-evaproduces a Frama-C value analysis - The source files
<source_file.c>shall have for extension .c or .i - The sub-directory
<report_dir>is used to store Frama-C stdout stream
In your project directory, create sonar-project.properties file, containing the following items :
sonar.projectKey=<your project key>
sonar.projectName=<your project name>
sonar.projectVersion= <your project version>
# Comma-separated paths to directories with sources (required)
sonar.sources=.
# Tells SonarQube where the frama-C analysis reports are
sonar.framac.reportsPath=<report_dir>
# Encoding of the source files
sonar.sourceEncoding=UTF-8Once you got frama-c results and sonar-project.properties configured, you can launch sonar scanner from you project directory : sonar-scanner
sonar-frama-c-plugin analyses frama-c text output and extracts the following rule's violations, defined by pattern. Complete explanation on the results are available from frama-c.
| Rule id | Pattern |
|---|---|
| Frama-C error | This rule is not directly linked to a problem in the code, but it exists to alert users that an error occurred when running Frama-C or reading Frama-C reports. |
| Unreferenced value rule | Unreferenced value rule |
| Division by zero | Integer division by zero |
| Mem access | Invalid pointer dereferencing |
| Index bound | Array access out of bounds |
| Shift | Invalid shift |
| Ptr comparison | Invalid pointer comparison |
| Differing blocks | Operation on pointers within different blocks |
| Separation | Unsequenced side-effects on non-separated memory |
| Overlap | Overlap between left- and right-hand-side in assignment |
| Initialization | Uninitialized memory read |
| Dangling pointer | Read of a dangling pointer |
| Is nan or infinite | Non-finite (nan or infinite) floating-point value |
| Is nan | NaN floating-point value |
| Float to int | Overflow in float to int conversion |
| Function pointer | Pointer to a function with non-compatible type |
| initialization of union | Uninitialized memory read of union |
| signed overflow | Integer overflow |
| unsigned overflow | Unsigned integer overflow |
| signed downcast | Integer downcast |
| unsigned downcast | Unsigned integer downcast |
| User assertion | ACSL User assertion |
| Assigns clause | ACSL Assigns clause |
| From clause | ACSL From clause |
You can contribute to sonar-frama-c-plugin :
- following the defined CODE_OF_CONDUCT
- using the PULL_REQUEST_TEMPLATE
- using the ISSUE_TEMPLATE
Contact : L-lequal@cnes.fr
Bugs and Feature requests : https://github.com/lequal/sonar-frama-c-plugin/issues
sonar-frama-c-plugin is under GNU GPL v3.