summaryrefslogtreecommitdiff
path: root/Binaries
Commit message (Collapse)AuthorAge
* 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
| * Implemented missing routine in runtime system (real-to-int conversion)Gravatar leino2014-07-21
|/
* MergeGravatar Dan Rosén2014-07-07
|\
* | New logical encoding of types with Is and IsAllocGravatar Dan Rosén2014-07-07
| |
| * Added some axioms about seq-to-multiset conversionsGravatar Rustan Leino2014-06-24
| |
| * Specialized Lit function for int and real (leaving all other cases ↵Gravatar Rustan Leino2014-06-10
| | | | | | | | | | | | polymorphic). This reduces the number of int<->U conversions that Boogie adds, which avoids a looping problem in Z3. (Regrettably, the test suite seems to have become rather unstable. Sometimes everything verifies and sometimes there is some looping forever.)
| * Improved axiom that knows that array-to-sequence converstion depends only on ↵Gravatar Rustan Leino2014-06-04
|/ | | | those heap location that hold the array elements
* Compile realsGravatar Rustan Leino2014-04-13
|
* Improvements in sequence axioms to make checking more automatic.Gravatar Rustan Leino2014-04-02
| | | | Minor changes in a test file.
* Added axiom to transfer array element-type information onto the elements ↵Gravatar Rustan Leino2014-03-20
| | | | | | themselves. Other serendipitous axiom improvements.
* Fixed problem with propagating allocation information about array elements.Gravatar Rustan Leino2014-03-20
| | | | Improved situation with (reducing bogosity of) type checking of "object".
* Removed an apparently unneeded trigger.Gravatar Rustan Leino2014-03-06
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 02:48:41 +0000