summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* refactoring in SIGravatar qadeer2012-06-12
* MergeGravatar qadeer2012-06-10
|\
* | 1. changed new SI implemnetation so that it performs substitution for call sitesGravatar qadeer2012-06-10
| * Dafny: added some test programsGravatar Rustan Leino2012-06-08
| * Dafny/Boogie/BVD: made Dafny plug-in for BVD work againGravatar Rustan Leino2012-06-08
| * GPUVerify: teach the array control flow analyser to handle unstructured programsGravatar Peter Collingbourne2012-06-08
| * GPUVerify: if one input file is supplied, choose output file name more intell...Gravatar Peter Collingbourne2012-06-08
| * GPUVerify: fix line endingsGravatar Peter Collingbourne2012-06-08
| * Chalice build succeededGravatar CodeplexBot2012-06-08
|/
* MergeGravatar qadeer2012-06-07
|\
* | final (hopefully) fix to new SIGravatar qadeer2012-06-07
| * Boogie build succeededGravatar CodeplexBot2012-06-08
|/
* testing a fix in SIGravatar qadeer2012-06-07
* Merging againGravatar Ken McMillan2012-06-07
|\
* | GPUVerify: have StripThreadIdentifiers deal properly with identifiers contain...Gravatar Peter Collingbourne2012-06-07
* | GPUVerify: block predicator: use the name '_P' for the procedure predicate fo...Gravatar Peter Collingbourne2012-06-07
* | GPUVerify: re-introduce the non-divergence check in unstructured modeGravatar Peter Collingbourne2012-06-07
* | GPUVerify: emit assumes for backedgesGravatar Peter Collingbourne2012-06-07
* | GPUVerify: refactor candidate invariant generators and analyses to use regionsGravatar Peter Collingbourne2012-06-07
* | Automatic merge.Gravatar stefanheule2012-06-07
|\ \
* | | Chalice: Remove IsGoodState as it is not needed and causes problems in certai...Gravatar stefanheule2012-06-07
| | * Trying to merge with recent changes, failing.Gravatar Ken McMillan2012-06-05
| | |\
| | | * Some changes to support expanded use of z3api.Gravatar Ken McMillan2012-06-05
| * | | GPUVerify: recognise offsets in forms other than that produced by the old fro...Gravatar Peter Collingbourne2012-06-01
| * | | GPUVerify: have dualiser reuse blocksGravatar Peter Collingbourne2012-06-07
| * | | GPUVerify: add newly created barrier procedures to resolution contextGravatar Peter Collingbourne2012-06-07
| * | | MergeGravatar Jason Koenig2012-06-06
| |\ \ \
| * | | | Dafny: change labels to use a generic singly linked listGravatar Jason Koenig2012-06-06
| | * | | GPUVerify: fix bug which caused us to log accesses at the end of the block, r...Gravatar Peter Collingbourne2012-06-06
| |/ / /
| * | | Boogie: add /printCFG command line option, which prints each implementation's...Gravatar Peter Collingbourne2012-06-06
| * | | Bug fix with mvInfo during VCGenGravatar akashlal2012-06-06
| * | | update to SIGravatar qadeer2012-06-04
| |/ /
| * | MergeGravatar qadeer2012-06-04
| |\ \
| * | | moved class Macro to AbsyGravatar qadeer2012-06-04
| | * | Chalice build succeededGravatar CodeplexBot2012-06-04
| |/ / |/| |
* | | Chalice: Add regression test for unfolding expressions in predicates.Gravatar stefanheule2012-06-03
* | | Chalice: Allow unfolding expressions in predicates (this fixes workitem 10223).Gravatar stefanheule2012-06-03
* | | Chalice: Add regression test case for disallowed 'waitlevel' in predicates.Gravatar stefanheule2012-06-03
* | | Chalice: Disallow 'waitlevel' in predicates.Gravatar stefanheule2012-06-03
|/ /
* | When translating an assighment, leave the source of the assignment on theGravatar Unknown2012-06-02
* | MergeGravatar Unknown2012-06-02
|\ \
* | | Don't add dummy modules (resulting from a failed load) to the list of modulesGravatar Unknown2012-06-02
| * | Boogie build succeededGravatar CodeplexBot2012-06-02
| * | MergeGravatar qadeer2012-06-01
| |\ \
| * | | changed behavior of InlinedEnsures so that free ensures is skipped unless an ...Gravatar qadeer2012-06-01
| | * | Merge with dafny_runtime_checking. Essentially, the fixes for free ensures an...Gravatar Unknown2012-06-01
| |/| |
| | * | 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