Static Verifier: Status should be UNKNOWN when there are true and false reachable traces

[jezhiggins]

Consider

#include <assert.h>
int global;

int main(void) {
  int local;
  unsigned int nondet;

  local = 1;
  global = 1;

  if (nondet == 0)
    local = 2;
  if (nondet == 0)
    global = 2;

  assert(local == global);
}

Running goto-analyzer wrong.c --verify --recursive-interprocedural --vsd --loop-unwind-and-branching 10 gives

[main.assertion.1] line 21 assertion local == global: FAILURE (if reachable)

which is, to put it kindly, an overapproximation.

However running goto-analyzer wrong.c --verify --recursive-interprocedural --vsd` gives

[main.assertion.1] line 21 assertion local == global: UNKNOWN

which is as correct as that configuration can give.

There are four paths through the code. Two are safe (take both ifs, take neither if), but the two take-one-if paths (which are spurious) will definitely fail. In an ideal world they'd be blocked, but we are not yet in that world.

The static verifier does not account for this "might be a red path but that doesn't mean it fails because that path could be an over-approximation" and returned a FAILURE when an UNKNOWN would be more appropriate.

(In the test cases updated in this PR, there are existing comments articulating this same issue.)

[martin-cs]

Looks good; thanks.

[codecov]

Codecov Report

Merging #6286 (25e8895) into develop (c311ad1) will decrease coverage by 0.00%.
The diff coverage is 100.00%.

@@             Coverage Diff             @@
##           develop    #6286      +/-   ##
===========================================
- Coverage    75.98%   75.98%   -0.01%     
===========================================
  Files         1507     1507              
  Lines       163224   163222       -2     
===========================================
- Hits        124026   124024       -2     
  Misses       39198    39198              

Impacted Files	Coverage Δ
src/goto-programs/goto_program.h	89.34% <ø> (ø)
src/goto-analyzer/static_verifier.cpp	76.36% <100.00%> (-0.22%)	⬇️
src/goto-instrument/contracts/contracts.cpp	92.59% <100.00%> (ø)
unit/goto-instrument/cover_instrument.cpp	100.00% <100.00%> (ø)
unit/goto-programs/goto_program_validate.cpp	100.00% <100.00%> (ø)

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 43c7f71...25e8895. Read the comment docs.

[martin-cs]

I think the drop in the number of lines covered is because we have reformatted and so removed some lines. I am going to ignore it for the purpose of merging.

[jezhiggins]

I think the drop in the number of lines covered is because we have reformatted and so removed some lines. I am going to ignore it for the purpose of merging.

Yes, it's entirely an artefact of having applied clang-format-7 to static_verifier.cpp https://github.com/diffblue/cbmc/pull/6286/files#diff-da2927e58d056b5906c1ed62c21527e7db528c499359547ddaa6d7b86f680c14