summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an a...Gravatar Unknown2012-06-01
* MergeGravatar Unknown2012-05-31
|\
* | Dafny: Added map comprehensions and updated display syntaxGravatar Unknown2012-05-31
| * GPUVerify: teach analyses, dualiser and race instrumenter about assigns with ...Gravatar Peter Collingbourne2012-05-31
| * added FindLeastToVerify to StratfiedVCGenBase as an abstract methodGravatar qadeer2012-05-30
| * moved a couple of overrides from StratifiedVCGen to StratifiedVCGenBaseGravatar qadeer2012-05-30
| * MergeGravatar qadeer2012-05-30
| |\
| * | added support for recordProcCallSites to new SIGravatar qadeer2012-05-30
| | * GPUVerify: implement assume stealing in block predicatorGravatar Peter Collingbourne2012-05-30
| |/
| * GPUVerify: disable barrier divergence check in unstructured mode for nowGravatar Peter Collingbourne2012-05-30
| * GPUVerify: have shared state abstraction, race instrumenter reuse blocksGravatar Peter Collingbourne2012-05-30
| * GPUVerify: factor shared state abstraction for unstructured blocksGravatar Peter Collingbourne2012-05-29
| * extra recursion boundGravatar akashlal2012-05-30
| * MergeGravatar qadeer2012-05-29
| |\ | |/ |/|
| * further refactoring of SI;Gravatar qadeer2012-05-29
* | MergeGravatar Unknown2012-05-29
|\ \
| | * MergeGravatar qadeer2012-05-29
| | |\ | | |/ | |/|
* | | Dafny: fixed minor map related issuesGravatar Unknown2012-05-29
| | * Removed program argument from VerifyImplementation. It is redundant since th...Gravatar qadeer2012-05-29
| * | GPUVerify: factor the race instrumenter to handle unstructured blocksGravatar Peter Collingbourne2012-05-29
| * | GPUVerify: mark new work-item constants as non-uniqueGravatar Peter Collingbourne2012-05-29
* | | Dafny: Added compilation of finite mapsGravatar Unknown2012-05-25
| * | GPUVerify: in unstructured mode, disable uniformity analysis and return conse...Gravatar Peter Collingbourne2012-05-25
| * | GPUVerify: implement a set of BV operation constructors which insert a functi...Gravatar Peter Collingbourne2012-05-25
| |/
| * further refactoringGravatar qadeer2012-05-28
| * more refactoringGravatar qadeer2012-05-28
| * MergeGravatar qadeer2012-05-28
| |\
| * | removed call site simplification from the old SI flowGravatar qadeer2012-05-28
| | * No need for extra attributes in ExtractLoopsGravatar akashlal2012-05-28
| | * updating FindLeastToVerify to the new flowGravatar akashlal2012-05-28
| |/
| * Better interface for adding skipped calls, andGravatar akashlal2012-05-26
| * MergeGravatar qadeer2012-05-25
| |\
| * | new stratified inlining (initial prototype)Gravatar qadeer2012-05-25
* | | Dafny: added finite mapsGravatar Unknown2012-05-25
| | * MergeGravatar Unknown2012-05-25
| | |\
| | * | Adding an option for deterministicExtractLoops, that uses an alternate way to...Gravatar Unknown2012-05-25
| | | * GPUVerify: declarations of barrier, work-item constants no longer required; G...Gravatar Peter Collingbourne2012-05-25
| | | * GPUVerify: add reference to Graph projectGravatar Peter Collingbourne2012-05-25
| | | * GPUVerify: add a MakeDual for unstructured blocksGravatar Peter Collingbourne2012-05-25
| | | * GPUVerify: factor out the Cmd dualiserGravatar Peter Collingbourne2012-05-24
| | | * GPUVerify: add block predicatorGravatar Peter Collingbourne2012-05-25
| | | * GPUVerify: add an /unstructured command line optionGravatar Peter Collingbourne2012-05-25
| | |/ | |/|
| * | MergeGravatar qadeer2012-05-24
| |\|
| * | more refactoring in stratified inliningGravatar qadeer2012-05-24
| | * Boogie: document /typeEncoding:mGravatar Peter Collingbourne2012-05-22
| |/ |/|
* | Fix DomRelation.DominatedBy for the case where the dominator is the sourceGravatar Peter Collingbourne2012-05-22
|/
* MergeGravatar qadeer2012-05-21
|\
* | small fixGravatar qadeer2012-05-21
* | starting the implementation of the new stratified inlining APIGravatar qadeer2012-05-21
| * MergeGravatar Unknown2012-05-18
| |\ | |/ |/|