summaryrefslogtreecommitdiff
path: root/Source/GPUVerify
Commit message (Expand)AuthorAge
* GPUVerify: add an option which controls whether to use smart predicationGravatar Peter Collingbourne2012-07-30
* Implemented Houdini-based pointer analysis. Made inter-group race checking d...Gravatar Unknown2012-07-20
* GPUVerify only generates _READ/WRITE_OFFSET variabls if they do not already e...Gravatar Unknown2012-07-17
* MergeGravatar Unknown2012-07-10
|\
* | Read and write logging variables are now only generated if they do not alread...Gravatar Unknown2012-07-10
| * GPUVerify: merge blocks into predecessors before and after predicationGravatar Peter Collingbourne2012-07-09
|/
* Worked on cross-thread annotations.Gravatar Unknown2012-07-03
* Reinstate GPUVerify filesGravatar Peter Collingbourne2012-07-02
* MergeGravatar Unknown2012-07-02
|\
* | Started adding support for annotation intrinsics for unstructured programs.Gravatar Unknown2012-07-02
| * MergeGravatar Jason Koenig2012-06-28
| |\ | |/ |/|
| * Dafny: MergeGravatar Jason Koenig2012-06-27
| |\
* | | GPUVerify: modify the variable definition analysis to track and reject self-r...Gravatar Peter Collingbourne2012-06-27
| |/ |/|
* | GPUVerify: when building offset predicates, skip unsubstitutable offsetsGravatar Peter Collingbourne2012-06-27
* | GPUVerify: use original expression for undefined variablesGravatar Peter Collingbourne2012-06-27
* | GPUVerify: implement generic reduced strength analysis for loop countersGravatar Peter Collingbourne2012-06-26
* | GPUVerify: fix UnstructuredRegion.CmdsChildRegionsGravatar Peter Collingbourne2012-06-26
* | Reinstated support for barrier flags.Gravatar Unknown2012-06-27
* | Undo bad merge.Gravatar afd2012-06-27
* | MergeGravatar Unknown2012-06-26
|\ \
* | | Added support for barrier flags.Gravatar Unknown2012-06-26
* | | MergeGravatar Unknown2012-06-25
|\ \ \
| | * | GPUVerify: factor all offset predicate handling code into a central locationGravatar Peter Collingbourne2012-06-25
| | * | GPUVerify: merge ElementEncodingRaceInstrumenter into RaceInstrumenterGravatar Peter Collingbourne2012-06-22
| |/ /
| * | GPUVerify: implement generic stride constraint generationGravatar Peter Collingbourne2012-06-22
| * | GPUVerify: make VarDefAnalysis capable of analysing non-constantsGravatar Peter Collingbourne2012-06-22
| * | GPUVerify: construct BV*_AND and BV*_SUB using MakeBVFunctionCallGravatar Peter Collingbourne2012-06-21
| * | GPUVerify: replace MayBe{ThreadConfigurationVariable,Gid}Analyser with simple...Gravatar Peter Collingbourne2012-06-21
* | | MergeGravatar Unknown2012-06-21
|\ \ \
| | * | GPUVerify: make BuildNamedDefVisitor and SubstDualisedDefVisitor DuplicatorsGravatar Peter Collingbourne2012-06-20
| |/ /
| * / GPUVerify: fix constant offset invariant generation for the case where no con...Gravatar Peter Collingbourne2012-06-20
| |/
| * Move block predicator to VCGenerationGravatar Peter Collingbourne2012-06-18
| * GPUVerify: block predicator: add a mode which disables procedure predicatesGravatar Peter Collingbourne2012-06-18
* | Merge with dafny_runtime_checkingGravatar Unknown2012-06-18
|\|
* | Added command line option.Gravatar Unknown2012-06-18
| * GPUVerify: implement is-a-constant analysisGravatar Peter Collingbourne2012-06-15
| * GPUVerify: revert ac36537a0eb8, as this is in fact a candidate invariant (e.g...Gravatar Peter Collingbourne2012-06-15
| * GPUVerify: when dualising assume and assert statements, emit two statements i...Gravatar Peter Collingbourne2012-06-15
|/
* Inter-thread race checking implementation done.Gravatar Unknown2012-06-14
* Fix for structured regions.Gravatar Unknown2012-06-14
* Progress on inter-group race checkingGravatar Unknown2012-06-14
* MergeGravatar Unknown2012-06-14
|\
* | Started work on inter-group race checking.Gravatar Unknown2012-06-14
| * GPUVerify: the non-uniform loop invariant is not a candidate invariantGravatar Peter Collingbourne2012-06-12
| * 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
|/
* GPUVerify: teach the array control flow analyser to handle unstructured programsGravatar Peter Collingbourne2012-06-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 18:54:45 +0000