Skip to content
New issue

Have a question about this project? # for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “#”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? # to your account

Extract refactorings from #952 #957

Merged
merged 8 commits into from
Oct 3, 2024

Conversation

keyboardDrummer
Copy link
Collaborator

No description provided.

@keyboardDrummer keyboardDrummer enabled auto-merge (squash) October 2, 2024 11:26
@keyboardDrummer keyboardDrummer changed the title Extract refactorings from https://github.com/boogie-org/boogie/pull/952 Extract refactorings from #952 Oct 3, 2024
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.

Refactorings look good.

@@ -166,7 +167,7 @@ public HoudiniSession(Houdini houdini, VerificationConditionGenerator vcgen, Pro
collector = new VerificationResultCollector(houdini.Options);
collector.OnProgress?.Invoke("HdnVCGen", 0, 0, 0.0);

vcgen.ConvertCFG2DAG(run, taskID: taskID);
new RemoveBackEdges(vcgen).ConvertCfg2Dag(run, taskID: taskId);
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nit: style and maintenance. A more discoverable IMO would be to declare a method on vcgen named "RemoveBackEdges() thar calls and return new RemoveBackEdges(this)

@@ -18,20 +18,20 @@ void ObjectInvariant()
}


public CallCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, AssertRequiresCmd assertRequiresCmd, Model model,
public CallCounterexample(VCGenOptions options, List<Block> trace, List<object> augmentedTrace, AssertRequiresCmd failingAssertRequires, Model model,
Copy link
Collaborator

Choose a reason for hiding this comment

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

Nice renaming that brings some meaning.

}

blockMap[(Block) bl] = auxNewBlock;
continue;
Copy link
Collaborator

Choose a reason for hiding this comment

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

Indentation saver !

@keyboardDrummer keyboardDrummer merged commit 9a8ce8d into boogie-org:master Oct 3, 2024
5 checks passed
@keyboardDrummer keyboardDrummer deleted the refactor branch October 3, 2024 14:55
# for free to join this conversation on GitHub. Already have an account? # to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants