Glossing over Bugs

We have a set of end-to-end tests that run on Goanna every night. This ensures that our commits during the day don’t break our development tree too badly.

Here is one of those tests. It was producing a strange result.Review Android Smartphone

void example(void) {
  int *x;
  x = malloc(sizeof(int));
  free(x);
  if (rand()) {
    x = malloc(sizeof(int));
  }

  *x++;
}

For this code, Goanna produced two warnings:

ex.c:12: warning: Variable `x' may have been freed
ex.c:12: warning: Pointer `x' reassigned, possible memory leak

The first was expected. Depending on the output of rand(), sometimes we de-reference after a free(), a segfault waiting to happen. But what is this second warning about memory being reassigned?

I assumed it was a bug in Goanna, and immediately Paul and I started generating debugging output and messing with the example code.

After a full ten minutes of searching, Paul and I suddenly realised what *x++ does: First it de-references the pointer, returning the value pointed to by x, then it post-increments the pointer x. That is, after the statement *x++, x is no longer pointing to the same piece of memory. Calling free(x) after *x++ would lead to disaster.

So the second warning is no bug in Goanna, it is a bug in our C example. Only 13 lines long and I managed to get confused, because when I saw *x++, I read it as (*x)++.

Tags:
1 Comment
  • Pascal Cuoq

    May 20, 2009 at 8:54 pm

    This happens to us all the time. You could call it an unforeseen consequence of writing in OCaml a static analyzer for a language with a completely different syntax.

    Another related “problem” is that Frama-C developpers write “==” in OCaml modules in places where they meant “=”, because they have been looking at C test files all morning. We actually complained about this in
    http://www.mediafire.com/?gt5hyzhybxg
    but we do not have a solution to propose, apart from the very low-tech periodical grep for “==” in the .ml files.

    Good luck with the launch. I hope we’ll be in touch.

    Pascal

Post a Comment