Frama-C Mac 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 MoreThis blog simultaneously passed the 100-posts and the 50-comments milestones, and also its 15-months birthday. Readers should now decide of future orientations. What does this blog need most? A norant tag, so that it's easy to subscribe to all posts but rants? A spivak tag, in order for Spivak pronouns...
Read MoreIf Frama-C doesn't work out, we can always make a comedy team Facetious colleagues ask me how I make Frama-C's value analysis' messages so informative. \Pascal " one of them says "in this case study the generated log contains 8GiB of information! It won't open in Emacs...". I helpfully point...
Read MoreI have been able to divert a few hours yesterday and today for programming. It was well worth it, as I have discovered a theorem. It is new to me, and I wonder whether it was ever published. The theorem is, a C program cannot double free() a block even...
Read MoreJustification There recently was a thread in the Frama-C mailing list on verifying the Rijndael cipher, standardized and better-known as AES. Nowadays, AES is mostly famous for being sensitive to timing attacks. An attacker measuring the time it takes to encrypt known plaintext with an unknown key can deduce the...
Read More