Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Merge | leino | 2015-06-25 |
|\ | |||
* | | Tried to reduce frame-axiom instantiations by saying the earlier heap must ↵ | leino | 2015-06-25 |
| | | | | | | | | | | | | be a "heap anchor". Currently, a heap is an anchor if it produced by a havoc (but not a direct update). | ||
* | | Removed unneeded :heapQuantifier from test case (rendinging this attribute ↵ | leino | 2015-06-25 |
| | | | | | | | | currently unused in the test suite) | ||
| * | Fix issue #85. Only try to interpret an identifier as a datatype constructor | qunyanm | 2015-06-22 |
| | | | | | | | | when the datetype is not null. | ||
| * | Fix various bugs in nested match patterns listed in issue #83 | qunyanm | 2015-06-19 |
|/ | |||
* | Auto-merged heads. | Michael Lowell Roberts | 2015-06-16 |
|\ | |||
* | | System.Collections.Immutable.dll is now stored in the Binaries directory and ↵ | Michael Lowell Roberts | 2015-06-16 |
| | | | | | | | | copied to the output directory when the /optimize flag is used. | ||
| * | Changed logical order of requires and reads clauses on functions. Reads clauses | Rustan Leino | 2015-06-15 |
| | | | | | | | | | | can now assume the precondition (as had also been the case back in the days when reads clauses had to be self framing). | ||
| * | Do postponsed reads checking also for the body of functions -- see ↵ | Rustan Leino | 2015-06-15 |
| | | | | | | | | | | | | Test/dafny0/Reads.dfy for benefits. (Unfortunately, this loses track of the "postcondition might not hold on this return path" locations, see Test/dafny0/FunctionSpecifications.dfy.) | ||
| * | Some more reads tests | Rustan Leino | 2015-06-15 |
| | | |||
| * | More reads tests | Rustan Leino | 2015-06-15 |
| | | |||
| * | Postpone reads checks of function preconditions until after the entire ↵ | leino | 2015-06-15 |
| | | | | | | | | precondition has otherwise been checked for well-formedness | ||
| * | More tests of reads-clause checking | Rustan Leino | 2015-06-15 |
| | | |||
| * | Little edits in new CheckWellformedAndAssume code | leino | 2015-06-12 |
| | | |||
| * | Merge | leino | 2015-06-12 |
| |\ | |||
| * | | Added /vcs... cop-out to test case to make it go through | leino | 2015-06-12 |
| | | | |||
| | * | Fix a bug spotted by Chris in my BigInteger patch; thanks! | Clément Pit--Claudel | 2015-06-12 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The problem was this: Console.WriteLine(Int64.Parse("08000000000000000", NumberStyles.HexNumber)); // => -9223372036854775808 Console.WriteLine(Int64.Parse("9223372036854775808")); // => Value was either too large or too small for an Int64. In other words, large hex numbers are interpreted as a sequence of bits, not as an actual number. | ||
| * | | Merge | leino | 2015-06-12 |
| |\| | |||
| * | | Combined some common routines into CheckWellformedAndAssume, which also ↵ | leino | 2015-06-12 |
| | | | | | | | | | | | | allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change) | ||
| | * | Merge | Clément Pit--Claudel | 2015-06-12 |
| | |\ | |_|/ |/| | | |||
| | * | Small fix in runTests.py | Clément Pit--Claudel | 2015-06-12 |
| | | | |||
* | | | merge | Michael Lowell Roberts | 2015-06-12 |
|\ \ \ | | |/ | |/| | |||
* | | | added -optimize option to compiler. | Michael Lowell Roberts | 2015-06-12 |
| |/ |/| | |||
| * | Add missing default parameter in runTests.py | Clément Pit--Claudel | 2015-06-11 |
| | | |||
| * | A few more improvements to runTests.py | Clément Pit--Claudel | 2015-06-11 |
| | | |||
| * | Small improvements to runTests.py | Clément Pit--Claudel | 2015-06-10 |
|/ | |||
* | Add a compatibility layer over BigInteger.Parse | Clément Pit--Claudel | 2015-06-07 |
| | | | | | | | Mono currently does not implement support for BigInteger.Parse, so use Int64 if possible, and throw the same error as was previously returned otherwise. This is not too much of a problem in practice, because most of the integers that we actually come across in real-life source files seem to fit in an Int64. | ||
* | Merge | Clément Pit--Claudel | 2015-06-08 |
|\ | |||
| * | Merge | Bryan Parno | 2015-06-08 |
| |\ | |||
| * | | Update the hash code for datatypes to use the djb2 hash algorithm, | Bryan Parno | 2015-06-08 |
| | | | | | | | | | | | | | | | rather than xor. The latter produces pessimal performance if the datatype contains duplicate data. | ||
| * | | Fix some issues when compiling generic types and generic function method calls | Bryan Parno | 2015-06-08 |
| | | | |||
* | | | Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero. | Clément Pit--Claudel | 2015-06-07 |
| | | | | | | | | | | | | | | | The test suite relies on error codes all being zero (except for preprocessing errors), so add a flag for that (as suggested in a source comment). | ||
* | | | Fix lit headers implicitly relying on bash-style constructs | Clément Pit--Claudel | 2015-06-08 |
| | | | | | | | | | | | | | | | Window's batch doesn't recognize ";" as a command separator; lit has a workaround for that, bu it's just as simple to do the right thing on our side. | ||
* | | | Add the beginning of a new testing infrastructure | Clément Pit--Claudel | 2015-06-08 |
| |/ |/| | | | | | | | | | | | | | | | | | | | | | runTests.py reads lit-style annotations, so we will be able to retain lit compatibility. This new framework adds: * Precise timings * Proper support for interrupting using Ctrl+C * Much better reporting (including tracking of error codes, and merging of successive reports for performance tracking) * No dependency on lit, OutputCheck, or Diff * Pretty colors! | ||
* | | Fix the Seq#Contain axiom; it should talk about T, not ref. | Clément Pit--Claudel | 2015-06-07 |
|/ | |||
* | Generate #requires function for OpaqueFunction. | qunyanm | 2015-06-04 |
| | |||
* | Added {:auto_generated} trigger, which indicates that a declaration was not ↵ | Rustan Leino | 2015-06-02 |
| | | | | explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations. | ||
* | Merge | leino | 2015-05-29 |
|\ | |||
| * | Add an infinite set collection type. | qunyanm | 2015-05-29 |
| | | |||
* | | Improvements in traits test case | leino | 2015-05-29 |
| | | |||
* | | Improvements to Nipkow and Klein test cases: Changed imap to map, removed ↵ | leino | 2015-05-29 |
| | | | | | | | | need for Total | ||
* | | Merge | leino | 2015-05-29 |
|\| | |||
* | | Bug fix in type-antecedent for traits in allocation axioms | leino | 2015-05-29 |
| | | |||
| * | Merge | Rustan Leino | 2015-05-29 |
| |\ | |||
| * | | Changes to ComputeFreeVariables--bug fix as well as beautification | Rustan Leino | 2015-05-29 |
| | | | |||
| | * | Fix build break. Part of the change was not checked in last check-in somehow. | qunyanm | 2015-05-19 |
| | | | |||
| | * | Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination. | qunyanm | 2015-05-18 |
| | | | |||
| | * | DafnyExtension: Added experimental support for diagnosing timeouts. | wuestholz | 2015-05-18 |
| | | | |||
| | * | Updated test output after change in Boogie. | wuestholz | 2015-05-17 |
| | | | |||
| | * | Fix issue #79. Allow tuple pattern matching with parenthesis only. | qunyanm | 2015-05-15 |
| | | |