This project is read-only.

Abandoning well-formedness checks for assertions

Jul 30, 2009 at 1:23 PM


currently, we generate reads checks for memory accesses in assertions. The main purpose here was to prevent the counter-intuitive situation where we could prove certain assertion in ghost code but could not use this knowledge. For example:

#include "vcc.h"

void foo(int *p)
  requires(*p == 5)
  int i;
  assert(*p == 5);
  i = *p;

Here, the assert can be proved, but then the assignment fails because in the physical code we need to be able to show that we can actually physically read from *p. To prevent situations like this, we have created the well-formedness checks.

Generating these assertions is relatively simple, but we now have an issue with the generation of a meaningful error message in case such a verification failed. A general solution for this problem would be somewhat involved, which led us to re-think the whole concept of well-formedness checks.

So, my question is: have you actually encountered situations where you found the the well-formedness checks have helped you? Or are you mostly annoyed by them and if they fail you disable them using "skip_wf"?



Jul 30, 2009 at 1:40 PM

Actually, why not just insert the necessary reads instead of just checking that they are there?

Or is there a situation where "requires(*p == 5)" might be necessary, but I do not want to read that location?


Jul 30, 2009 at 1:51 PM

Since a non-well-formed assertion can't introduce unsoundness, why not make it a warning rather than an error?

Jul 30, 2009 at 2:09 PM

We cannot do this because it is a Boogie assertion and these either succeed or fail, where the latter is an error. Also, the question "warning or error", is really orthogonal to the original question, which was "useful or not".

Jul 30, 2009 at 3:11 PM

I was responding to the "annoying or not" part of the question :) The main source of annoyance is the need to put in the skip_wf to make the verification succeed.

Jul 30, 2009 at 3:15 PM

But then, what's the point in having in a check where, as soon as it fails, you disable it (in case of an error) or ignore it (in case of a warning).

Thus the question: have there been situations where somedoby had the well-formedness test fail because of a genuine problem in the assertion?

Jul 30, 2009 at 3:23 PM

Personally, I don't find the well-formedness check very useful and could live without it. Maybe we should allow enabling it (and similar checks?) at the command-line, like for a "novice mode" or something.

Aug 3, 2009 at 9:48 AM

I don't think that such an option would be of much help, and extra options make the tool harder to use. As noboby has argued strongly in favour of the well-formedness checks, I will remove them. Let's see how that works out.