Frama-C Likely, you have heard this one before: Two campers are surprised by an angry bear. One of them starts putting on eir running shoes. Surprised the other exclaims “What are you doing Alex? You can't outrun a bear!” To which Alex replies: “I don't have to outrun the bear. I...
Read MoreIn 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 More