Frama-C The recent posts on extremely minor undefined behaviors in zlib neatly tie in with a discussion on John Regehr's blog about the future-proofitude of C and C++. Another insightful post in this regard is this one by Derek Jones. Derek claims that the situation is different for proprietary compilers with...
Read MoreBlogger of multiple qualities Harry McCracken was recently still looking for “an iPad PDF reader which can handle giant files which are 100s of pages long without choking”. Sorry I meant “STILL looking”. PDF is a nineteen-nineties technology to display text and pictures. Key quote: “Each PDF file encapsulates a...
Read MoreIn a previous post we remarked that the decompression function of zlib for some inputs computes an invalid pointer. But at least it neither dereferences it nor compares it to another pointer. Or does it? Recipe for an invalid pointer comparison Instrument Take an ordinary zlib library version 1.2.7 and...
Read MoreAs an interlude in the zlib verification thread, this post asks two questions. Is there any chance of finding a bug in zlib, and does it matter? Could there be a bug in zlib? It is not entirely impossible. The previous post in this blog pointed to a relatively minor...
Read MoreIn an article about comparing static analyzers (long-time readers of the blog do not follow the link. It is still the same old article)… Where was I? Ah yes. One reason why it is extremely tricky to compare static analyzers is that a static analyzer is for identifying undefined behavior...
Read More