summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* deleted an unused classGravatar qadeer2012-06-12
* MergeGravatar qadeer2012-06-12
|\
* | refactoring in SIGravatar qadeer2012-06-12
| * Dafny: allow types to be qualified with the name of the module that declares ...Gravatar Unknown2012-06-11
| * Dafny: fixed bug in type cloning, as part of refinement machineryGravatar Unknown2012-06-11
| * Dafny: removed support for the old keyword "unlimited" (all functions are lim...Gravatar Unknown2012-06-11
| * GPUVerify: emit non-uniform loop candidate invariantGravatar Peter Collingbourne2012-06-11
| * GPUVerify: emit "uniform loop" candidate invariantGravatar Peter Collingbourne2012-06-11
| * GPUVerify: dualiser: preserve attributes of assert cmdGravatar Peter Collingbourne2012-06-11
| * GPUVerify: factor out CreateCandidateInvariant from AddCandidateInvariantGravatar Peter Collingbourne2012-06-11
| * GPUVerify: initialise invariantGenerationCounter in the constructor, rather t...Gravatar Peter Collingbourne2012-06-11
* | MergeGravatar qadeer2012-06-10
|\|
* | 1. changed new SI implemnetation so that it performs substitution for call sitesGravatar qadeer2012-06-10
| * 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
|/
* final (hopefully) fix to new SIGravatar qadeer2012-06-07
* 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
| * 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
|/ /
* | moved class Macro to AbsyGravatar qadeer2012-06-04
* | MergeGravatar qadeer2012-06-01
|\ \
* | | changed behavior of InlinedEnsures so that free ensures is skipped unless an ...Gravatar qadeer2012-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
* | | 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
| |\ \