summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
...
| | | * Dafny: re-added field non-uniqueness (was accidentally reverted by a bad merge)Gravatar Jason Koenig2012-07-02
| | |/
* | | MergeGravatar Unknown2012-07-02
|\ \ \ | | |/ | |/|
| * | Reinstate GPUVerify filesGravatar Peter Collingbourne2012-07-02
| * | MergeGravatar Jason Koenig2012-07-02
| |\ \
| | * | Dafny: reinstated autocontractsGravatar Jason Koenig2012-07-02
* | | | Added support for non-predicated assertionsGravatar Unknown2012-07-02
|/ / /
* | | MergeGravatar Unknown2012-07-02
|\ \ \ | | |/ | |/|
* | | Started adding support for annotation intrinsics for unstructured programs.Gravatar Unknown2012-07-02
| | * MergeGravatar Jason Koenig2012-06-29
| |/|
| * | Dafny: updated contracts to allow null parent (of the default module)Gravatar Rustan Leino2012-06-29
| * | MergeGravatar Jason Koenig2012-06-28
| |\ \ | |/ / |/| |
| * | Dafny: fixed up test suite (temporarily removed autocontract tests)Gravatar Jason Koenig2012-06-28
| | * Boogie: formated elapsed timeGravatar Jason Koenig2012-06-28
| |/ |/|
| * Dafny: fixed bug with translation of class._System.object;Gravatar Jason Koenig2012-06-28
| * Dafny: MergeGravatar Jason Koenig2012-06-27
| |\
| * | Dafny: fixed bug in which _module scope declarations were not verified.Gravatar Jason Koenig2012-06-27
| * | Dafny: Fixed module bugsGravatar 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
| * Dafny: Implemented abstract modulesGravatar Jason Koenig2012-06-26
* | GPUVerify: implement generic reduced strength analysis for loop countersGravatar Peter Collingbourne2012-06-26
* | GPUVerify: fix UnstructuredRegion.CmdsChildRegionsGravatar Peter Collingbourne2012-06-26
* | Model: sort variables by nameGravatar 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
| |/ /
| * | Dafny: now, equality-support determination and checking feels ripe; so, codat...Gravatar Rustan Leino2012-06-22
| * | MergeGravatar Unknown2012-06-22
| |\ \
| * | | Dafny: mark code for equality-support determination tentativeGravatar Unknown2012-06-22
| * | | Dafny: equality-support test cases. This is just a snapshot--some things sti...Gravatar Unknown2012-06-22
| * | | Dafny: added contracts to IRewriter methodsGravatar Unknown2012-06-22
| * | | Dafny: allow "assume ..." as a refining statement (provided it replaces an "a...Gravatar Unknown2012-06-22
| * | | Dafny: deal with equality-support issues in refinementsGravatar Unknown2012-06-22
| | * | GPUVerify: implement generic stride constraint generationGravatar Peter Collingbourne2012-06-22
| | * | GPUVerify: make VarDefAnalysis capable of analysing non-constantsGravatar Peter Collingbourne2012-06-22
| | * | Dafny: Fixed bug in CompilerizeName.Gravatar chmaria2012-06-22
| | * | Dafny: fixed two contractsGravatar Rustan Leino2012-06-22
| * | | Dafny: Since it's no longer true that all types support equality at run-time ...Gravatar Unknown2012-06-21
| | * | 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
| | * | merge with Peter's changesGravatar qadeer2012-06-20
| | * | MergeGravatar qadeer2012-06-20
| | |\ \ | | |/ / | |/| |
| * | | GPUVerify: fix constant offset invariant generation for the case where no con...Gravatar Peter Collingbourne2012-06-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-12 17:18:32 +0000