Interval Analysis Method For Floating-point C Programs

As a basic data type in the C program, the floating point type is widely used inmany softwares. As a result, research on the analysis method on floating-point programsis important to the independence of this kind of software. The value range offloating-point variables in the program is very important for analyzing properties andfinding run-time errors. The inexactness of floating-point computation makes itchallenging to analyze value range of floating-point variables.The theory of abstract interpretation provides a general framework to analyze thevalue range of program variables. Under this framework, this paper proposes a newnumerical abstract domain, namely powerset of intervals abstract domain, which usesdisjunctions of finite numbers of intervals to express the value range of a variable. It ismore expressive than the classic interval abstract domain, and it can infer somenon-convex properties that are beyond the ability of most numerical abstract domains.For the sake of efficieny, this paper makes use of floating-point number toimplement the abstract domain, and meanwhile provides a sound implementing method.And then it tells the application of floating-point powerset of intervals in the analysis offloating-point program, and the way how to ensure the soundness as well as.Finally, this paper implements a static analyzer prototype for analyzingfloating-point C programs based on the abstract interpretation framework. It has threeparts: the module of frontend for preprocessing, the module of numeric abstract domainlibrary and the module of iterating for calculating the fix-point. This paper makes use ofan open source compiler frontend to get the control-flow graph of the source program,and build the semantic equation based on the type provided by Apron, a numericabstract domain library. And it calculates the numeric invariant of the program to beanalysesed eventually. So far the tool prototype has analysesd some intraprocedual Ccodes.At last, based on the tool prototype, this paper do some experiments on thefloating-point programs based on the powerset of intervals domain and the intervaldomain. The result shows that the former could illustrate the non-convex value rangeinformation well.