Home

Welcome to the sonar-frama-c-plugin wiki!

---

Table of contents

• About
• Build
• Install
• Configure
• Run
• Frama-c plugin rules definition
• Contribute
• Support
• Licensing

About

Sonar-frama-c-plugin is a SonarQube plugin integrating frama-c results into SonarQube dashboard.

Build

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)

Install

• Copy the generated jar into <SonarQube_installation_directory>/extensions/plugins.
• Restart SonarQube : sonar restart or service sonar restart
• Check SonarQube logs : tail -f <SonarQube_installation_directory>/logs/web.log

Configure

• Open SonarQube web interfaces http://<SonarQube_installation_host_ip>:9000 or http://localhost:9000 if your are on the host machine
• Select "FramaC Quality Profile" and add selected Frama-c rules to the Profile.

Run

Prepare Frama-c project

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

Configure sonar-scanner

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

Run sonar-scanner

Once you got frama-c results and sonar-project.properties configured, you can launch sonar scanner from you project directory : sonar-scanner

Frama-c plugin rules definition

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

Contribute

You can contribute to sonar-frama-c-plugin :

• following the defined CODE_OF_CONDUCT
• using the PULL_REQUEST_TEMPLATE
• using the ISSUE_TEMPLATE

Support

Contact : [email protected]

Bugs and Feature requests : https://github.com/lequal/sonar-frama-c-plugin/issues

Licensing

sonar-frama-c-plugin is under GNU GPL v3.