Commit message (Collapse) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Finished up refactoring of the new name segment parsing, AST, and resolution. | leino | 2014-12-07 | |
| | | | | | | | | Removed now defunct IdentifierSequence from the AST. | |||
| * | minor change on a test. | Reza Ahmadi | 2014-12-03 | |
| | | ||||
| * | fixed a minor bug: null checking. | Reza Ahmadi | 2014-12-03 | |
| | | ||||
| * | added multiple trait inheritance. | Reza Ahmadi | 2014-12-03 | |
| | | | | | | | | - a class can now extend more than one traits | |||
* | | Fixed some issues with assignments in refinements, both soundness bugs in ↵ | leino | 2014-12-02 | |
| | | | | | | | | previous version and changes necessitated by recent parsing refactoring | |||
* | | Fixed parser lookahead bug that had caused an infinite loop. | leino | 2014-12-02 | |
| | | ||||
* | | Snapshot, to be continued | leino | 2014-12-02 | |
| | | ||||
| * | removing one unnessessary check in the cloner | Reza Ahmadi | 2014-12-02 | |
| | | ||||
| * | - fixed a bug in merging fields that come from a parent trait | Reza Ahmadi | 2014-12-02 | |
| | | | | | | | | - added one more test | |||
| * | Updated test output after change in Boogie. | wuestholz | 2014-11-25 | |
|/ | ||||
* | Merge | leino | 2014-11-19 | |
|\ | ||||
* | | Fixed bug where resolution was overly restrictive with ghost variables ↵ | leino | 2014-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. | wuestholz | 2014-11-16 | |
|/ | ||||
* | Bug fixes in the compilation of forall statements. | leino | 2014-11-13 | |
| | ||||
* | Merge | leino | 2014-11-13 | |
|\ | ||||
* | | Use arbitrary lookahead to determine if the next expression is a lambda ↵ | leino | 2014-11-13 | |
| | | | | | | | | expression. | |||
* | | Took a pass through the whole grammar to clean up allowSemi/allowLambda ↵ | leino | 2014-11-11 | |
| | | | | | | | | parameters | |||
* | | Cleaned up a number of LL(1) conflicts in the grammar (I wish Coco/R ↵ | leino | 2014-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) | Rustan Leino | 2014-11-07 | |
|/ | ||||
* | Resolved several more LL(1) warnings in the grammar | Rustan Leino | 2014-11-06 | |
| | ||||
* | Merge | leino | 2014-11-06 | |
|\ | ||||
* | | Started fixing a number of LL(1) warnings | leino | 2014-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 trait | Reza Ahmadi | 2014-11-05 | |
| | | ||||
| * | Extracted a separate class to generate fresh variable names. | wuestholz | 2014-11-06 | |
| | | ||||
| * | Updated test. | chmaria | 2014-11-06 | |
| | | ||||
| * | Added computation of free variables in dirty while statements. | chmaria | 2014-11-06 | |
|/ | ||||
* | Merge | Rustan Leino | 2014-11-05 | |
|\ | ||||
* | | Temporarily disabled one of the methods in NumberRepresentations.dfy -- this ↵ | leino | 2014-11-05 | |
| | | | | | | | | needs to be addressed in some way that will produce stable verification results | |||
* | | Merge | leino | 2014-11-05 | |
|\ \ | ||||
| * | | Refactored the generation of unique IDs for temporary variable names. | wuestholz | 2014-11-05 | |
| | | | ||||
| * | | Did some refactoring. | wuestholz | 2014-11-05 | |
| | | | ||||
* | | | Merge | leino | 2014-11-04 | |
|\| | | ||||
* | | | Merge | leino | 2014-11-04 | |
|\ \ \ | ||||
* | | | | Refactored SnapshotableTrees a bit and made it verify in a reasonable amount ↵ | leino | 2014-11-04 | |
| | | | | | | | | | | | | | | | | of time :) | |||
| | * | | Made dirty statements ghost. | chmaria | 2014-11-04 | |
| | | | | ||||
| | | * | Merge | Rustan Leino | 2014-11-03 | |
| | | |\ | | | |/ | | |/| | ||||
| | | * | Updated a test case for new syntax and convensions | Rustan Leino | 2014-11-03 | |
| | | | | ||||
| | * | | Fixed test output after refactoring in Boogie. | wuestholz | 2014-11-03 | |
| | | | | ||||
| | * | | Fixed test output after refactoring in Boogie. | wuestholz | 2014-11-02 | |
| | | | | ||||
| * | | | Merge | leino | 2014-11-01 | |
| |\| | | ||||
| * | | | Various DafnyPrelude.bpl cleanup. | leino | 2014-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. | chmaria | 2014-11-01 | |
| | | | | ||||
| | * | | Added initial support for dirty while statements. | chmaria | 2014-11-01 | |
| | | | | ||||
| * | | | Improved power of axioms Seq#FromArray | leino | 2014-10-31 | |
| |/ / | ||||
| * | | Allow assignment LHSs in a forall statement to be the same, so long as the ↵ | leino | 2014-10-30 | |
| | | | | | | | | | | | | | | | | | | they are assigned the same RHS value. Don't include havoc assignments in LHS-duplicate checks. | |||
| * | | Resolve attributes of a forall statement only after bound variables have ↵ | leino | 2014-10-29 | |
| |/ | | | | | | | | | | | | | been added to the scope. Resolve the attributes of local variables. Don't resolve attributes of PredicateStmt's more than once. | |||
| * | Fix bug in translation of 'new' for arrays | Rustan Leino | 2014-10-29 | |
| | | ||||
| * | Merge | leino | 2014-10-28 | |
| |\ | ||||
| * | | Fixed type-inference bug that could create cycles in proxy type graph | leino | 2014-10-28 | |
| | | | ||||
| * | | Disallow automatic completion of type arguments to the LHS of datatype ↵ | leino | 2014-10-28 | |
| | | | | | | | | | | | | declarations |