Formidable colleagues, patchlevels and new features in Nitrogen

My colleagues are formidable. Over the last few days, three of them fixed four bugs in my code. And one of the fixes was a simple, obviously correct fix for the bug previously discussed here.

In celebration of these terrific colleagues here is a new patchset for Nitrogen 20111001 patchlevel 2. It replaces patchlevel 1. I have tested it as thoroughly as the previous one that is I didn't even check if it applied cleanly to the Nitrogen tarball.

Finally with the aforementioned bugfix out the door it is time to boast about another new feature available in Nitrogen: string constants. String constants are now properly treated as read-only: the program is not supposed to write there. If it does an alarm is emitted and for the sake of precision when analyzing the rest of the program it is assumed that the write did not take place in the string constant. If the pointer could also point somewhere writable then the write is assumed to take place there instead. If the pointer was only pointing to read-only or otherwise unwritable locations the propagation ends for that state.

If this seems a bit abstract here is the same example as before revisited:

char *p = "foo";
char c;
char s = 'F';
void f(int u)
{
  if (u) p = &c;
  *p = s;
}

Treating f as the entry point of the program the analyzer doesn't know what values may be passed for the argument u. Just before assigning to *p it assumes that p may point to c or inside "foo" but as the program tries to write to *p it warns that p had better point somewhere writable and since the user will of course make sure of that it then knows that p points to c and since p was pointing to c it also knows that c contains 'F' at the end of the function:

...
bl.c:8:[kernel] warning: out of bounds write. assert \valid(p);
...
[value] Values at end of function f:
          p ∈ {{ &c }}
          c ∈ {70}

One of the next steps will be to transform the "p points somewhere writable" condition before the assignment into "u is non-null" as a pre-condition of function f() using weakest pre-condition computation. Quite a lot of effort remains before this works. For one thing the value analysis does not yet distinguish between "valid for reading" and "valid for writing" in the ACSL predicates it annotates the program with (although it makes the distinction in the log messages).

Speaking of string constants I should also mention that the value analysis in Nitrogen emits a warning for "foo" == "foo". I already boasted about that here but Nitrogen wasn't released at the time.

This post was brought to you thanks to the formidableness of Philippe Herrmann Virgile Prevosto and Boris Yakobowski.