Frama-C SSL in the news SSL is a protocol for point-to-point confidential and authenticated communication over an insecure medium. It is the protocol behind HTTPS, among many other uses. In an Internet-connected system, the SSL implementation stands at the frontier between the system and the hostile outside world. For this reason,...
Read MoreCorrect and wrong definitions for the constant FLT_EPSILON If I google “FLT_EPSILON”, the topmost result is this page with this definition: FLT_EPSILON the minimum positive number such that 1.0 + FLT_EPSILON != 1.0. No no no no no. I don't know where this definition originates from but it is obviously...
Read MoreA rant about programming interview questions Software development is a peculiar field. An applicant for a more traditionally artistic position would bring a portfolio to eir job interview: a selection of creations ey deems representative of eir work and wants to be judged by. But in the field of software...
Read MoreA discussion I often have addresses the question of whether a compiler¹ can warn for all possible illegal actions a program could take at run-time within a specific, well-understood family² . (1) or some other piece of software that receives a program as input and, in finite time, does something...
Read MoreThere is no “sign extension” in C. Please stop referring to “sign extension” in C programs. In assembly, there is such a thing as “sign extension” Sign-extend is an assembly instruction say movsx %al %ebx to transfer the contents of a narrow register say %al to a wide register say...
Read More