locked
What is masked RRS feed

  • Question

  • I get a message "Checked 57 assertions: 50 correct (7 masked)". What the heck does "masked" mean? And how do I find out which assertions are correct and which are masked.

    It doesn't seem to matter what kinds of errors I introduce into my implementation, I don't seem to get any ensures clauses reported as incorrect. For the record, here is some of the code in question. Because the implementation is full of bugs, I would expect at least one ensures clause in bsearch to be flagged in some way, but they are not.

            static int bsearch(int t, int[] x)
            {
                // Pre: x != null
                Contract.Requires(x != null);
                // Pre: x is sorted nondescending
                Contract.Requires(Contract.ForAll(Enumerable.Range(0, x.Length-1), i => x[i] <= x[i + 1]));
                // Post: (exists i in {0,..x.Length}. x[i]==t) ==> 0 <= result && result < x.Length &&
                //                                                 x[result] == t 
                Contract.Ensures(Contract.ForAll(x, (z => z != t))
                              ||  0 <= Contract.Result<int>()
                                  && Contract.Result<int>() < x.Length
                                  && t == x[Contract.Result<int>()] );
                // Post: !(exists i in {0,..x.Length}. x[i]==t) ==> result == -1
                Contract.Ensures(!Contract.ForAll(x, (z => z != t)) || Contract.Result<int>() == -1);
                int p = 0;
                int q = x.Length;
                // Invariant: (exists i in {0,..x.length}. x(i)==t) ==> (exists i in {p,..q}. x[i]==t)
                while(true) {
                    Contract.Assert(Contract.ForAll(x, (z => z != t))
                                 || Contract.Exists(Enumerable.Range(p, q - p), (i => x[i] == t)));
                    if (q - p <= 2) break;
                    int variant0 = q - p;
                    int m = between(p, q);
                    if( t < x[m] ) q = m-1 ;
                    else p = m+1;
                    int variant = q - p;
                    Contract.Assert(variant < variant0);
                }
                if( p==q ) return -1 ;
                else if( x[p] == t ) return p ;
                else return -2 ;
            }
    
            static int between(int p, int q)
            {
                Contract.Requires(q - p > 1);
                Contract.Ensures(p < Contract.Result<int>() && Contract.Result<int>() < q);
                return p + (q - p) / 2;
            }
    

    • Edited by Theodore Norvell Monday, September 16, 2013 3:19 AM Errors in earlier version.
    Monday, September 16, 2013 1:59 AM

Answers

  • "(masked)" is the number of alarms that the static checker would show without any filter.

    We have two kinds of filters:

    1. thresholds: the low, medium etc. The checker gives a score to each warning, and if the score is not good enough for a given warning level, it masks the warning

    2. SuppressMessage: It may happen that the contract is out of the reach of the checker (e.g., the loop invariant in your example). In this case you can explicitly say to the checker to mask the warning, using the SuppressMessage attribute (details in the doc)

    ciao

    f

    Monday, September 30, 2013 10:20 PM

All replies

  • To partly answer my own question: After setting the "warning level" property to "hi" on the code contracts tab of the properties pane, there were no more "masked" assertions. The assertions that were previously "masked" now appear as either "correct" or "unproven".
    Tuesday, September 17, 2013 11:11 AM
  • "(masked)" is the number of alarms that the static checker would show without any filter.

    We have two kinds of filters:

    1. thresholds: the low, medium etc. The checker gives a score to each warning, and if the score is not good enough for a given warning level, it masks the warning

    2. SuppressMessage: It may happen that the contract is out of the reach of the checker (e.g., the loop invariant in your example). In this case you can explicitly say to the checker to mask the warning, using the SuppressMessage attribute (details in the doc)

    ciao

    f

    Monday, September 30, 2013 10:20 PM
  • Thanks for the answer.  It seems to me the default should be "hi".
    Wednesday, October 2, 2013 8:40 PM
  • Well, it depends... On large codebases hi will provide you too many warnings.

    Low allows you to focus on the high-priority problems.

    The rule of thumb is that low identifies important problems in your code, medium/medium high requires some annotation effort, and hi requires an even stronger annotation effort.

    ciao

    f

    Wednesday, October 2, 2013 8:57 PM