fix(csharp): walk primary-constructor parameters for references and calls - #2836
Closed
brobl2008 wants to merge 1 commit into
Closed
fix(csharp): walk primary-constructor parameters for references and calls#2836brobl2008 wants to merge 1 commit into
brobl2008 wants to merge 1 commit into
Graphify Labs / Graphify Formal Verification
completed
Aug 17, 2026 in 0s
No divergence found (not a proof)
Compared 558df6d57d61cb6ef79c740ec7473c6d953d79a7 (base) against c097479b8552a01d37a4577bc9972ab4ccf9a142 (head).
Covered 3/15 changed functions (12 abstained, 0 never run)
| equivalent (proved) | distinguished | may-equivalent (sampled) | unsupported | error |
|---|---|---|---|---|
| 0 | 0 | 3 | 12 | 0 |
graphify/build\.py· build: unsupported — not verifiable: all 9 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)graphify/build\.py· build_from_json: unsupported — not verifiable: all 6 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly NameError — names the real obstacle, not a sampling gap)graphify/build\.py· build_merge: unsupported — parameter `graph_path` is annotated `str | Path | None` — outside the synthesizable primitive/collection setgraphify/dedup\.py· deduplicate_entities: unsupported — not verifiable: all 9 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly TypeError — names the real obstacle, not a sampling gap)graphify/detect\.py· _load_dir_own_ignore: unsupported — parameter `d` is annotated `Path` — outside the synthesizable primitive/collection setgraphify/detect\.py· _load_graphifyignore: unsupported — parameter `root` is annotated `Path` — outside the synthesizable primitive/collection setgraphify/extractors/engine\.py· _extract_generic: unsupported — parameter `path` is annotated `Path` — outside the synthesizable primitive/collection setgraphify/extractors/engine\.py· _java_annotation_names: unsupported — not verifiable: all 182 sampled inputs raised on both versions — the function never executed, so 'no divergence' would be vacuous (mostly AttributeError — names the real obstacle, not a sampling gap)graphify/extractors/engine\.py· _java_collect_type_refs: unsupported — parameter `skip` is annotated `frozenset[str] | None` — outside the synthesizable primitive/collection setgraphify/extractors/markdown\.py· extract_markdown: unsupported — parameter `path` is annotated `Path` — outside the synthesizable primitive/collection setgraphify/extractors/resolution\.py· _resolve_go_type_references: unsupported — parameter `root` is annotated `Path` — outside the synthesizable primitive/collection setgraphify/extractors/resolution\.py· _resolve_java_type_references: unsupported — non-vacuity: domain too small (only 1 distinct inputs exercised, need 3) — 'no divergence' would be near-vacuous
Backend availability notices:
- 2 changed test function(s) excluded from verification (a test is the oracle, not the subject)
Formal verification is advisory: equivalent is a proof over a bounded sound subset; may_equivalent is sampled, not proven; unsupported and error are honest abstentions.
Loading