summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Collapse)AuthorAge
* Fix issue 148. The results for sign comparison for BigRational.CompareTo wasGravatar qunyanm2016-04-01
| | | | wrong.
* Add a wrapper for DafnyServer.exeGravatar Clément Pit--Claudel2016-03-30
|
* Changed checked-in version of Z3 to 4.4.1 (from 4.4.0)Gravatar leino2015-11-17
|
* MergeGravatar leino2015-09-28
|\
* | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| | | | | | | | | | | | | | Other clean-up in resolution passes, like: Include everything of type "char" into bounds that are discovered, and likewise for reference types. Allow more set comprehensions, determining if they are finite based on their argument type. Changed CalcExpr.SubExpressions to not include computed expressions.
| * Revert part of 1899 (47fd7d09d605, "Fix a check that occasionally led to ...")Gravatar Clément Pit--Claudel2015-09-23
| | | | | | | | That commit accidentally overwrote the dafny shell script for Linux and MacOS.
| * Auto-merged heads.Gravatar Michael Lowell Roberts2015-09-21
| |\
| | * Fix a check that occasionally led to an out of bounds exception in the extensionGravatar Bryan Parno2015-09-17
| |/ |/|
| * Fix for soundness bug discovered in SeqFromArray.Gravatar Michael Lowell Roberts2015-09-17
|/
* Fix #90Gravatar Clément Pit--Claudel2015-09-09
| | | | The mono wrapper for Dafny didn't forward command line arguments.
* fix for comparison error in prelude when using /optimize.Gravatar Michael Lowell Roberts2015-08-31
|
* Look for z3 in Binaries/z3/bin (but keep the vendored version for convenience)Gravatar Clément Pit--Claudel2015-08-27
| | | | | | Dafny now first looks for a z3 binary in z3/bin, and if it can't find one it looks for one in Binaries/z3.exe (mostly for backwards-compatibility with already set-up source installations).
* Set exec flag on Binaries/z3Gravatar Clément Pit--Claudel2015-08-22
|
* Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
|
* Add a wrapper script around the Dafny binary (for mono).Gravatar Clément Pit--Claudel2015-08-13
|
* Add a Linux z3 binary to the repo, and use that or z3.exe based on the OSGravatar Clément Pit--Claudel2015-07-31
|
* Update z3 to 4.4. One test had to be edited.Gravatar Clément Pit--Claudel2015-07-21
|
* Fixed bug in BplImp!Gravatar leino2015-07-01
| | | | Improvements in encoding of reads of function values.
* Tried to reduce frame-axiom instantiations by saying the earlier heap must ↵Gravatar leino2015-06-25
| | | | | | be a "heap anchor". Currently, a heap is an anchor if it produced by a havoc (but not a direct update).
* System.Collections.Immutable.dll is now stored in the Binaries directory and ↵Gravatar Michael Lowell Roberts2015-06-16
| | | | copied to the output directory when the /optimize flag is used.
* added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
|
* Fix the Seq#Contain axiom; it should talk about T, not ref.Gravatar Clément Pit--Claudel2015-06-07
|
* Add an infinite set collection type.Gravatar qunyanm2015-05-29
|
* Bumped version to 1.9.4.20428Gravatar leino2015-04-29
|
* 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 #68. Change GetHashCode implementation for Sequence.Gravatar qunyanm2015-04-14
|
* MergeGravatar qunyanm2015-04-06
|\
* | Add z3.exe and z3-license.txt to dafny binary and extension distribution.Gravatar qunyanm2015-04-06
| |
| * 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.
* Add LongLength methods to Set/Map in DafnyRuntime.csGravatar chrishaw2015-03-17
|
* Beefed up collection axioms (in particular, for maps) to improve the chance ↵Gravatar Rustan Leino2015-03-10
| | | | of proving the existence check of let-such-that and assign-such-that
* Removed some old and unused functionsGravatar leino2015-03-09
|
* Fix issue #60Gravatar qunyanm2015-03-06
|
* Add imap display/update expressionsGravatar chrishaw2015-02-27
|
* Add imap type, which is like map but may have have infinite sizeGravatar chrishaw2015-02-26
|
* Optimization to nativeType: have EuclideanModulus_sbyte and ↵Gravatar chrishaw2014-12-11
| | | | EuclideanModulus_short call EuclideanModulus_int, not the BigInteger EuclideanModulus. (Same for EuclideanDivision.)
* Optimization to nativeType: have EuclideanDivision_sbyte and ↵Gravatar chrishaw2014-12-09
| | | | EuclideanDivision_short call EuclideanDivision_int, not the BigInteger EuclideanDivision. (Same for EuclideanModulus.)
* Add nativeType attribute for newtype declarations. Change Compiler.cs to ↵Gravatar chrishaw2014-12-09
| | | | | | | | | | | | | | | | | | | | | | | | use native C# representation of small integer newtypes. Examples: newtype{:nativeType "byte"} byte = i:int | 0 <= i < 0x100 newtype{:nativeType "sbyte"} sbyte = i:int | -0x80 <= i < 0x80 newtype{:nativeType "ushort"} uint16 = i:int | 0 <= i < 0x10000 newtype{:nativeType "short"} int16 = i:int | -0x8000 <= i < 0x8000 newtype{:nativeType "uint"} uint32 = i:int | 0 <= i < 0x100000000 newtype{:nativeType "int"} int32 = i:int | -0x80000000 <= i < 0x80000000 newtype{:nativeType "ulong"} uint64 = i:int | 0 <= i < 0x10000000000000000 newtype{:nativeType "long"} int64 = i:int | -0x8000000000000000 <= i < 0x8000000000000000 newtype month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise BigInteger newtype{:nativeType} month = i:int | 0 <= i < 12 // same as {:nativeType true} newtype{:nativeType true} month = i:int | 0 <= i < 12 // use smallest compatible C# type if possible (byte in this case), otherwise error newtype{:nativeType false} month = i:int | 0 <= i < 12 // use BigInteger newtype{:nativeType "uint"} month = i:int | 0 <= i < 12 // use C# uint type if possible, otherwise error newtype{:nativeType} even20 = i:int | 0 <= i < 20 && (i % 2 == 0) // nativeTypes need not be contiguous newtype{:nativeType} even10 = i:even20 | i < 10 // nativeTypes can inherit constraints from other nativeTypes
* Various DafnyPrelude.bpl cleanup.Gravatar leino2014-11-01
| | | | Removed unused cases from axioms where Seq#Take and Seq#Drop take out-of-range arguments
* Improved power of axioms Seq#FromArrayGravatar leino2014-10-31
|
* Add an option to use reduce Z3's knowledge of non-linear arithmetic.Gravatar Bryan Parno2014-10-24
| | | | Results in more manual work, but it also produces more predictable behavior.
* Changed version to 1.9.1.11021Gravatar leino2014-10-21
| | | | Also include ModelViewer.dll in binary distribution
* Comparisons and well-founded order of charGravatar leino2014-10-21
|
* Added types "char" and "string" (the latter being a synonym for "seq<char>").Gravatar leino2014-10-20
| | | | | | Added string literals with various escapes--a subset of those supported in C# and similar languages, including the C# verbatim strings. Previously, the "print" statement and custom attributes could support expression-or-string arguments; there is no longer a need to special-case these, so these arguments are now just expressions. Fixed lack of operator resolution in custom attributes.
* Fixed bugs in previous check-inGravatar leino2014-08-25
| | | | Made up for inadequacy in reasoning machinery (supplying Int(Real(i)) == i axiom)
* Added .Trunc field to real-based typesGravatar leino2014-08-21
| | | | Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer
* Compile lambda functions and apply expressions, and change let expr compilationGravatar Dan Rosén2014-08-12
|
* MergeGravatar Dan Rosén2014-08-11
|\
* | Add higher-order-functions and some other goodiesGravatar Dan Rosén2014-08-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | * The reads clause now needs to be self framing. * The requires clause now needs to be framed by the reads clause. * There are one-shot lambdas, with a single arrow, but they will probably be removed. * There is a {:heapQuantifier} attribute to quantifiers, but they will probably be removed. * Add smart handling of type variables * Add < and > for datatype & type parameter
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 16:53:11 +0000