Driving Frama-C's Value Analysis Towards a User Specified Goal
SPALTER is a Frama-C plug-in that iteratively improves the precision of Frama-C's value analysis results. It uses a variation of the Skelboe-Moore algorithm from the field of interval arithmetic and instructs Frama-C to execute case analyses that reintroduce previously ignored relations.
The video below shows SPALTER applied to the donut example. The Y axis of the graph represents possible values for the maximum of the function.
Each dot represents an (input dimension-4 cube, output interval) pair from the worklist. The algorithm consumes limiting pairs (that is, dots from the topmost line). The resulting sub-divided dimension-4 cubes hopefully allow to compute a lower maximum, making other lines grow.
On the right-hand side, the current best estimate for the maximum is the value of "Currgoal". When an entire line has been consumed, this value improves. "Currborder" is the best known minimum value for the maximum. The input dimension-4 cubes for which function compute() is known to be always below this value can be discarded.