Interval Analysis of C-variables using Abstract Interpretation

Interpretation Andreas Ermedahl Mikael Sjodin December 18, 1996 Department of Computer Systems, Uppsala University Box 325, S-751 05 Uppsala, Sweden email: febbe, micg@docs.uu.se Contents 1 Introduction 4 2 Data Flow Analysis 4 2.1 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 Program description . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 Fixpoints . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 2.4 Iteration strategies . . . . . . . . . . . . . . . . . . . . . . . . . . 6 Jacobi iteration . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 Chaotic iteration . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3 Introducing Intervals 7 4 Interval Abstraction 8 4.1 Galois connection . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Monotonicity of ff . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 Monotonicity of fl . . . . . . . . . . . . . . . . . . . . . . . . . . . 10 ff(d) v d 0 , d ` fl(d..