Frama-C This page contains various remarks that did not make it into our article about Csmith-testing Frama-C. It is an annex of sorts except that it is written in a less formal style that will be familiar to readers of the Frama-C blog. It is not intended to make sense by...
Read MoreMy presentation Friday at the U3CAT meeting was on the topic of Frama-C Csmith testing. Several posts in this blog already describe facets of this work (it has its own tag). Yet another angle can be found in this short article draft. Said draft by the way will soon need...
Read MoreYes, I have read that static analysis post If you are one of the three persons in the world who have not sent me a link to John Carmack's Christmas post on static analysis [removed dead link] go ahead and read it it might interest you. You can stop sending...
Read MoreReminiscing The first benchmark Frama-C's value analysis was ever evaluated on was the Verisec suite, described in "A buffer overflow benchmark for software model checkers". My colleague Géraud Canet was doing the work thence the facetious-colleagues tag of this post. In retrospect Verisec was a solid piece of work. Being...
Read MoreMac OS X and assembly labels A few months ago, I was moving things around in Zarith. It's a good way to relax not unlike gardening. And then I noticed something strange. On Mac OS X a label in assembly code is marked as local by prefixing it with "L"...
Read More