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
IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL, Inria Rennes – Bretagne Atlantique
2 LSL - Laboratoire Sûreté des Logiciels
DILS - Département Ingénierie Logiciels et Systèmes : DRT/LIST/DILS
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 conditionals statements, and postpone the loss of information. The work has been integrated into Frama-C, a C source code analysis platform. Experiments on real code show that our approach scales, and improves significantly the precision of the existing analyses of Frama-C.
Type de document :
Communication dans un congrès
FMICS 2014: Formal Methods for Industrial Critical Systems, Sep 2014, Florence, Italy. Lecture Notes in Computer Science (LNCS) (8718), pp.15, 2014, FMICS 2014: Formal Methods for Industrial Critical Systems. 〈http://fmics2014.unifi.it〉. 〈10.1007/978-3-319-10702-8_10〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01242087
Contributeur : Sandrine Blazy <>
Soumis le : vendredi 11 décembre 2015 - 14:12:29
Dernière modification le : mercredi 16 mai 2018 - 11:23:28

Lien texte intégral

Identifiants

Collections

Citation

Sandrine Blazy, David Bühler, Boris Yakobowski. Improving static analyses of C programs with conditional predicates. FMICS 2014: Formal Methods for Industrial Critical Systems, Sep 2014, Florence, Italy. Lecture Notes in Computer Science (LNCS) (8718), pp.15, 2014, FMICS 2014: Formal Methods for Industrial Critical Systems. 〈http://fmics2014.unifi.it〉. 〈10.1007/978-3-319-10702-8_10〉. 〈hal-01242087〉

Partager

Métriques

Consultations de la notice

410