Frama-C This post is a follow-up of bug 990. When this issue was resolved the following question arose: "Why is it so dangerous to have a global c declared as a pointer in one compilation unit and defined as an array in another one given the fact that almost anywhere an...
Read MoreIf you like this blog, then on the basis of recent posts, you will with good probability like that blog. The recent posts I have read all deal with various subtle undefined behaviors in C.
Read MoreThe function in this post to the musl mailing list is a good candidate for formal verification. It should just barely be possible to verify the absence of undefined behaviors with Frama-C's value analysis and it should just barely be possible to verify it functionally with one of the Jessie...
Read MoreSven Mattsen is working at CEA until the summer. He is the author of this post. The post continues the series explaining how to guide the value analysis towards more precise conclusions. It starts where that one and that other left off. Problem This article is concerned with the Value...
Read MoreSemi-serious musings During the Frama-C random testing experiment described at length on this blog and this page we found a few bugs in Csmith too. John Regehr one of the Csmith developers and not entirely coincidentally a co-author of the article linked in the previous post is also a co-author...
Read More