Frama-C In an ACSL post-condition, any reference to the name of one of the function's arguments is assumed to refer to the initial value of the argument. /* ensures arg == 1; */ void f(int arg) { arg = 1; } For instance, in function f above, Frama-C's value analysis plug-in...
Read MoreI move that all computing devices be equipped with a small explosive charge, set to explode when someone refers someone else to Goldberg's What Every Computer Scientist Should Know About Floating-Point Arithmetic without the referrer emself having read it. It would not have to be lethal. I could be content...
Read MoreAutomatic testcase reduction for compilers: the story so far A previous post linked to a discussion of manual testcase reduction when the program being debugged is a compiler (and the input demonstrating the faulty behavior is thus a C program). Since then quite a few related events took place: In...
Read MoreWe interrupt our regularly scheduled program to link to this post by Jakob Engblom. The post was prompted by the jury's conclusion in a lawsuit over what appears to be an automotive software glitch that the carmaker is liable.
Read MoreBruce Dawson has written a superb blog post on a Visual C++ compiler bug (now fixed) covering every aspect an essay on compiler bugs should cover. I really like one section that I am going to quote in full: Security In these paranoid days of the NSA subverting every computer...
Read More