summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Improved encoding of a property of reads clauses to make things more easily ↵Gravatar leino2015-05-01
| | | | provable.
* Added to the test suite a Dafny encoding of Chapter 3 from the Nipkow and ↵Gravatar leino2015-04-29
| | | | Klein book on semantics
* Bumped version to 1.9.4.20428Gravatar leino2015-04-29
|
* Added a test where Dafny verifies something that the Juggernaut tool can inferGravatar leino2015-04-28
|
* MergeGravatar leino2015-04-28
|\
* | Changes to the VerifyThis2015 test programsGravatar leino2015-04-28
| |
| * added notice about vim-loves-dafny.Gravatar Michael Lowell Roberts2015-04-27
| |
| * Fix issue #72. Add the constructor questionmark to a function's axiom if theGravatar qunyanm2015-04-24
| | | | | | | | function has a MemberSelectExpr that accesses a type with only one constructor.
* | Fixed bug in tuplesGravatar leino2015-04-24
| |
| * Rearranged handling ambiguously named declarations, so that the multitudes ↵Gravatar Rustan Leino2015-04-22
| | | | | | | | | | | | | | | | of ambiguous names that arise when layers of modules are opened-imported don't cause gross memory waste. In particular, previously, the names of many such ambiguous declarations were shown to exceed 1 million characters, the way they had been constructed. Now, multiple imports of the same declaration are immediatley resolved as not being ambiguous.
| * 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
| | | | | | | | members of the enclosing module or its imports.
| * HashCode for Set/MultiSet/Map should be independent of the order of theGravatar qunyanm2015-04-17
| | | | | | | | elements.
| * 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
| | | | | | | | fn in fixupRevealLemma substitute the types as well.
| * Fix issue #68. Change GetHashCode implementation for Sequence.Gravatar qunyanm2015-04-14
|/
* Completed problems from the VerifyThis 2015 program verification competitionGravatar leino2015-04-14
|
* Fix issue #67. Check SupportsEquality before determining whether to emit EqualsGravatar qunyanm2015-04-13
| | | | or == for equality testing.
* Include axioms about $Is and $IsAlloc for traitsGravatar leino2015-04-07
|
* Support calls to static trait methods/functions via the classGravatar leino2015-04-07
|
* MergeGravatar leino2015-04-07
|\
* | Revised look-up and compilation of inherited trait members (static ↵Gravatar leino2015-04-07
| | | | | | | | functions/methods don't work yet)
| * Make sure that PrintTopLevelDecls receives program FullName, not just Name, ↵Gravatar chrishaw2015-04-07
|/ | | | so that printMode NoIncludes/NoGhost works
* Changed version to 1.9.3.20406 and updated copyright year to include 2015.Gravatar leino2015-04-06
|
* Copy z3.exe and Z3-LICENSE.txt (from Binaries directory to ↵Gravatar leino2015-04-06
| | | | Source/DafnyExtension directory) as pre-build events
* MergeGravatar leino2015-04-06
|\
| * MergeGravatar qunyanm2015-04-06
| |\
| * | Add z3.exe and z3-license.txt to dafny binary and extension distribution.Gravatar qunyanm2015-04-06
| | |
* | | Fixed missing case in previous check-inGravatar leino2015-04-05
| |/ |/|
* | Fixed compilation of static members in traitsGravatar leino2015-04-05
| |
* | Fixed some bugs in override axioms (but still missing support for classes ↵Gravatar leino2015-04-05
| | | | | | | | | | | | | | with type parameters). Resolve ClassDecl.TraitsTyp as types. Moved declaration of TraitParent and NoTraitAtAll to prelude.
* | Whitespace deltas in test files (in particular, removing tabs and adjusting ↵Gravatar leino2015-04-03
| | | | | | | | some indentation)
* | MergeGravatar leino2015-04-03
|\|
* | Added test cases and fixes for overrides termination checksGravatar leino2015-04-03
| | | | | | | | Removed syntactic presence checks for specifications--these will be checked semantically by the verifier
| * Eliminate redundant checks of newtype and opaque function well-formedness ↵Gravatar chrishaw2015-04-02
|/ | | | from included files
* Reflect cleaner syntax in some test programsGravatar leino2015-03-31
|
* Fix issue #62. Check for modifies clause and constructors in the enclosingGravatar qunyanm2015-03-31
| | | | class when determining whether a method named Main() is the program entry.
* Fix issue 61. Decreases are by default in ghost context. Therefore,Gravatar qunyanm2015-03-31
| | | | dontCareAboutCompilation flag should be set to false in the ResolveOpts.
* Fix issue #56. Convert parametered opaque type parameters into an IdentifierExprGravatar qunyanm2015-03-27
| | | | instead of FunctionCall.
* Fix issue #58. In TrSplitExpr(), add allocatedness for arguments to the inlinedGravatar qunyanm2015-03-26
| | | | call.
* Add LongLength methods to Set/Map in DafnyRuntime.csGravatar chrishaw2015-03-17
|
* MergeGravatar chrishaw2015-03-17
|\
* | Optimize datatype/tuple update expression to coalesce adjacent updates into ↵Gravatar chrishaw2015-03-17
| | | | | | | | a single update. Specifically, e[x1:=e1]...[xn:=en] is treated like a single update e[x1,...,xn := e1,...,en].
| * 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
| | | | | | F's corresponding F_FULL, make sure the function is indeed the FullVesion before the substitution. Also keep the TypeArgsSubst for the enclosingClass in the typeMap.
* Fixed merge issuesGravatar leino2015-03-13
|
* MergeGravatar leino2015-03-13
|\
* | Allow let-such-that expression to be compiled, provided that they provably ↵Gravatar leino2015-03-13
| | | | | | | | have a unique value
| * Allow trigger annotations in more statements and expressionsGravatar chrishaw2015-03-11
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-28 18:22:52 +0000