Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands

boogie-org / boogie

Boogie

http://research.microsoft.com/en-us/projects/boogie/

MIT License

514 stars 112 forks source link

Introduce `{:isolate}` and `{:isolate "paths"}` attributes for assert and return commands #952

Closed keyboardDrummer closed 1 month ago

keyboardDrummer commented 1 month ago

Changes

Introduce the {:isolate} attribute on AssertCmd and ReturnCmd
Introduce the {:isolate "paths"} attribute on AssertCmd and ReturnCmd
Introduce new tokens that allow precisely describing where a particular Split comes from.
Fix a bug that caused too many VCs to be created when using /vcsSplitOnEveryAssert together with focus
Fix incorrect token bug for VCs originating from focus.

Testing

Created a folder Test/implementationDivision that has tests for {:isolate}, {:isolate "paths"}, {:focus} and {:split_here}

shazqadeer commented 3 weeks ago

@keyboardDrummer : Thank you for your continued contributions to Boogie. I am adding a late comment to this PR.

I notice that this PR adds a few more attributes related to VC splitting. Perhaps, the Dafny team has added other related attributes in the past also. Could you please make sure that all added attributes are documented in CommandLineOptions.cs? Thanks.

keyboardDrummer commented 3 weeks ago

@keyboardDrummer : Thank you for your continued contributions to Boogie. I am adding a late comment to this PR.

I notice that this PR adds a few more attributes related to VC splitting. Perhaps, the Dafny team has added other related attributes in the past also. Could you please make sure that all added attributes are documented in CommandLineOptions.cs? Thanks.

I've added some small documentation in https://github.com/boogie-org/boogie/pull/970