summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Dafny: Added infrastructure for runtime checking.Gravatar chmaria2012-06-04
* Merge with defaultGravatar Unknown2012-06-01
|\
* | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an a...Gravatar Unknown2012-06-01
* | Dafny: Created a branch for runtime checking.Gravatar chmaria2012-06-01
| * GPUVerify: use Concat instead of PureCollections.Sequence.operator+Gravatar Peter Collingbourne2012-05-31
| * GPUVerify: resolve barrier implementation in unstructured modeGravatar Peter Collingbourne2012-05-31
| * GPUVerify: use a Formal for procedure predicatesGravatar Peter Collingbourne2012-05-31
|/
* 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
| * Boogie build succeededGravatar CodeplexBot2012-05-30
| * extra recursion boundGravatar akashlal2012-05-30
| * MergeGravatar qadeer2012-05-29
| |\ | |/ |/|
| * further refactoring of SI;Gravatar qadeer2012-05-29
* | MergeGravatar Unknown2012-05-29
|\ \
* | | Dafny: fixed regression testsGravatar Unknown2012-05-29
* | | Dafny: Added maps to regression tests.Gravatar 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
| |/
| * MergeGravatar qadeer2012-05-28
| |\
| * | further refactoringGravatar qadeer2012-05-28
| | * Boogie build succeededGravatar CodeplexBot2012-05-29
| |/
| * 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
| |/
| * MergeGravatar akashlal2012-05-26
| |\
| | * Better interface for adding skipped calls, andGravatar akashlal2012-05-26
| * | Boogie build succeededGravatar CodeplexBot2012-05-26
| |/
| * MergeGravatar qadeer2012-05-25
| |\
| * | new stratified inlining (initial prototype)Gravatar qadeer2012-05-25
| | * Fixed the regression for deterministicExtractLoops.Gravatar Unknown2012-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