summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Changes needed to translate both contracts and method bodies. The Statement a...Gravatar mikebarnett2011-03-05
* Dafny: Added heuristic for when to turn on the induction tacticGravatar rustanleino2011-03-05
* changes for dealing with delegatesGravatar qadeer2011-03-05
* Dafny:Gravatar rustanleino2011-03-04
* Fix translation of "new" so that a procedure is generated (if needed) for the...Gravatar mikebarnett2011-03-03
* Made it unnecessary to set the types on the Boogie ASTs as we create them.Gravatar mikebarnett2011-03-03
* Create a static constructor only for types that don't already define one.Gravatar mikebarnett2011-03-02
* put the call to CreateStaticConstructor back inGravatar qadeer2011-03-02
* some fixesGravatar qadeer2011-03-02
* Fix null-equivalent initialization of fields so that instance fields are init...Gravatar mikebarnett2011-03-02
* fixes for splitFields optionGravatar qadeer2011-03-02
* Use the Sink's API for creating a procedure for the Invoke method of a delegate.Gravatar mikebarnett2011-03-01
* Fixed many bugs.Gravatar mikebarnett2011-03-01
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-03-01
* Dafny: support for nested match expressionsGravatar rustanleino2011-03-01
* Updates to Answer files from recent changesGravatar rustanleino2011-03-01
* Boogie build succeeded, 5 test(s) failedGravatar codeplexbot2011-02-27
* Dafny: Non-empty Visual-Studio error messages for related split-expr locations.Gravatar rustanleino2011-02-27
* Fixed dynamic dispatch so the most derived override is called for each subtype.Gravatar mikebarnett2011-02-25
* two bug fixesGravatar qadeer2011-02-25
* implemented delegates and eventsGravatar qadeer2011-02-25
* Added a new type, Type, that represents runtime types. The Heap interface now...Gravatar mikebarnett2011-02-24
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-02-24
* Changed calls to Debug.Assert to Contract.Assert.Gravatar mikebarnett2011-02-24
* Mimic Z3 logic for figuring out the blocking clause for the next counterexampleGravatar MichalMoskal2011-02-23
* Don't ever put a label under a quantifier.Gravatar MichalMoskal2011-02-23
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
* Add IEnumerable.Concat1 method.Gravatar MichalMoskal2011-02-23
* Add tests for -z3multipleErrors from Shuvendu.Gravatar MichalMoskal2011-02-23
* Fix build by adding missing project.Gravatar mikebarnett2011-02-23
* Boogie build succeeded, 4 test(s) failedGravatar codeplexbot2011-02-23
* Boogie build succeeded, 26 test(s) failedGravatar codeplexbot2011-02-23
* Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different...Gravatar MichalMoskal2011-02-23
* Check for timeout/memoryoutGravatar MichalMoskal2011-02-23
* Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing...Gravatar MichalMoskal2011-02-23
* Don't try to declare bv typesGravatar MichalMoskal2011-02-23
* Dispose of the prover when Close() is called.Gravatar MichalMoskal2011-02-23
* Add workaround for cmd raceGravatar MichalMoskal2011-02-23
* Set SOFT_TIMEOUT Z3 option if desired (SMT2 doesn't have :time-limit option!)Gravatar MichalMoskal2011-02-23
* Pass solverargumentsGravatar MichalMoskal2011-02-23
* Do typed->untyped translation for -mv variablesGravatar MichalMoskal2011-02-23
* Provide dummy implementation of FlushAxiomsToTheoremProver()Gravatar MichalMoskal2011-02-23
* Handle as-array[...] model elementsGravatar MichalMoskal2011-02-23
* Fixes in /useArrayTheory handlingGravatar MichalMoskal2011-02-23
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
* Throw exceptions when push/pop interface is used but not implementedGravatar MichalMoskal2011-02-23
* Pass :skolemid to SMTLib proverGravatar MichalMoskal2011-02-23
* Implement Push/Pop interface.Gravatar MichalMoskal2011-02-23
* Allow recent Z3 versions to be usedGravatar MichalMoskal2011-02-21
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21