Improving static analyses of C programs with conditional predicates

Sandrine Blazy 1 David Bühler 1, 2 Boris Yakobowski 2
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
2 LSL - Laboratoire Sûreté des Logiciels
LIST - Laboratoire d'Intégration des Systèmes et des Technologies : DRT/LIST
Abstract : 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.
Type de document :
Article dans une revue
Science of Computer Programming, Elsevier, 2016, 118, 〈10.1145/2854065.2854082〉
Liste complète des métadonnées

Littérature citée [34 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01242077
Contributeur : Sandrine Blazy <>
Soumis le : mardi 25 octobre 2016 - 12:04:20
Dernière modification le : mardi 16 janvier 2018 - 15:54:17
Document(s) archivé(s) le : vendredi 3 février 2017 - 12:24:04

Fichier

elsmain.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Sandrine Blazy, David Bühler, Boris Yakobowski. Improving static analyses of C programs with conditional predicates. Science of Computer Programming, Elsevier, 2016, 118, 〈10.1145/2854065.2854082〉. 〈hal-01242077〉

Partager

Métriques

Consultations de la notice

371

Téléchargements de fichiers

107