summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Add imap keyword to VS/emacs/vim/latex filesGravatar chrishaw2015-02-26
|
* Add imap type, which is like map but may have have infinite sizeGravatar chrishaw2015-02-26
|
* Add an explicit trigger so that Z3 doesn't choose an overly generous trigger ↵Gravatar Bryan Parno2015-02-09
| | | | on SeqIndex
* Make allowGlobals a bit more generousGravatar Bryan Parno2015-02-09
|
* Generate unique IDs hierarchically, to reduce changes to IDs when the ↵Gravatar leino2015-01-28
| | | | program is modified (to help with fine-grained caching)
* Did some refactoring to improve the name generation.Gravatar wuestholz2015-01-28
|
* Did some refactoring to improve the name generation.Gravatar wuestholz2015-01-28
|
* Did some refactoring to improve the name generation.Gravatar wuestholz2015-01-27
|
* Did some refactoring to improve the name generation.Gravatar wuestholz2015-01-27
|
* Did some refactoring to improve the name generation.Gravatar wuestholz2015-01-27
|
* Assume type properties of values that are created by a havoc assignment. ↵Gravatar Rustan Leino2015-01-27
| | | | | | Such assignments are part of assign-such-that statements, and thus this also fixes Issue 52.
* Fixed an encoding bug for newtypes (this fixes Issue #50)Gravatar Rustan Leino2015-01-27
|
* Minor change to a test caseGravatar wuestholz2015-01-27
|
* DafnyExtension: Made it use the more advanced on-demand re-verification by ↵Gravatar wuestholz2015-01-26
| | | | default.
* Updated test output after change in Boogie.Gravatar wuestholz2015-01-24
|
* Minor change to grammar to avoid missing tokenGravatar wuestholz2015-01-24
|
* Make sure to check that subrange types are not used as type parametersGravatar leino2015-01-23
|
* MergeGravatar leino2015-01-23
|\
* | Switched use of List(IToken) in UserDefinedType to NameSegment/ExprDotName, ↵Gravatar leino2015-01-23
| | | | | | | | | | | | | | so use the new name resolution machinery that handles modules and type parameters Included some inadvertently left-out test cases in dafny0/Modules0.dfy Fixed comparable-types tests
| * MergeGravatar Bryan Parno2015-01-13
| |\
| | * Minor change due to a change in BoogieGravatar wuestholz2015-01-13
| |/ |/|
* | When ambiguous references all resolve to the same declaration, don't complainGravatar leino2015-01-09
| |
| * Check the AllowGlobals flag in one additional location to avoid a contract ↵Gravatar Bryan Parno2015-01-08
|/ | | | failure
* Added command-line switch /allowGlobals to simplify transition from language ↵Gravatar leino2015-01-07
| | | | changes introduced in changeset c56031307ac1
* Bumped the version number to 1.9.3.20107Gravatar leino2015-01-07
|
* Fixed bug in opaque functions with type parametersGravatar leino2015-01-07
|
* Added lemmas that make verification go through faster and more reliablyGravatar leino2015-01-05
|
* MergeGravatar leino2015-01-03
|\
* | Fixed resolution of method calls with explicit type parameters.Gravatar leino2015-01-02
| | | | | | | | Finished refactoring of the recent name segments changes.
| * Updated test output after change in Boogie.Gravatar wuestholz2014-12-28
| |
| * Minor changeGravatar wuestholz2014-12-26
| |
| * When in DafnyCC mode, ignore termination checkingGravatar Bryan Parno2014-12-16
| |
* | Fixed bug in /compile:3, when Main is explicitly given as a static methodGravatar leino2014-12-12
| |
* | Language change: All functions and methods declared lexically outside any ↵Gravatar leino2014-12-12
| | | | | | | | | | | | | | | | | | | | class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods.
| * Optimization to nativeType: have EuclideanModulus_sbyte and ↵Gravatar chrishaw2014-12-11
|/ | | | EuclideanModulus_short call EuclideanModulus_int, not the BigInteger EuclideanModulus. (Same for EuclideanDivision.)
* Fixed two crashes in resolverGravatar leino2014-12-10
| | | | Corrected merge
* MergeGravatar leino2014-12-09
|\
| * 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
* | Allow user-specified type parametersGravatar leino2014-12-09
| |
* | Finished up refactoring of the new name segment parsing, AST, and resolution.Gravatar leino2014-12-07
| | | | | | | | Removed now defunct IdentifierSequence from the AST.
| * minor change on a test.Gravatar Reza Ahmadi2014-12-03
| |
| * fixed a minor bug: null checking.Gravatar Reza Ahmadi2014-12-03
| |
| * added multiple trait inheritance.Gravatar Reza Ahmadi2014-12-03
| | | | | | | | - a class can now extend more than one traits
* | Fixed some issues with assignments in refinements, both soundness bugs in ↵Gravatar leino2014-12-02
| | | | | | | | previous version and changes necessitated by recent parsing refactoring
* | Fixed parser lookahead bug that had caused an infinite loop.Gravatar leino2014-12-02
| |
* | Snapshot, to be continuedGravatar leino2014-12-02
| |
| * removing one unnessessary check in the clonerGravatar Reza Ahmadi2014-12-02
| |
| * - fixed a bug in merging fields that come from a parent traitGravatar Reza Ahmadi2014-12-02
| | | | | | | | - added one more test
| * Updated test output after change in Boogie.Gravatar wuestholz2014-11-25
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 10:31:39 +0000