Improving static analyses of C programs with conditional predicates - CEA - Commissariat à l’énergie atomique et aux énergies alternatives Accéder directement au contenu
Article Dans Une Revue Science of Computer Programming Année : 2016

Improving static analyses of C programs with conditional predicates

Résumé

Static code analysis is increasingly used to guarantee the absence of undesirable behaviors in industrial programs. Designing sound analyses is a continuing trade-off between precision and complexity. Notably, dataflow analyses often perform overly wide approximations when two control-flow paths meet, by merging states from each path. This paper presents a generic abstract interpretation based framework to enhance the precision of such analyses on join points. It relies on predicated domains, that preserve and reuse information valid only inside some branches of the code. Our predicates are derived from conditional statements, and postpone the loss of information. The work has been integrated into Frama-C, a C source code analysis platform. Experiments on real generated code show that our approach scales, and improves significantly the precision of the existing analyses of Frama-C.
Fichier principal
Vignette du fichier
elsmain.pdf (697.18 Ko) Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-01242077 , version 1 (25-10-2016)

Identifiants

Citer

Sandrine Blazy, David Bühler, Boris Yakobowski. Improving static analyses of C programs with conditional predicates. Science of Computer Programming, 2016, 118, ⟨10.1145/2854065.2854082⟩. ⟨hal-01242077⟩
285 Consultations
323 Téléchargements

Altmetric

Partager

Gmail Facebook X LinkedIn More