-
Notifications
You must be signed in to change notification settings - Fork 6
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 restart
orservice sonar restart
- Check SonarQube logs :
tail -f <SonarQube_installation_directory>/logs/web.log
- Open SonarQube web interfaces
http://<SonarQube_installation_host_ip>:9000
orhttp://localhost:9000
if 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
-val
or-eva
produces 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-8
Once 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 : [email protected]
Bugs and Feature requests : https://github.com/lequal/sonar-frama-c-plugin/issues
sonar-frama-c-plugin is under GNU GPL v3.