Lab for Automated Reasoning and Analysis LARA

Variable Range Analysis

By: Simon Blanchoud and Yuanjian Wang Zufferey

Based on the paper of Patrick Cousot and Radhia Cousot

Implemented in OCaml as we have in mind to get integrated into Jahob to be able to analyse real Java code.

Goal

Our goal is to compute the range of all variables in a piece of code as precisely as possible. These ranges could then be reused for latter analysis (e.g. possible division by 0, array out of bound, …).

Done

  • Fully analysis with one variable, loops, branches and sequences
  • Use float values with operators +, -, * and /
  • Uses both widening to ensure convergence and narrowing to precise the result

To Do

  • Accept multiple variables
  • Call to procedure

Possible Improvements

  • Call to functions
  • Arrays
  • Object-oriented properties handling

Material

 
variable_range_analysis.txt · Last modified: 2007/06/30 03:30 by simon.blanchoud