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 betweenInitandFinal. 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:
{% endraw %}Some compilation plaforms' headers define the names
memsetandmemcpyin 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 namestring.htypedef unsigned int size_t; void* memcpy(void* region1 const void* region2 size_t n); void* memset (void* dest int val size_t len);