Skip to content

Boogie

Compare
Choose a tag to compare
@github-actions github-actions released this 01 Jun 09:05
· 200 commits to master since this release
v2.16.8
38b0d21
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode. 
Fix to Lheap_Add translation (#740)

Lheap_Add primitive adds a cell to a linear heap. This PR changes the
translation so that only the domain of the target heap is modified. The
heap contents is assumed (magically) to contain the value being inserted
at the fresh address. This is sound because Ref T, the address type for
Lheap T is uninterpreted and potentially infinite source of cells with a
particular value.
Assets 15
Loading