| Commit message (Expand) | Author | Age |
* | Merge | Rustan Leino | 2011-11-15 |
|\ |
|
* | | Added Dafny solutions to the VSTTE 2012 program verification competition | Rustan Leino | 2011-11-15 |
| * | Merge | qadeer | 2011-11-15 |
| |\ |
|
| * | | changed inlining code so that candidate preconditions and postconditions are ... | qadeer | 2011-11-15 |
| | * | Some fixes for race checking contracts | Unknown | 2011-11-15 |
| | * | Modified solution to build on all platforms. | Unknown | 2011-11-15 |
| |/ |
|
* | | Dafny: added let expressions (syntax: "var x := E0; E1") | Rustan Leino | 2011-11-14 |
| * | Merge | qadeer | 2011-11-14 |
| |\ |
|
| * | | fixed another bug in model parser related to datatype values | qadeer | 2011-11-14 |
| | * | For some reason, these didn't get into the last commit. | Mike Barnett | 2011-11-14 |
| | * | Trying to get the generics translation correct... | Mike Barnett | 2011-11-14 |
| |/ |
|
| * | added the option /inlineDepth:n. This option defaults to -1. If the user prov... | qadeer | 2011-11-13 |
| * | Boogie build succeeded | CodeplexBot | 2011-11-12 |
* | | Dafny: implemented the wellformedness check that datatype destructors are onl... | Rustan Leino | 2011-11-11 |
|/ |
|
* | Merge | qadeer | 2011-11-11 |
|\ |
|
| * | moved the addition of selectors and testers to program.Resolve | qadeer | 2011-11-11 |
* | | Produce unsat cores only when enabled (in stratified inlining) | Unknown | 2011-11-11 |
|/ |
|
* | Many, many bug fixes related to generics and some other random problems. | Mike Barnett | 2011-11-10 |
* | Dafny: allow assert/assume expressions in more places | Rustan Leino | 2011-11-09 |
* | Dafny: added assert/assume expressions | Rustan Leino | 2011-11-09 |
* | Merge | qadeer | 2011-11-09 |
|\ |
|
* | | copied all attributes of the constructor (except for :constructor) to the sel... | qadeer | 2011-11-09 |
| * | VCC: remove _vcc_math_type_ from type names | Michal Moskal | 2011-11-09 |
| * | VCC: hide #limited# functions | Michal Moskal | 2011-11-09 |
| * | Merge | Rustan Leino | 2011-11-09 |
| |\ |
|
| * | | Dafny: moved definition of class.array into prelude, anticipating writing axi... | Rustan Leino | 2011-11-09 |
| * | | Dafny: allow single-quote as a character in identifiers in the VS2010 mode | Rustan Leino | 2011-11-09 |
| * | | Dafny: added "multiset" keyword to syntax highlighting in emacs, vim, latex, VSX | Rustan Leino | 2011-11-09 |
| | * | Refactoring, and work on race checking contracts | Unknown | 2011-11-09 |
| |/ |
|
| * | Merge | Rustan Leino | 2011-11-09 |
| |\ |
|
| * | | Dafny: fixed part of a type-inference issue with datatypes and the < operator... | Rustan Leino | 2011-11-09 |
| | * | Tagging EMIC CC.NET build 2.1.31109.0 | VccBuildServer | 2011-11-09 |
| | * | BVD: don't do the "Duplicate entry exception"; uncomment for debugging | Michal Moskal | 2011-11-08 |
| | * | VCC: show output parameters as roots | Michal Moskal | 2011-11-08 |
| |/
|/| |
|
* | | moved GPUVerify into its own solution | qadeer | 2011-11-08 |
|/ |
|
* | Merge | Rustan Leino | 2011-11-08 |
|\ |
|
* | | Dafny: fixed bug in reads checking of array-to-sequence conversions | Rustan Leino | 2011-11-08 |
* | | Dafny: Cleaned up proof of RevConcat in test case | Rustan Leino | 2011-11-08 |
| * | Merge | Unknown | 2011-11-08 |
| |\ |
|
| * | | Additions to GPU Verify for paper submission. | Unknown | 2011-11-08 |
| | * | some refactoring suggested by Michal | qadeer | 2011-11-07 |
| | * | Merge | qadeer | 2011-11-07 |
| | |\ |
|
| | * \ | Merge | qadeer | 2011-11-07 |
| | |\ \
| |_|/ /
|/| | | |
|
| | * | | change in model parsing with datatype values | qadeer | 2011-11-07 |
* | | | | Dafny: added a new /inductionHeuristic option | Rustan Leino | 2011-11-04 |
* | | | | Dafny: in test suite (Rippling.dfy), replaced an inline lemma with a call to ... | Rustan Leino | 2011-11-04 |
* | | | | Dafny: added options to make Induction Heuristic apply to array index express... | Rustan Leino | 2011-11-04 |
* | | | | Merge | Rustan Leino | 2011-11-03 |
|\ \ \ \ |
|
* | | | | | Added some Dafny and Boogie test cases, including Turing's factorial program,... | Rustan Leino | 2011-11-03 |
| | | * | | Merge | qadeer | 2011-11-01 |
| | | |\ \
| | |_|/ /
| |/| | | |
|