Frama-C In order to create a tradition of providing solutions to previous quizzes, this post is a partial answer to the question in this one about Frama-C's value analysis. To recap: at the end of the Boron tutorial we arrive at the main function below. This function is useful as an...
Read MoreA simple example Broadly speaking, every location which is not mentioned in such a clause should have the same value when exiting the corresponding code as it when entering it. For instance, if we take the following declaration (extracted from ACSL by Example) /*@ assigns \ othing; */ bool equal(const...
Read MoreBoron'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...
Read MoreFrama-C is an extensible platform dedicated to the analysis of C programs. It provides various plug-ins for navigating in a C code and better understanding its semantics. It can also be used to guarantee the absence of run-time error in a given program. At last, given a specification expressed in...
Read More