| Commit message (Expand) | Author | Age |
* | Boogie build succeeded, 4 test(s) failed | codeplexbot | 2011-03-07 |
* | Fix some more contracts. | mikebarnett | 2011-03-07 |
* | Fix contracts so runtime checking can be turned on. | mikebarnett | 2011-03-07 |
* | Fix Sink.FindOrCreateProcedure so that it takes an IMethodDefinition instead ... | mikebarnett | 2011-03-06 |
* | Added support for stub methods. If a method definition is marked with a custo... | mikebarnett | 2011-03-06 |
* | Dafny: | rustanleino | 2011-03-06 |
* | In the Sink, keep track of any procedures defined in the initial program (whi... | mikebarnett | 2011-03-06 |
* | Changes needed to translate both contracts and method bodies. The Statement a... | mikebarnett | 2011-03-05 |
* | Dafny: Added heuristic for when to turn on the induction tactic | rustanleino | 2011-03-05 |
* | changes for dealing with delegates | qadeer | 2011-03-05 |
* | Dafny: | rustanleino | 2011-03-04 |
* | Fix translation of "new" so that a procedure is generated (if needed) for the... | mikebarnett | 2011-03-03 |
* | Made it unnecessary to set the types on the Boogie ASTs as we create them. | mikebarnett | 2011-03-03 |
* | Create a static constructor only for types that don't already define one. | mikebarnett | 2011-03-02 |
* | put the call to CreateStaticConstructor back in | qadeer | 2011-03-02 |
* | some fixes | qadeer | 2011-03-02 |
* | Fix null-equivalent initialization of fields so that instance fields are init... | mikebarnett | 2011-03-02 |
* | fixes for splitFields option | qadeer | 2011-03-02 |
* | Use the Sink's API for creating a procedure for the Invoke method of a delegate. | mikebarnett | 2011-03-01 |
* | Fixed many bugs. | mikebarnett | 2011-03-01 |
* | Boogie build succeeded, 4 test(s) failed | codeplexbot | 2011-03-01 |
* | Dafny: support for nested match expressions | rustanleino | 2011-03-01 |
* | Updates to Answer files from recent changes | rustanleino | 2011-03-01 |
* | Boogie build succeeded, 5 test(s) failed | codeplexbot | 2011-02-27 |
* | Dafny: Non-empty Visual-Studio error messages for related split-expr locations. | rustanleino | 2011-02-27 |
* | Fixed dynamic dispatch so the most derived override is called for each subtype. | mikebarnett | 2011-02-25 |
* | two bug fixes | qadeer | 2011-02-25 |
* | implemented delegates and events | qadeer | 2011-02-25 |
* | Added a new type, Type, that represents runtime types. The Heap interface now... | mikebarnett | 2011-02-24 |
* | Boogie build succeeded, 4 test(s) failed | codeplexbot | 2011-02-24 |
* | Changed calls to Debug.Assert to Contract.Assert. | mikebarnett | 2011-02-24 |
* | Mimic Z3 logic for figuring out the blocking clause for the next counterexample | MichalMoskal | 2011-02-23 |
* | Don't ever put a label under a quantifier. | MichalMoskal | 2011-02-23 |
* | Add MULTI_TRACES prover option (equivalent of /z3multipleErrors) | MichalMoskal | 2011-02-23 |
* | Add IEnumerable.Concat1 method. | MichalMoskal | 2011-02-23 |
* | Add tests for -z3multipleErrors from Shuvendu. | MichalMoskal | 2011-02-23 |
* | Fix build by adding missing project. | mikebarnett | 2011-02-23 |
* | Boogie build succeeded, 4 test(s) failed | codeplexbot | 2011-02-23 |
* | Boogie build succeeded, 26 test(s) failed | codeplexbot | 2011-02-23 |
* | Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different... | MichalMoskal | 2011-02-23 |
* | Check for timeout/memoryout | MichalMoskal | 2011-02-23 |
* | Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing... | MichalMoskal | 2011-02-23 |
* | Don't try to declare bv types | MichalMoskal | 2011-02-23 |
* | Dispose of the prover when Close() is called. | MichalMoskal | 2011-02-23 |
* | Add workaround for cmd race | MichalMoskal | 2011-02-23 |
* | Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!) | MichalMoskal | 2011-02-23 |
* | Pass solverarguments | MichalMoskal | 2011-02-23 |
* | Do typed->untyped translation for -mv variables | MichalMoskal | 2011-02-23 |
* | Provide dummy implementation of FlushAxiomsToTheoremProver() | MichalMoskal | 2011-02-23 |
* | Handle as-array[...] model elements | MichalMoskal | 2011-02-23 |