Skip to content
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

Merged
merged 5 commits into from
Jan 26, 2024

Conversation

keyboardDrummer
Copy link
Collaborator

@keyboardDrummer keyboardDrummer commented Jan 26, 2024

Changes

  • Rename VCGen to VerificationConditionGenerator
  • Rename VerificationResult to ImplementationRunResult
  • Rename VCResult to VerificationRunResult
  • Move several classes into separate files: BlockListComparer, BlockStats, VerificationResultCollector
  • Move several methods from Split into several new files: BlockTransformation.cs, CommandTransformations.cs, ManualSplitFinder.cs and FocusAttribute.cs
  • Rename ConditionGeneration.Outcome to VcOutcome and move it to the outer scope
  • Move ProverInterface.Outcome to the outer scope

Testing

This is pure almost fully automated refactoring, so this is covered by existing automated tests

Copy link
Collaborator

@MikaelMayer MikaelMayer left a 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);
Copy link
Collaborator

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" ?

Copy link
Collaborator Author

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)
Copy link
Collaborator

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

Copy link
Collaborator Author

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:
Copy link
Collaborator

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?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Maybe already.. !

@keyboardDrummer keyboardDrummer merged commit 0efcb0b into boogie-org:master Jan 26, 2024
4 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants