summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Dafny: types can now be qualified with full module pathsGravatar Jason Koenig2012-07-06
* Dafny: datatype constructors can be accessed across module boundaries.Gravatar Jason Koenig2012-07-06
* Dafny: fixed a crash in datatype argument resolutionGravatar Jason Koenig2012-07-05
* MergeGravatar Jason Koenig2012-07-05
|\
* | Dafny: Fixed bug in autocontracts where the post resolver was run even if the...Gravatar Jason Koenig2012-07-05
* | Dafny: disallow importing ghost modules into physical ones.Gravatar Jason Koenig2012-07-05
| * Made error trace generation (without labels) more general for stratifiedGravatar Unknown2012-07-04
|/
* Dafny: added static members of _default to the module level scope, at low pri...Gravatar Jason Koenig2012-07-03
* MergeGravatar Jason Koenig2012-07-03
|\
| * Dafny: added support for nested abstract modules, fixed some translation issuesGravatar Jason Koenig2012-07-03
* | Worked on cross-thread annotations.Gravatar Unknown2012-07-03
| * 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