summaryrefslogtreecommitdiff
path: root/Test/og/ticket.bpl
Commit message (Collapse)AuthorAge
* renamed og to civlGravatar qadeer2015-04-22
|
* strengthened type checkingGravatar qadeer2014-12-26
| | | | | cleaned up the generation of mover checks (based on example from Chris) added two examples from Chris to regressions
* changed type checking of yield procedures so that they can only call other ↵Gravatar qadeer2014-12-18
| | | | yielding procedures
* 1. made variable introduction layer explicit in the test casesGravatar qadeer2014-12-15
| | | | 2. if a single layer is specified for a global variable, that layer is the introduction layer
* renamed :phase to :layerGravatar qadeer2014-11-14
|
* deleted the free assume about gates after parallel callsGravatar qadeer2014-07-26
|
* updated the linear type system based on Chris' design with linear, ↵Gravatar qadeer2014-07-15
| | | | linear_in, linear_out
* simplified yield type chcking and added treiber stack (not fully done)Gravatar qadeer2014-07-15
|
* Fix lit test suite when running Boogie under a path that containsGravatar Dan Liew2014-05-27
| | | | spaces.
* 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 variable hidingGravatar qadeer2014-04-16
| | | | added annotation on an atomic action about the phases in which it exists
* new design for linear types + VCgenGravatar qadeer2014-02-07
| | | | | ported all the examples added the QED examples to runtest.bat
* small update to the exampleGravatar qadeer2014-01-09
|
* a fix regarding the checking of assertions in atomic specs at call sitesGravatar qadeer2014-01-08
|
* first cut of refinement checkingGravatar qadeer2014-01-07
|
* some more fixes to examplesGravatar qadeer2014-01-02
|
* fixed examples to deal with yield type checking errorsGravatar qadeer2014-01-01
|
* more bug fixesGravatar qadeer2013-12-24
| | | | updates to DeviceCache.bpl to make it verify
* bug fixes in Duplicate.cs and parsing of invariant attributesGravatar qadeer2013-12-22
| | | | other bug fixes in QED stuff
* various updates and tighter integration of QED stuff into mainlineGravatar qadeer2013-12-19
|
* added syntax for par call and ParCallCmdGravatar qadeer2013-12-16