Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Move block predicator to VCGeneration | 2012-06-18 | |
| | |||
* | GPUVerify: block predicator: add a mode which disables procedure predicates | 2012-06-18 | |
| | | | | | This mode also conditionalises if statements to avoid problems with recursion. | ||
* | GPUVerify: revert ac36537a0eb8, as this is in fact a candidate invariant ↵ | 2012-06-15 | |
| | | | | | | (e.g. consider a loop within a conditional) Pointed out by Ally. | ||
* | GPUVerify: the non-uniform loop invariant is not a candidate invariant | 2012-06-12 | |
| | | | | Thanks to Ally for pointing this out. | ||
* | GPUVerify: emit non-uniform loop candidate invariant | 2012-06-11 | |
| | |||
* | GPUVerify: emit "uniform loop" candidate invariant | 2012-06-11 | |
| | |||
* | GPUVerify: fix line endings | 2012-06-08 | |
| | |||
* | GPUVerify: block predicator: use the name '_P' for the procedure predicate ↵ | 2012-06-07 | |
| | | | | for consistency with the structured predicator | ||
* | GPUVerify: emit assumes for backedges | 2012-06-07 | |
| | | | | | | Specifically, have the predicator emit backedge assumes with a :backedge attribute, and have the dualiser recognise such assumes and create an OR expression instead of an AND expression. | ||
* | GPUVerify: use Concat instead of PureCollections.Sequence.operator+ | 2012-05-31 | |
| | |||
* | GPUVerify: use a Formal for procedure predicates | 2012-05-31 | |
| | |||
* | GPUVerify: implement assume stealing in block predicator | 2012-05-30 | |
| | |||
* | GPUVerify: add block predicator | 2012-05-25 | |