Lack of Documentation and Unclear Output for --verification-coverage-report

[ricostynha1]

There is very little documentation about the --verification-coverage-report flag (I’m aware there is already an open issue about this: [#5182].

I’m struggling to interpret the output, even for simple examples such as the following:

method Abs(x: int) returns (y: int)
  ensures x >= 0 ==> x == y
  ensures x < 0 ==> x + y == 0
{
  if x < 0 {
    return -x;
  } else {
    return x;
  }
}

Running:

dafny verify fileName --verification-coverage-report cov

produces an HTML file with the following color highlights:

method Abs(x: int) returns (y: int)
         red           yellow
  ensures x>=0 ==> x==y
         red          yellow
  ensures x<0 ==> x+y==0
{
  if x < 0 {
    return -x; // green line
  } else {
    return x; // yellow line
  }
}

From my understanding, a green line indicates that the code was used in a proof obligation ( which makes sense for return -x;.)
However, I would also expect the return x; line to be green, since commenting it out breaks verification. This suggests that it too should be part of a proof obligation.

In a simpler test without postconditions, both return -x and return x appear yellow. This makes me think that yellow might indicate code that isn’t used in any proof obligation, but in that case, what does red mean?

I’m also unsure how to interpret the coloring on postconditions. Initially, I thought that making use of the function (so that postconditions are “used” in a proof) would change their color to green. However, even after adding:

method test_abs() {
  var a := Abs(-7);
  assert 7 == a;
  var b := Abs(7);
  assert 7 == b;
}

…the colors on the postconditions remain unchanged: the left-hand sides of the implications are red, while the right-hand sides remain yellow.

Could someone clarify the intended meaning of these colors and how to interpret them correctly in verification coverage reports? Moreover, why not both lines are marked as green?