This project is read-only.

Drop a warning?

Dec 15, 2009 at 10:35 PM


  equality and inequality have a higher priority than logical connectives in VCC, which would usually allow to leave out brackets in the invariants below, suppressing a lot of line noise. However, for booleans, VCC will output a warning (in struct S below). I don't think the warning is necessary, since one takes advantage of priorities as they are so often - what do others think?

  Best, Mark

#include "vcc.h"

struct S {
    bool a;
    invariant(a == a && a == a)

struct T {
    int a;
    invariant(a == a && a == a)
testcase(5,17) : warning VC0000: Operator '==' binds stronger than '&&' and '||' which is possibly not what you wanted;  use '<==>' or parenthesize the equality.
Verification of S#adm succeeded.
Verification of T#adm succeeded.

Dec 15, 2009 at 11:02 PM

I agree: VCC shouldn't warn when programmers use priorities to save brackets


Feb 4, 2010 at 1:11 PM
This discussion has been copied to a work item. Click here to go to the work item and continue the discussion.