summaryrefslogtreecommitdiff
path: root/Test/dafny4
Commit message (Expand)AuthorAge
* Added another lemma to a test fileGravatar Rustan Leino2015-07-02
* MergeGravatar leino2015-07-01
|\
* | Fixed bug in BplImp!Gravatar leino2015-07-01
| * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
|/
* MergeGravatar leino2015-06-12
|\
* | Added /vcs... cop-out to test case to make it go throughGravatar leino2015-06-12
| * Fix a bug spotted by Chris in my BigInteger patch; thanks!Gravatar Clément Pit--Claudel2015-06-12
|/
* Generate #requires function for OpaqueFunction.Gravatar qunyanm2015-06-04
* Improvements to Nipkow and Klein test cases: Changed imap to map, removed ne...Gravatar leino2015-05-29
* Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.Gravatar qunyanm2015-05-18
* Fix issue #79. Allow tuple pattern matching with parenthesis only.Gravatar qunyanm2015-05-15
* Don't include arrow types among ordered types.Gravatar leino2015-05-11
* Added to the test suite a Dafny encoding of Chapter 7 from the Nipkow and Kle...Gravatar leino2015-05-10
* Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and Kle...Gravatar leino2015-04-29
* Added a test where Dafny verifies something that the Juggernaut tool can inferGravatar leino2015-04-28
* Fix issue #72. Add the constructor questionmark to a function's axiom if theGravatar qunyanm2015-04-24
* Fix issue #70. Check the ctors for equality before marking them as duplicates.Gravatar qunyanm2015-04-21
* Fix issue #73. Pass in expr.tok when creating Bpl.Expr for InMap and NotInMap.Gravatar qunyanm2015-04-20
* Fix issue #69. If we can't find a member in classMembers, search the staticGravatar qunyanm2015-04-17
* HashCode for Set/MultiSet/Map should be independent of the order of theGravatar qunyanm2015-04-17
* Change GetHashCode for Set, MultiSet and MapGravatar qunyanm2015-04-16
* Fix issue #71. When substitute the forall's variables for those of theGravatar qunyanm2015-04-16
* Fix issue #68. Change GetHashCode implementation for Sequence.Gravatar qunyanm2015-04-14
* Fix issue #67. Check SupportsEquality before determining whether to emit EqualsGravatar qunyanm2015-04-13
* Fix issue #62. Check for modifies clause and constructors in the enclosingGravatar qunyanm2015-03-31
* Fix issue 61. Decreases are by default in ghost context. Therefore,Gravatar qunyanm2015-03-31
* Fix issue #56. Convert parametered opaque type parameters into an IdentifierExprGravatar qunyanm2015-03-27
* Fix issue #58. In TrSplitExpr(), add allocatedness for arguments to the inlinedGravatar qunyanm2015-03-26
* Fix issue #63. ForceSubstitutionOfQuantifiedVars for SetComprehesion.Gravatar qunyanm2015-03-17
* Fix issue #55 and #64. When performing type argument substitution for functionGravatar qunyanm2015-03-16
* MergeGravatar qunyanm2015-03-11
|\
* | Fix issue #54 and #57. Resolve a formal's type before creating a substitute.Gravatar qunyanm2015-03-11
| * This changeset changes the default visibility of a function/predicate body ou...Gravatar leino2015-03-09
|/
* Fix issue #60Gravatar qunyanm2015-03-06
* Temporarily disabled one of the methods in NumberRepresentations.dfy -- this ...Gravatar leino2014-11-05
* Made semi-colons are specification clauses optional. In a future version, th...Gravatar leino2014-10-25
* Allow underscores in numeric literals (and in field/destructor names that are...Gravatar leino2014-10-23
* Fixed crash in inferred descreases clauses involving newtypes.Gravatar leino2014-10-21
* Changed test case to not use '/doNotUseParallelism' anymore.Gravatar wuestholz2014-07-31
* An attempt at making dafny4/NumberRepresentations.dfy run faster and more pre...Gravatar Rustan Leino2014-07-15
* Include an explicit trigger to make NumberRepresentations.dfy behave more con...Gravatar Rustan Leino2014-07-09
* Tidy up two files in test suiteGravatar Dan Rosen2014-07-07
* MergeGravatar Dan Rosén2014-07-07
|\
* | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| * MergeGravatar leino2014-07-01
| |\
| | * Removed the old test infrastructure.Gravatar wuestholz2014-07-01
| |/ |/|
| * Add support doing computations over sequencesGravatar leino2014-06-16
|/
* Set up the same test infrastructure as in Boogie.Gravatar wuestholz2014-05-29
* Fixed refinement of modify statementsGravatar Rustan Leino2014-04-04
* Also include lower set bounds (bounding a set from below) in witness guesses ...Gravatar Rustan Leino2014-04-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 15:08:57 +0000