Improving static analyses of C programs with conditional predicates

8 years 7 months ago

Download www.yakobowski.org

Abstract. Static code analysis is increasingly used to guarantee the absence of undesirable behaviors in industrial programs. Designing sound analyses is a continuing trade-oﬀ between precision and complexity. Notably, dataﬂow analyses often perform overly wide approximations when two control-ﬂow 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 signiﬁcantly the precision of the existing analyses of Frama-C.

Sandrine Blazy, David Bühler, Boris Yakobowsk

Real-time Traffic