Frama-C A privately sent question may deserve a quick blog post. Context The example is as below: int x, y, s; main(){ x = Frama_C_interval(0, 2000000000); y = 1000000000; s = x + y; Frama_C_dump_each(); } Sorry for all the zeroes. There are nine of them in each large constant, so...
Read MoreThis 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 More