| Commit message (Collapse) | Author | Age |
|---|
| | |
|
| |
|
|
| |
elements.
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
| |/
|
|
|
|
|
| |
with type parameters).
Resolve ClassDecl.TraitsTyp as types.
Moved declaration of TraitParent and NoTraitAtAll to prelude.
|
| | |
|
| |
|
|
| |
of proving the existence check of let-such-that and assign-such-that
|
| | |
|
| | |
|
| | |
|
| | |
|
| |
|
|
| |
EuclideanModulus_short call EuclideanModulus_int, not the BigInteger EuclideanModulus. (Same for EuclideanDivision.)
|
| |
|
|
| |
EuclideanDivision_short call EuclideanDivision_int, not the BigInteger EuclideanDivision. (Same for EuclideanModulus.)
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
|
| |
|
|
| |
Removed unused cases from axioms where Seq#Take and Seq#Drop take out-of-range arguments
|
| | |
|
| |
|
|
| |
Results in more manual work, but it also produces more predictable behavior.
|
| |
|
|
| |
Also include ModelViewer.dll in binary distribution
|
| | |
|
| |
|
|
|
|
| |
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.
|
| |
|
|
| |
Made up for inadequacy in reasoning machinery (supplying Int(Real(i)) == i axiom)
|
| |
|
|
| |
Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
* 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
|
| |/ |
|
| |\ |
|
| | | |
|
| | | |
|
| | |
| |
| |
| |
| |
| | |
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.)
|
| |/
|
|
| |
those heap location that hold the array elements
|
| | |
|
| |
|
|
| |
Minor changes in a test file.
|
| |
|
|
|
|
| |
themselves.
Other serendipitous axiom improvements.
|
| |
|
|
| |
Improved situation with (reducing bogosity of) type checking of "object".
|
| | |
|
| |
|
|
|
|
| |
literals.
Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations).
|
| | |
|
| |\ |
|
| | |
| |
| |
| |
| |
| |
| | |
of a match expression).
Moved the implementation of CondApplyBox, BoxIfNecessary, CondApplyUnbox, and ModeledAsBoxType from class ExpressionTranslator to class Translator.
Fixed compilation of match expressions, to allow them anywhere.
|
| |/ |
|
| |
|
|
| |
the top-level of function bodies. (Note, resolver also needs to allow this before the user can take advantage of this.)
|
| | |
|
| |
|
|
| |
'UnivBackPred2.smt2' no longer needed).
|
| | |
|
| | |
|
| |\ |
|
| | | |
|
leino
Bryan Parno
Dan Rosén