summaryrefslogtreecommitdiff
path: root/Test/dafny4
Commit message (Expand)AuthorAge
* 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
* Support the transition from "modify Frame;" to "modify Frame { Body }" by ref...Gravatar Rustan Leino2014-04-04
* MergeGravatar Rustan Leino2014-03-17
|\
* | AST refactoring:Gravatar Rustan Leino2014-03-17
| * MergeGravatar Nada Amin2014-03-12
| |\ | |/ |/|
| * Improve computations, in particular compositionality. Isolated useless litera...Gravatar Nada Amin2014-03-12
* | Added a test case from the ACL2 bookGravatar Rustan Leino2014-03-10
|/
* Moved the (long running) CloudMake test files to their own directoryGravatar Rustan Leino2014-02-28
* Added CloudMake formalization and proofs to the test suiteGravatar Rustan Leino2014-02-26
* Added examples mentioned in a paper on circular coinduction.Gravatar Rustan Leino2014-02-25
* Added further assistance in coming up with decreases clauses in SCCs with co-...Gravatar Rustan Leino2014-02-24
* Minor clean-up in a couple of test files.Gravatar Rustan Leino2014-02-24
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 16:40:21 +0000