RTL-Check / News: Recent posts

A new version is released with minor improvement: a bug has been fixed and performance is improved. The bigest changed is that what was called an abstract value is now an abstract variable. This should make it easier to understand.

The latest version of RTL-Check features a new experimental analysis to detect integer overflows. It also includes a new analysis to automatically detect the size of local variables. A preview release of RDB, a shell to run and debug analysis is also available as a patch.

This version adds a new base class for flow insensitive analyses, it implements an analysis to find automatically the size of call parameters, it adds documentation and it fixes a few bugs.

This version is mostly a bug fix release. Many important bugs that affected the correctness of the analysis were fixed. The analysis as a whole is now cleaner and easier to understand. Integer overflows aside, this version of the analysis is believed to be safe. (The last few versions were definitely not.)

This version improves a few things in the framework and in the main analyis, but the main improvement is the support for widening and narrowing (from abstract interpretation) in the framework.

Improved analysis framework: the relations between solvers, policies, interpreters and analyses are better defined. Better implementation of liveness analysis that follow more closely the definition of a monotone framework. Fixed an important flaw in solvers.

The latest version of RTL-Check supports memory aliases, fixes many bug, has a much cleaner output and improved documentation.

The new version of RTL-Check implements a new much more modular framework for abstract interpretation. The analysis is more precise. See docs/new-architecture for the details.

Try the new version with faster analysis and more complete results.

Implemented abstract interpretation to perform analysis on programs using the constraint system.

This release adds a constraint system to describe program state. Comparison between states have also been implemented. Documentation has been updated.

I just made a new release of RTL-Check. It now tries to automatically build the memory shape of the input expected by a function. It is far from complete, but it might be enough to see what I have in mind.

RTL-Check 0.0.3 was just released. It can now generate control flow graph (CFG) on demand. Just import cfg and then you can access the CFG of any RtlFunction with the cfg attribute.

Download and try it! It requires Python 2.3 or more recent. Feed back will be much appreciated!