feat: Verification coverage analysis for axioms #948
Conversation
|
Can you provide the Dafny code that uses this PR? Probably best to have working Dafny code before merging this, in particular because this PR does not add tests. |
Since this PR is an extension of an existing feature, it updates the tests for that feature to include the newly-covered case rather than adding new tests. It might still be worth having the Dafny side of this ready before merging. |
| axiomConjuncts.Add(translator.Translate(ax.Expr)); | ||
| var expr = translator.Translate(ax.Expr); | ||
| var assumeId = QKeyValue.FindStringAttribute(ax.Attributes, "id"); | ||
| if (assumeId != null && options.TrackVerificationCoverage) |
There was a problem hiding this comment.
Is there already code like this around somewhere else? If so can you prevent the duplication?
| @@ -226,7 +226,15 @@ public override void AddAxiom(Axiom ax, string attributes) | |||
| //Contract.Requires(ax != null); | |||
| base.AddAxiom(ax, attributes); | |||
|
|
|||
| axiomConjuncts.Add(translator.Translate(ax.Expr)); | |||
| var expr = translator.Translate(ax.Expr); | |||
| var assumeId = QKeyValue.FindStringAttribute(ax.Attributes, "id"); | |||
There was a problem hiding this comment.
Where does the magic constant "id" come from?
This PR enables verification coverage analysis for axioms.