Progress of the value analysis tutorial

Boron's value analysis manual has the beginning of a captivating tutorial and I figure that the suspense must be unbearable. I on the other hand already know how it ends. But I'm not telling yet. Neener-neener! Okay maybe later on this blog.

The new manual (with an expanded tutorial) will be released at the same time as Frama-C version Carbon which is not immediately for various technical reasons. The new version will have some amazing performance improvements but the Boron version is good enough for one of the steps that comes after the current tutorial ends:

Generalizing to arbitrary numbers of Update calls

As an exercise try to verify that there cannot be a run-time error when hashing arbitrary contents by calling Update(... 80) an arbitrary number of times between Init and Final. The general strategy is to modify the C analysis context we have already written in a way such that it is evident that it captures all such sequences of calls and also in a way such that launched with adequate options the value analysis does not emit any warning.

The latter condition is harder than the former. Observing results (with the GUI or observation functions described in section 8.3) can help iterate towards a solution. Be creative.

Solution(s) in a few days.

Note: if you try the tutorial for the first time or on a new computer you may also appreciate this new paragraph in the documentation:

Some compilation plaforms' headers define the names memset and memcpy in a way that make it impossible to provide your own implementation for these functions. If this happens for yours you can try placing your own header in the analysis directory under the name string.h

typedef unsigned int size_t;
void* memcpy(void* region1  const void* region2  size_t n);
void* memset (void* dest  int val  size_t len);