Skip to content

Tags: boogie-org/boogie

Tags

v3.1.6

Toggle v3.1.6's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Remove code that causes memory leaks (#888)

### Changes
- Replace two usages of `ConcurrentBag` with `ConcurrentStack`, which
has a much simpler implementation that has no risk of memory leaks.
ConcurrentBag was causing leaks. More information is here:
https://stackoverflow.com/questions/5353164/possible-memoryleak-in-concurrentbag
- Remove cancellation support from AsyncQueue, since the cancellation
token would gain a reference to the item being dequeued, which a caller
might not expect and which causes a memory leak if the cancellation
token is kept alive.
- Add a 'Clear' method to 'AsyncQueue' to allow cancelling all customers
- Fix a surprising memory leak in `CustomStackSizePoolTaskScheduler`
- Enable using an ExecutionEngine with a custom TaskScheduler

### Testing
- Tested with a profiler that the above changes resolve the issue that
each Boogie program created by Dafny was never garbage collected.

v3.1.5

Toggle v3.1.5's commit message
Release version 3.1.5

v3.1.4

Toggle v3.1.4's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Add missing string interpolation (#865)

The fact that we didn't detect this earlier makes it clear that this
functionality wasn't being tested. Unfortunately, it's not immediately
clear to me how to write a test that would exercise the relevant code.

This should fix #863, even though we don't have tests to confirm that.

v3.1.3

Toggle v3.1.3's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Fix crash on low rlimit (#859)

Z3 has multiple ways of responding that the resource limit has been
exceeded. In some cases it responds with an error message including
"push canceled". This updates Boogie to handle more of the strange side
cases.

v3.1.2

Toggle v3.1.2's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Reset predecessors before focusing (#856)

There are two calls to `FocusAndSplit` in Boogie. Before one, there was
already a call to `ResetPredecessors`, but not before the other. Now
they both work on an implementation where the `Predecessors` attributes
has been reset.

---------

Co-authored-by: Remy Willems <rwillems@amazon.com>

v3.1.1

Toggle v3.1.1's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Copy split index when cloning split (#854)

v3.1.0

Toggle v3.1.0's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
[Civl] Fixed bug in refinement check for actions (#853)

The refinement check for actions was handling the frame condition
correctly. Now the frame condition is handled in the same manner as the
refinement check for procedures.

Co-authored-by: Shaz Qadeer <shaz@meta.com>

v3.0.12

Toggle v3.0.12's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Allow `/prune:0` to disable pruning (#848)

Add a `/noprune` flag to turn off pruning. It's off by default, but this
can be convenient if a) it's turned on earlier on the command line, or
b) Boogie is being used from another system like Dafny.

I would have made it `/prune:{1,0}`, but it's harder to make that
backward compatible with the current behavior.

v3.0.11

Toggle v3.0.11's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Verification task per split (#841)

Dependent Dafny PR: dafny-lang/dafny#5031

### Changes
- Change the API `executionEngine.GetImplementationTasks` to
`executionEngine.GetVerificationTasks`, which returns a task for each
statically defined assertion batch. When using the split on every assert
option, this will return a verification task for each assertion.

### Testing
- Added test SplitOnEveryAssertion

---------

Co-authored-by: Aaron Tomb <aarotomb@amazon.com>

v3.0.10

Toggle v3.0.10's commit message

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature.
Update Version to 3.0.10 (#837)