Frama-C I know! Let us make [ and ] function as meta-characters when in code style. Users will surely love the ability to insert hyperlinks inside the code they are writing a blog post about. —The authors of the Content Management System this blog relies on In the previous post, (float){…},...
Read MoreYesterday's quiz was about the expression *(char*)(float[]){x*x} - 63 (for big-endian architectures) or *(3+(char*)(float[]){x*x}) - 63 (for little-endian ones). This post provides an explanation. First, let us try the function on a few values: int main(){ for (unsigned int i=0; i<=20; i++) printf(\l(%2u)=%d" i l(i)); } This may provide the...
Read MoreA remark I have not heard about the last two posts is the following. Pascal, how can you, in your last post claim that formal verification would have found the bug in your decimal-to-floating-point function? This is the kind of outrageous claim you rant against in your penultimate post! Formal...
Read MoreIn a previous post almost exactly one year ago before Frama-C Oxygen was released I mentioned that the then future release would incorporate a custom decimal-to-binary floating-point conversion function. The reason was that the system's strtof() and strtod() functions could not be trusted. This custom conversion function is written in...
Read More