In a setting where we have intervals for the values of floating-point variables x, a, and b, we are interested in improving these intervals when the floating-point equality x ⊕ a = b holds. This problem is common in constraint propagation and called the inverse projection of the addition. It also appears in abstract interpretation for the analysis of programs containing IEEE 754 operations. We propose floating-point theorems that provide optimal bounds for all the intervals. Fast loop-free algorithms compute these optimal bounds using only floating-point computations at the target precision.

Type-based alias analyses allow C compilers to infer that memory locations of distinct types do not alias. Idiomatic reliance on pointers on the one hand, and separate compilation on the other hand, together make it impossible to get this aliasing information any other way. As a consequence, most modern optimizing C compilers implement some sort of type-based alias analysis. Unfortunately, pointer conversions, another pervasive idiom to achieve code reuse in C, can interact badly with type-based alias analyses. This article investigate the fine line between the allowable uses of low-level constructs (pointer conversions, unions) that should never cause the predictions of a standard-compliant type-based alias analysis to be wrong, and the dangerous uses that can result in bugs in the generated binary. A sound and precise analyzer for “strict aliasing” violations is briefly described.

TIS-Analyzer is a static analysis platform based on FramaC. It integrates C analyzers in a plugin architecture and can be used to soundly detect undefined behaviors in C programs. The plugins communicate with each other to increase their precision. The Value analysis is an important TIS-Analyzer plugin. It uses dataflow analysis to produce a sound representation of the memory state at each control point of the program. Its abstract domain allows to represent disjunctions of non-relational value states. Further plugins then use this information to conduct derived analyses (operational inputs, dependencies...) However, some information is lost in the process: the derived analyses cannot know which disjuncts of the representation of an abstract state can be reached from each disjunct of the state at the preceding statement. We propose to represent the state of the Value analysis with a graph that refines the control flow graph of the analyzed program and that accurately represents the disjunction of abstract memory states at each statement in separate nodes. This avoids the aforementioned loss of information and leads to precision gains for the derived analyses. This new domain also allows us to formalize the Value analysis and its use of disjunctions in terms of abstract interpretation. Finally, result graphs are suited for human review and allow users to find the root cause of alarms raised by the analysis. 1. A MOTIVATING EXAMPLE The operational inputs (or inout) plugin of Frama-C [4] computes the operational inputs and sure outputs of each function call in a C program. The operational inputs are defined as the memory zones that may be read by the program without having been previously overwritten, and the sure outputs are the memory zones that are written to for sure. The inout plugin runs a dataflow analysis on the control flow graph, with knowledge of the results of Value. In the program represented in Figure 1, we therefore expect the operational inputs to be empty (t[1] is read, but not before having been written to) and the sure outputs to be t, i and x. However, the program’s control flow graph is not expressive enough to reflect that the program goes through the full three iterations of the for loop. The dataflow analysis therefore concludes that it is possible to read t[1] at line 8 without having initialized it in, which makes it an operational input. Although the value analysis did iterate through ∗This work was partially supported by the French ANR-14CE28-0014 AnaStaSec. 1 char t[3]; 2 void main() { 3 int i,x; 4 for (i=0; i<3; i++)

While the development of one software verification tool is often seen as a difficult task, the realization of a tool combining various verification techniques is even more complex. This paper presents an innovative tool for verification of C programs called Sante (Static ANalysis and TEsting). We show how several tools based on heterogeneous techniques such as abstract interpretation, dependency analysis, program slicing, constraint solving and test generation can be combined within one tool. We describe the integration of these tools and discuss particular aspects of each underlying tool that are beneficial for the whole combination.

During the last decade, static analyzers of source code have improved greatly. Today, precise analyzers that propagate values for the program's variables, for instance with interval arithmetic, are used in the industry. The simultaneous propagation of sets of values, while computationally efficient, is a source of approximations, and ultimately of false positives. When the loss of precision is detrimental to the user's goals, a user needs to provide some kind of manual guidance. Frama-C, a framework for the static analysis of C programs, provides a sound value analyzer. This analyzer can optionally be guided by skillfully placed user annotations. This article describes SPALTER, a Frama-C plug-in that uses a variation of the Skelboe-Moore algorithm from the field of interval arithmetic to guide Frama-C's value analyzer towards a high-level objective set by the user. SPALTER reproduces the results of a case study that used Frama-C's value analysis and required extensive manual guidance. In difference, our approach with SPALTER required no guidance, except preparation of the analyzed program by slicing.

Static analysis benchmarks matter. Although benchmarking requires significant effort, it has driven innovation in many areas of Computer Science. Therefore this process and the underlying testcases should be carefully devised. However the problem that static analysis tackles—statically predicting whether a program is correct, or what it does when executed—is so hard that there exist no perfect oracle. For this and other reasons, there is little consensus on desirable and undesirable properties of a static analyzer. This article discusses some of these issues. Its examples involve the minutiae of C, but the principles should generalize to static analysis for most programming languages and, for some, to benchmarks for other partial solutions to undecidable problems.

Frama-C is a source code analysis platform that aims at conducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive verification, and testing, for safety- and security-critical software. Collaborative verification across cooperating plug-ins is enabled by their integration on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.

To report a compiler bug, one must often find a small test case that triggers the bug. The existing approach to automated test-case reduction, delta debugging, works by removing substrings of the original input; the result is a concatenation of substrings that delta cannot remove. We have found this approach less than ideal for reducing C programs because it typically yields test cases that are too large or even invalid (relying on undefined behavior). To obtain small and valid test cases consistently, we designed and implemented three new, domain-specific test-case reducers. The best of these is based on a novel framework in which a generic fixpoint computation invokes modular transformations that perform reduction operations. This reducer produces outputs that are, on average, more than 25 times smaller than those produced by our other reducers or by the existing reducer that is most commonly used by compiler developers. We conclude that effective program reduction requires more than straightforward delta debugging.

Frama-C is a source code analysis platform that aims at con- ducting verification of industrial-size C programs. It provides its users with a collection of plug-ins that perform static analysis, deductive veri- fication, and testing, for safety- and security-critical software. Collabora- tive verification across cooperating plug-ins is enabled by their integra- tion on top of a shared kernel and datastructures, and their compliance to a common specification language. This foundational article presents a consolidated view of the platform, its main and composite analyses, and some of its industrial achievements.

DO-178B compliant avionics development processes must both define the data and control flows of embedded software at design level, and verify flows are faithfully implemented in the source code. This verification is traditionally performed during dedicated code reviews, but such intellectual activities are costly and error-prone, especially for large and complex software. In this paper, we present the Fan-C plug-in, developed by Airbus on top of the abstract-interpretation-based value and dataflow analyses of the Frama-C platform, in order to automate this verification activity for C avionics software. We therefore describe the Airbus context, the Frama-C platform, its value analysis and related plug-ins, the Fan-C plug-in, and discuss analysis results and ongoing industrial deployment and qualification activities.

Static analyzers should be correct. We used the random C-program generator Csmith, initially intended to test C compilers, to test parts of the Frama-C static analysis platform. Although Frama-C was already relatively mature at that point, fifty bugs were found and fixed during the process, in the front-end (AST elaboration and type-checking) and in the value analysis, constant propagation and slicing plug-ins. Several bugs were also found in Csmith, even though it had been extensively tested and had been used to find numerous bugs in compilers.

We present functional dependencies , a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.

interpretation, static analysis, value analysis, data flow analysis, avionics software, DO-178B, industrial application

We demonstrate the value analysis of Frama-C. Frama-C is an Open Source static analysis framework for the C language. In Frama-C, each static analysis technique, approach or idea can be implemented as a new plug-in, with the opportunity to obtain information from other plug-ins, and to leave the verification of difficult properties to yet other plug-ins. The new analysis may in turn provide access to the data it has computed. The value analysis of Frama-C is a plug-in based on abstract interpretation. It computes and stores supersets of possible values for all the variables at each statement of the analyzed program. It handles pointers, arrays, structs, and heterogeneous pointer casts. Besides producing supersets of possible values for the variables at each point of the execution, the value analysis produces run-time-error alarms. An alarm is emitted for each operation in the analyzed program where the value analysis cannot guarantee that there will not be a run-time error.

This experience report describes the choice of OCaml as the implementation language for Frama-C, a framework for the static analysis of C programs. OCaml became the implementation language for Frama-C because it is expressive. Most of the reasons listed in the remaining of this article are secondary reasons, features which are not specific to OCaml (modularity, availability of a C parser, control over the use of resources...) but could have prevented the use of OCaml for this project if they had been missing.

This article describes the implementations of weak pointers, weak hashtables and hashconsing in version 3.10.2 of the Objective Caml system, with focus on several performance pitfalls and their solutions.

This article describes an efficient persistent mergeable data structure for map- ping intervals to values. We call this data structure rangemap. We provide an example of appli- cation where the need for such a data structure arises (abstract interpretation of programs with pointer casts). We detail different solutions we have considered and dismissed before reaching the solution of rangemaps. We show how they solve the initial problem. We then describe their implementation and, as a conclusion, mention further work we would like to do. RÉSUMÉ. Cet article décrit une structure de données représentant efficacement des tables d'associations persistantes indexées par des intervalles, ayant la propriété supplémentaire d'être fusionnable. Nous nommons (en anglais) rangemap cette structure de données. Nous donnons un exemple de circonstances dans lesquelles se rencontre le besoin d'associer de cette façon des valeurs à des intervalles (analyse par interprétation abstraite de programmes com- portant des conversions de pointeurs). Nous détaillons différentes solutions envisagées puis écartées avant d'arriver à la solution des rangemaps. Nous montrons ensuite comment ceux-ci résolvent le problème initial. Enfin, nous décrivons leur implémentation avant d'évoquer les travaux en cours et futurs que nous nous proposons de mener à ce sujet.