summaryrefslogtreecommitdiff
path: root/Source
Commit message (Collapse)AuthorAge
* Version 1.9.5.20511Gravatar leino2015-05-11
|
* Don't include arrow types among ordered types.Gravatar leino2015-05-11
| | | | | | Fix bug with not seeing imap's because of type synonyms. Don't show semi-colon after "decreases" in hover text. Minor cosmetic change in a test case.
* Added "inductive lemma" methodsGravatar leino2015-05-07
|
* Added inductive predicatesGravatar leino2015-05-06
|
* Improved generation of .reads axioms (correcting an incorrect answer and ↵Gravatar leino2015-05-01
| | | | corresponding incorrectly recorded desired answer)
* Improved encoding of a property of reads clauses to make things more easily ↵Gravatar leino2015-05-01
| | | | provable.
* Bumped version to 1.9.4.20428Gravatar leino2015-04-29
|
* MergeGravatar leino2015-04-28
|\
| * 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.
| * 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 #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.
* | 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
* 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.
* 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
| |
| * Remove unneeded reference from DafnyExtension.csproj (accidentally added by ↵Gravatar chrishaw2015-03-11
| | | | | | | | my previous checkin)
| * Add DafnyOptions.txt, and have the Dafny Visual Studio extension read ↵Gravatar chrishaw2015-03-11
| | | | | | | | command-line options from DafnyOptions.txt during initialization. DafnyOptions.txt gets built into the VSIX file and is installed as part of the Dafny Visual Studio extension.
| * MergeGravatar qunyanm2015-03-11
| |\ | |/ |/|
| * Fix issue #54 and #57. Resolve a formal's type before creating a substitute.Gravatar qunyanm2015-03-11
| |
* | Fixed bug in resolution of illegal programs.Gravatar leino2015-03-10
| | | | | | | | Fixed comments in some test cases.
* | Removed some old and unused functionsGravatar leino2015-03-09
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 15:20:54 +0000