Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | 1. Fix for free ensures in inlined procedures. Becomes a skip instead of an ↵ | 2012-06-01 | |
| | | | | | | | assume. 2. Fix for deterministic loop extraction, and a new regression. 3. All regressions (including Dafny) except houdini pass, it is most likely related to the free ensures change. | ||
* | Dafny: Created a branch for runtime checking. | 2012-06-01 | |
| | |||
* | Merge | 2012-05-31 | |
|\ | |||
* | | Dafny: Added map comprehensions and updated display syntax | 2012-05-31 | |
| | | |||
| * | GPUVerify: teach analyses, dualiser and race instrumenter about assigns with ↵ | 2012-05-31 | |
| | | | | | | | | multiple LHSs | ||
| * | added FindLeastToVerify to StratfiedVCGenBase as an abstract method | 2012-05-30 | |
| | | |||
| * | moved a couple of overrides from StratifiedVCGen to StratifiedVCGenBase | 2012-05-30 | |
| | | |||
| * | Merge | 2012-05-30 | |
| |\ | |||
| * | | added support for recordProcCallSites to new SI | 2012-05-30 | |
| | | | |||
| | * | GPUVerify: implement assume stealing in block predicator | 2012-05-30 | |
| |/ | |||
| * | GPUVerify: disable barrier divergence check in unstructured mode for now | 2012-05-30 | |
| | | |||
| * | GPUVerify: have shared state abstraction, race instrumenter reuse blocks | 2012-05-30 | |
| | | | | | | | | | | Since we do not update transfer commands, they would otherwise refer to old blocks. | ||
| * | GPUVerify: factor shared state abstraction for unstructured blocks | 2012-05-29 | |
| | | |||
| * | Boogie build succeeded | 2012-05-30 | |
| | | |||
| * | extra recursion bound | 2012-05-30 | |
| | | |||
| * | Merge | 2012-05-29 | |
| |\ | |/ |/| | |||
| * | further refactoring of SI; | 2012-05-29 | |
| | | | | | | | | removed the program argument to call to VerifyImplementation in Dafny | ||
* | | Merge | 2012-05-29 | |
|\ \ | |||
* | | | Dafny: fixed regression tests | 2012-05-29 | |
| | | | |||
* | | | Dafny: Added maps to regression tests. | 2012-05-29 | |
| | | | |||
| | * | Merge | 2012-05-29 | |
| | |\ | | |/ | |/| | |||
* | | | Dafny: fixed minor map related issues | 2012-05-29 | |
| | | | |||
| | * | Removed program argument from VerifyImplementation. It is redundant since ↵ | 2012-05-29 | |
| | | | | | | | | | | | | | | | | | | the constructor of ConditionGeneration takes a program reference and stashes it in a field. | ||
| * | | GPUVerify: factor the race instrumenter to handle unstructured blocks | 2012-05-29 | |
| | | | |||
| * | | GPUVerify: mark new work-item constants as non-unique | 2012-05-29 | |
| | | | |||
* | | | Dafny: Added compilation of finite maps | 2012-05-25 | |
| | | | |||
| * | | GPUVerify: in unstructured mode, disable uniformity analysis and return ↵ | 2012-05-25 | |
| | | | | | | | | | | | | conservative results | ||
| * | | GPUVerify: implement a set of BV operation constructors which insert a ↵ | 2012-05-25 | |
| |/ | | | | | | | function declaration if missing | ||
| * | Merge | 2012-05-28 | |
| |\ | |||
| * | | further refactoring | 2012-05-28 | |
| | | | |||
| | * | Boogie build succeeded | 2012-05-29 | |
| |/ | |||
| * | more refactoring | 2012-05-28 | |
| | | |||
| * | Merge | 2012-05-28 | |
| |\ | |||
| * | | removed call site simplification from the old SI flow | 2012-05-28 | |
| | | | |||
| | * | No need for extra attributes in ExtractLoops | 2012-05-28 | |
| | | | |||
| | * | updating FindLeastToVerify to the new flow | 2012-05-28 | |
| |/ | |||
| * | Merge | 2012-05-26 | |
| |\ | |||
| | * | Better interface for adding skipped calls, and | 2012-05-26 | |
| | | | | | | | | | | | | adding extra recursion bound to some procedures. | ||
| * | | Boogie build succeeded | 2012-05-26 | |
| |/ | |||
| * | Merge | 2012-05-25 | |
| |\ | |||
| * | | new stratified inlining (initial prototype) | 2012-05-25 | |
| | | | |||
| | * | Fixed the regression for deterministicExtractLoops. | 2012-05-25 | |
| | | | |||
* | | | Dafny: added finite maps | 2012-05-25 | |
| | | | |||
| | * | Merge | 2012-05-25 | |
| | |\ | |||
| | * | | Adding an option for deterministicExtractLoops, that uses an alternate way ↵ | 2012-05-25 | |
| | | | | | | | | | | | | | | | | | | | | | | | | to extract loops into procedures. Unsound for concurrency. Added a test in extractLoops directory. | ||
| | | * | GPUVerify: declarations of barrier, work-item constants no longer required; ↵ | 2012-05-25 | |
| | | | | | | | | | | | | | | | | GPUVerify will create them if not present | ||
| | | * | GPUVerify: add reference to Graph project | 2012-05-25 | |
| | | | | |||
| | | * | GPUVerify: add a MakeDual for unstructured blocks | 2012-05-25 | |
| | | | | |||
| | | * | GPUVerify: factor out the Cmd dualiser | 2012-05-24 | |
| | | | | |||
| | | * | GPUVerify: add block predicator | 2012-05-25 | |
| | | | |