Frama-C This post offers two C programs that look analyzable. Each is self-contained, not so small that verification is trivial, but not so big that it's a man-year effort. If it was me doing the work, I would see what Frama-C's value analysis can do, but if you decide to do...
Read MoreI usually feel uncomfortable diving into the subject of safety vs security, because while I think I have a good intuition of the difference between them, I find this difference hard to formalize in writing. Fortunately, a large “security” “administration” provides: “We use layers of security to ensure the security...
Read MoreMy colleague Boris Yakobowski is on holidays, and while leisurely browsing the internet, he seems to have stumbled upon my previous post. He e-mailed me about it. For some reason, it does not feel right to provide much biography when mentioning facetious colleagues perhaps because it would look too self-congratulatory...
Read MoreThis blog post describes for the first time some options that became available in Nitrogen, continuing this series. This post also offers a benchmark but the results of this benchmark cannot be reproduced with Nitrogen. They should be reproducible with the next version of Frama-C. Alarms false alarms and redundant...
Read MoreHere are two links related to ptrdiff_t: Ptrdiff_t is evil [removed dead link] a blog post for if you are not tired of conversion and promotion issues yet and an interesting answer on StackOverflow. I was doubtful about the second one (I had no difficulties to accept the first one...
Read More