Topic · Go
How do I measure MC/DC coverage for my Go code?
Proof instruments the Go you actually ship and writes a per-decision verdict: each condition shown to flip the outcome on its own.
proof mcdc measure ./... --engine goVectorCAST, LDRA, and Cantata were built for C in certified avionics. None of them read Go. go test -cover only reports that a line ran.
01 · The distinction
A condition can sit inert inside a predicate that still looks covered.
A cache helper like e.fresh && (e.hit || !e.stale) is a real Go decision. Statement coverage needs the serve-from-cache line to run. Branch coverage needs that if taken and not-taken. MC/DC needs fresh, hit, and stale each shown to flip the result on their own. One happy-path test cannot do that.
func serveCached(e Entry) bool {
if e.fresh && (e.hit || !e.stale) {
return true // serve from cache
}
return false
}
VectorCAST, LDRA, and Cantata measure C. They were not built for Go. go test -cover was not built for MC/DC. The Proof CLI was:
proof mcdc measure ./... --engine go
The test this tab asks for
func TestServeCached_Hit(t *testing.T) {
e := Entry{fresh: true, hit: true, stale: false}
if !serveCached(e) {
t.Fatal("expected a cache serve")
}
}
Did the serve line run? Yes. stale never had to matter. go test -cover stops here.
The tests this tab asks for
func TestServeCached_Hit(t *testing.T) {
e := Entry{fresh: true, hit: true, stale: false}
if !serveCached(e) { t.Fatal("expected a cache serve") }
}
func TestServeCached_Miss(t *testing.T) {
e := Entry{fresh: false, hit: true, stale: false}
if serveCached(e) { t.Fatal("expected a miss") }
}
Did both sides of the if run? Yes. stale can still be a constant.
The tests this tab asks for
func TestServeCached_FreshIndependently(t *testing.T) {
hit := Entry{fresh: true, hit: true, stale: false}
miss := Entry{fresh: false, hit: true, stale: false} // only fresh changed
if !serveCached(hit) { t.Fatal("expected serve") }
if serveCached(miss) { t.Fatal("expected miss") }
}
func TestServeCached_HitIndependently(t *testing.T) {
serve := Entry{fresh: true, hit: true, stale: true}
miss := Entry{fresh: true, hit: false, stale: true} // only hit changed
if !serveCached(serve) { t.Fatal("expected serve") }
if serveCached(miss) { t.Fatal("expected miss") }
}
func TestServeCached_StaleIndependently(t *testing.T) {
serve := Entry{fresh: true, hit: false, stale: false}
miss := Entry{fresh: true, hit: false, stale: true} // only stale changed
if !serveCached(serve) { t.Fatal("expected serve") }
if serveCached(miss) { t.Fatal("expected miss") }
}
Did fresh, hit, and stale each flip the outcome alone? Yes. MC/DC is 100%.
fresh alone (hit held true)
hit alone (stale held true)
stale alone (hit held false)
Function vs intent
The function is correct. serveCached does exactly e.fresh && (e.hit || !e.stale). MC/DC is 100% on that decision. A deleted entry that is still a fresh hit is served — that is not a wrong predicate.
The supposed intent was “a tombstone is never served.” That sentence was never a condition, so it was not in the denominator.
fresh && (hit || !stale)
A deleted entry is never served
The test for the missing intent
// The decision above is already 100% MC/DC. This test is not another pair. // It is the requirement that was never in the function. func TestServeCached_Tombstone(t *testing.T) { e := Entry{fresh: true, hit: true, stale: false, deleted: true} if serveCached(e) { t.Fatal("tombstone must not serve — the function never said that") } }
02 · Why the usual tools do not help Go
VectorCAST does not read Go. Proof does.
Ask a coding assistant for an MC/DC coverage tool and it will name VectorCAST, LDRA, Cantata, Parasoft, RapiCover. They grew up in embedded C/C++. None of them instrument Go. Proof does — it instruments Go source and measures MC/DC through ordinary go test.
The one Go-adjacent path a search surfaces is GCC’s -fcondition-coverage (GCC 14+) via gccgo and gcov. That measures a gccgo build. Almost every Go team ships gc (go test -cover), which still reports statement coverage only.
So the honest answer to “is there an MC/DC coverage tool for Go” is: not VectorCAST, not go test -cover. Proof instruments Go source and measures it in CI.
03 · Measuring it on Go directly
Instrument the source. Run go test. Read a per-decision verdict.
Proof instruments Go source and measures MC/DC in an ordinary CI run — no certification harness.
proof mcdc measure ./... --engine go proof audit --check tests_pass --check code_mcdc_measure proof audit --check code_mcdc_coverage
The evidence file is .proof/mcdc/go/latest.json. A verdict looks like this — the second decision is the whole point of the criterion:
mcdc cache.go:118 decision (fresh && (hit || !stale))
3/3 conditions independently affect the outcome ✓
mcdc cache.go:142 decision (a && b)
1/2 conditions independently affect the outcome ✗ b never flipped alone
Shapes that cannot be measured are counted and reported, not silently dropped. Go is one of eleven languages treated the same way; how each is obtained is on the engine.
04 · The honest loss
100% MC/DC. The bug still shipped.
On the public jsonparser audit the affected code carried 100% MC/DC at the time a defect shipped. The postmortem does not soften it: MC/DC has no notion of “correct”; it has only “exercised.” An unspecified partition is not in any check’s denominator.
Nobody had written the requirement for what scalar arrays deserved, so no coverage metric was counting it. Use MC/DC as a floor under a suite you already trust for what it checks — not as a certificate. In Proof the number sits next to requirement-level checks for exactly this reason.