Static Analysis For A Class Of Floating-point Range Constraint

The abstract interpretation theory was proposed by P.Cousot and R.Cousot in 1 977, and is widely used in the program's static analysis domain to construct and approximate the program's fixpoint semantics. One of the important applications is used to analyze the range of constraint problems of the variable or expression in the program. The information of the range will help us for the limits of the array and loop analysis, based on an array of data dependence analysis, pointer analysis, cycle time analysis, the executable path analysis.The characteristics of the abstract interpretation theory is reliable, but not complete.that is, if the verification results show that the abstract nature of the system meet the verification, then the abstract interpretation theory ensures the nature of the original system to meet the verification; if test results show that the abstract system does not meet the validation nature, the nature of the original system may satisfy the verification or not, we need to design more precise abstract analysis. A precise abstract domain can reduce this incompleteness, helping to improve the verification efficiency. Therefore, it is the core content of the abstract interpretation theory to design a good and precise abstract domain,including its abstract operation.This paper uses the abstract interpretation theory to estimate the range of the floating-point expression constraint problem whose goal is to improve imcomple-tenses, The main contributions of this article are as follows:First of all,According to the property of the complete lattices on the abstract interpretation theory,the paper gives the abstract semantics of the floating-point based on IEEE 754-1985 model specifications. Then according to some operation properties on the interval abstract domain and the IEEE 754-1985 floating point rounding model,the paper defines the abstract operations on the interval abstract domain.Next,For the sake of the calculation of a balance between accuracy and efficiency,the paper establishs interval constraint for the two variables floating-point linear expressions constraint problems, based on floating-point abstract model and abstract operations on the model. The paper establishs the constraint chart for interval constraint. according to the constraint chart,the paper transform the constraint problem into interval linear equation.Then the paper defined interval operations,and gives solutions of such problems.Last, Compared to the previous algorithm using the widening operators or the narrowing operator, the abstract domain which makes use of our proposed algorithm is more accurately and effectually to represent the reachability state set,and simplify reduce the abstract operations on the abstract domain and reduced the false error report highly.