Reduce Warnings from Static Code Analysis

Meta-Information

Also known as Refined Code Analysis

Written: September 2014

Origin: Brian Nielsen / Aalborg University

Purpose: The intent is to reduce number of false positives from static code analyzers (SCA). SCA tools use abstraction interpretation techniques to produce results efficiently but at the cost of over-approximating and producing warnings of which many, but not all, are false-positives. Normally, a huge manual effort is needed subsequently to prove that a warning is a false-positive. The idea behind this pattern is to formulate a smaller analysis problem that can be analyzed by more precise techniques (but at the same time likely more time consuming and less scalable) to investigate the warnings automatically.

Context/Pre-Conditions: Static code analysis applied to safety critical software; most warnings are false-positives.

To consider: Implementing this pattern requires fairly sophisticated solutions because the static code analyzer has to output the required data needed to formulate the subsequent analysis problem, and because this must preserve the semantics of the underlying program to be analyzed. However, once implemented little user involvement is required, except assist in tuning verification parameters the model-analyzer.

Structure

Participants and Important Artefacts

Static Code Analyzer: A tool that analyses (source) code by safe approximation techniques like abstract interpretation.

Model Generator: A tool that is capable of transforming a program slice into a semantic preserving model that can be analyzed by another analysis techniques.

Model Analyzer: A more precise analysis tool (model-checker or sat-solver).

Report Merger: A script that merge the original report from the SCA and refined results from the refined analysis.

.

Actions / Collaborations

(1) A static code analyzer is configured and applied to the source code under investigation. This produces an analysis report containing a set of confirmed defects, and warnings. In case of warnings diagnostic data is also generated in terms of a program slice and a path-precondition for the approximate location that triggers the warning.

(2) For each warning, a simpler analysis problem is defined based on the source code, configuration information and the diagnostic information. The model generator is invoked to create a problem formulation for the analyzer.

(3) The analyzer is invoked on the simpler model-problem, and eventually generate a report for the warning, stating whether it was a false positive, a confirmed defect or still unknown.

(4) The report merger creates the final combined report.

.

Discussion

Implications:

Benefit: false warnings from SCA are avoided without the need to manually inspect the code. This helps to avoid huge manual efforts for subsequent prove that a warning is a false positive.

Limitation: pattern requires experience by the tool developer (not end-user) for semantics-preserving transformation of the source code and SCA output into the notation required for the subsequent analysis.

Implementation of the pattern needs some effort that compensates partially the efforts needed for manually showing that warnings are false positives.

Comments:

– More research may help determining what kind of analysis technologies and tools are effective on the derived/reduced model.

– Concerning “report merger” (from F.Loiret, Dec.13, 2013): its work can be substantially supported be IOS standardized interfaces. Once all data are available from multiple sources (i.e., from the Tool Adaptors) and provided in a harmonized way (thanks to the IOS), then it becomes straightforward for a consumer (in this case, the report merger / dashboard) to get access to these data which are distributed over the tool chain, process it, and present relevant outputs to the end user.

.

Application Examples

MBAT Automotive Use Case 2 (Common Powertrain Control) / (model checking):

Comment: significant effort

MBAT Rail Use Case 3 (ZLB ATOP System) / (hot spot analysis):

Comment: Variance of the pattern

– Test cases represent subproblems.

– RT-Tester tries to generate TCs for hot spots. Those hot spots, for which no TC can be generated, are false positives.

.

 

Relations to other Patterns

Pattern Name	Relation*
Target MBA&T by Static Code Analysis	This pattern (Reduce Warnings from SCA) helps to avoid uneccesary work in that pattern

* “this pattern” denotes the pattern described here, “that pattern” denotes the related pattern