summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
...
| * 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
|/
* MergeGravatar leino2014-11-19
|\
* | Fixed bug where resolution was overly restrictive with ghost variables ↵Gravatar leino2014-11-19
| | | | | | | | | | | | appearing in reads clauses. Fixed bug in the checking of reads subset for field frame targets ("back ticks")
| * Updated test output after change in Boogie.Gravatar wuestholz2014-11-16
|/
* Bug fixes in the compilation of forall statements.Gravatar leino2014-11-13
|
* MergeGravatar leino2014-11-13
|\
* | Use arbitrary lookahead to determine if the next expression is a lambda ↵Gravatar leino2014-11-13
| | | | | | | | expression.
* | Took a pass through the whole grammar to clean up allowSemi/allowLambda ↵Gravatar leino2014-11-11
| | | | | | | | parameters
* | Cleaned up a number of LL(1) conflicts in the grammar (I wish Coco/R ↵Gravatar leino2014-11-10
| | | | | | | | | | | | supported a GREEDY annotation) Don't allow colons with no intervening expressions in sequence-slicing expression
| * Updated version to 1.9.2.11107 (which is going out on rise4fun)Gravatar Rustan Leino2014-11-07
|/
* Resolved several more LL(1) warnings in the grammarGravatar Rustan Leino2014-11-06
|
* MergeGravatar leino2014-11-06
|\
* | Started fixing a number of LL(1) warningsGravatar leino2014-11-06
| | | | | | | | | | Disallow empty modifies/reads clauses (this eliminates some LL(1) warnings) Require modify statement to take a nonempty list of frame expressions
| * Now the parser parses "Type" rather than "IToken" for a traitGravatar Reza Ahmadi2014-11-05
| |
| * Extracted a separate class to generate fresh variable names.Gravatar wuestholz2014-11-06
| |
| * Updated test.Gravatar chmaria2014-11-06
| |
| * Added computation of free variables in dirty while statements.Gravatar chmaria2014-11-06
|/
* MergeGravatar Rustan Leino2014-11-05
|\
* | Temporarily disabled one of the methods in NumberRepresentations.dfy -- this ↵Gravatar leino2014-11-05
| | | | | | | | needs to be addressed in some way that will produce stable verification results
* | MergeGravatar leino2014-11-05
|\ \
| * | Refactored the generation of unique IDs for temporary variable names.Gravatar wuestholz2014-11-05
| | |
| * | Did some refactoring.Gravatar wuestholz2014-11-05
| | |
* | | MergeGravatar leino2014-11-04
|\| |
* | | MergeGravatar leino2014-11-04
|\ \ \
* | | | Refactored SnapshotableTrees a bit and made it verify in a reasonable amount ↵Gravatar leino2014-11-04
| | | | | | | | | | | | | | | | of time :)
| | * | Made dirty statements ghost.Gravatar chmaria2014-11-04
| | | |
| | | * MergeGravatar Rustan Leino2014-11-03
| | | |\ | | | |/ | | |/|
| | | * Updated a test case for new syntax and convensionsGravatar Rustan Leino2014-11-03
| | | |
| | * | Fixed test output after refactoring in Boogie.Gravatar wuestholz2014-11-03
| | | |
| | * | Fixed test output after refactoring in Boogie.Gravatar wuestholz2014-11-02
| | | |
| * | | MergeGravatar leino2014-11-01
| |\| |
| * | | Various DafnyPrelude.bpl cleanup.Gravatar leino2014-11-01
| | | | | | | | | | | | | | | | Removed unused cases from axioms where Seq#Take and Seq#Drop take out-of-range arguments
| | * | Minor fix in test dafny2/SnapshotableTrees.dfy.Gravatar chmaria2014-11-01
| | | |
| | * | Added initial support for dirty while statements.Gravatar chmaria2014-11-01
| | | |
| * | | Improved power of axioms Seq#FromArrayGravatar leino2014-10-31
| |/ /
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 08:34:29 +0000