summaryrefslogtreecommitdiff
path: root/Test/og/lock.bpl
Commit message (Collapse)AuthorAge
* Enable as many "og" lit tests. Several fail because they weren'tGravatar Dan Liew2014-05-11
| | | | | | | | | | | | being executed previously! Boogie :: og/DeviceCacheSimplified.bpl Boogie :: og/DeviceCacheWithBuffer.bpl Boogie :: og/async.bpl Boogie :: og/houd1.bpl Boogie :: og/lock-introduced.bpl Boogie :: og/termination.bpl Boogie :: og/treiber-stack.bpl
* second checkpointGravatar qadeer2014-05-04
|
* checkpointGravatar qadeer2014-05-03
|
* added simulation relation computation to yield type checkingGravatar qadeer2014-04-20
| | | | updated the type check to incorporate {:terminates} annotation
* made some fixesGravatar qadeer2013-12-29
|
* various updates and tighter integration of QED stuff into mainlineGravatar qadeer2013-12-19
|
* fixes to type checking codeGravatar qadeer2013-12-11
|
* some refactoring of QED stuffGravatar qadeer2013-12-10
|
* first check inGravatar qadeer2013-12-04