The Interproc Analyzer

This is a web interface to the Interproc analyzer connected to the APRON Abstract Domain Library and the Fixpoint Solver Library, whose goal is to demonstrate the features of the APRON library and, to a less extent, of the Analyzer fixpoint engine, in the static analysis field.

There are two compiled versions: interprocweb, in which all the abstract domains use underlying multiprecision integer/rational numbers, and interprocwebf, in which box and octagon domains use underlying floating-point numbers in safe way.

This is the Interproc version

Arguments

Please type a program, upload a file from your hard-drive, or choose one the provided examples:




Numerical Abstract Domain:
Kind of Analysis: (sequence of forward and/or backward analysis)

Iterations/Widening options:
guided iterations widening delay descending steps
debugging level (0 to 6)

Hit the OK button to proceed:

``Simple'' language syntax

Here are some program examples: incr ackerman fact numerical numerical2 maccarthy91 heapsort symmetricalstairs

Results

In order not to flood our web-server, analysis computation time is limited to 1min in this demonstration. Also note that result files are temporary files stored on our server that have a very short life-time.

The analysis computes an invariant at each program point.

Informations

The Interproc is freely available. It is written in C, with a OCaml binding. The APRON Abstract Domain Library analyzer and the Fixpoint Solver Library are freely available, and are written in OCaml.

This CGI-WEB interface is written in OCaml using the OCamlHtml library, freely available



Bertrand Jeannet
bjeannet@NOSPAM inrialpes.fr