-
Notifications
You must be signed in to change notification settings - Fork 112
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Some refactoring in the VCGeneration assembly #840
Some refactoring in the VCGeneration assembly #840
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is improving maintenance, thanks. A few suggestions to piggy-back on your effort.
@@ -1331,7 +1331,7 @@ private static void UpdateStatistics(PipelineStatistics stats, VC.VCGen.Outcome | |||
continue; | |||
} | |||
|
|||
var errorInfo = error.CreateErrorInformation(outcome, Options.ForceBplErrors); | |||
var errorInfo = error.CreateErrorInformation(vcOutcome, Options.ForceBplErrors); |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm reading all these vcOutcome, since you are doing refactoring, would it make sense to remove the abbreviation and name this "verificationConditionOutcome" or just "verificationOutcome" ?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'm not sure about that rename. I'll leave it for another time.
@@ -158,7 +158,7 @@ public override void UpdateImplementation(Implementation implementation) | |||
curImp = implementation; | |||
} | |||
|
|||
public override void UpdateOutcome(ProverInterface.Outcome o) | |||
public override void UpdateOutcome(Outcome o) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
And this one could be renamed ProverOutcome for disambiguation with the other VcOutcome
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Made a fresh PR
return Outcome.Inconclusive; | ||
case ProverInterface.Outcome.Valid: | ||
return Outcome.Correct; | ||
case Microsoft.Boogie.Outcome.Invalid: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you give a specific name for Outcome, you would not need the prefix Microsoft.Boogie, right?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Maybe already.. !
Changes
ConditionGeneration.Outcome
toVcOutcome
and move it to the outer scopeProverInterface.Outcome
to the outer scopeTesting
This is pure almost fully automated refactoring, so this is covered by existing automated tests