summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Add code to calculate various interesting statistics about Dafny files.Gravatar Bryan Parno2015-07-01
|
* MergeGravatar leino2015-06-25
|\
* | Tried to reduce frame-axiom instantiations by saying the earlier heap must ↵Gravatar leino2015-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 ↵Gravatar leino2015-06-25
| | | | | | | | currently unused in the test suite)
| * Fix issue #85. Only try to interpret an identifier as a datatype constructorGravatar qunyanm2015-06-22
| | | | | | | | when the datetype is not null.
| * Fix various bugs in nested match patterns listed in issue #83Gravatar qunyanm2015-06-19
|/
* Auto-merged heads.Gravatar Michael Lowell Roberts2015-06-16
|\
* | System.Collections.Immutable.dll is now stored in the Binaries directory and ↵Gravatar Michael Lowell Roberts2015-06-16
| | | | | | | | copied to the output directory when the /optimize flag is used.
| * Changed logical order of requires and reads clauses on functions. Reads clausesGravatar Rustan Leino2015-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 ↵Gravatar Rustan Leino2015-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 testsGravatar Rustan Leino2015-06-15
| |
| * More reads testsGravatar Rustan Leino2015-06-15
| |
| * Postpone reads checks of function preconditions until after the entire ↵Gravatar leino2015-06-15
| | | | | | | | precondition has otherwise been checked for well-formedness
| * More tests of reads-clause checkingGravatar Rustan Leino2015-06-15
| |
| * Little edits in new CheckWellformedAndAssume codeGravatar leino2015-06-12
| |
| * MergeGravatar leino2015-06-12
| |\
| * | Added /vcs... cop-out to test case to make it go throughGravatar leino2015-06-12
| | |
| | * Fix a bug spotted by Chris in my BigInteger patch; thanks!Gravatar Clément Pit--Claudel2015-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.
| * | MergeGravatar leino2015-06-12
| |\|
| * | Combined some common routines into CheckWellformedAndAssume, which also ↵Gravatar leino2015-06-12
| | | | | | | | | | | | allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
| | * MergeGravatar Clément Pit--Claudel2015-06-12
| | |\ | |_|/ |/| |
| | * Small fix in runTests.pyGravatar Clément Pit--Claudel2015-06-12
| | |
* | | mergeGravatar Michael Lowell Roberts2015-06-12
|\ \ \ | | |/ | |/|
* | | added -optimize option to compiler.Gravatar Michael Lowell Roberts2015-06-12
| |/ |/|
| * Add missing default parameter in runTests.pyGravatar Clément Pit--Claudel2015-06-11
| |
| * A few more improvements to runTests.pyGravatar Clément Pit--Claudel2015-06-11
| |
| * Small improvements to runTests.pyGravatar Clément Pit--Claudel2015-06-10
|/
* Add a compatibility layer over BigInteger.ParseGravatar Clément Pit--Claudel2015-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.
* MergeGravatar Clément Pit--Claudel2015-06-08
|\
| * MergeGravatar Bryan Parno2015-06-08
| |\
| * | Update the hash code for datatypes to use the djb2 hash algorithm,Gravatar Bryan Parno2015-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 callsGravatar Bryan Parno2015-06-08
| | |
* | | Fix the UseBaseNameForFileName flag; it shouldn't set the return code to zero.Gravatar Clément Pit--Claudel2015-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 constructsGravatar Clément Pit--Claudel2015-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 infrastructureGravatar Clément Pit--Claudel2015-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.Gravatar Clément Pit--Claudel2015-06-07
|/
* Generate #requires function for OpaqueFunction.Gravatar qunyanm2015-06-04
|
* Added {:auto_generated} trigger, which indicates that a declaration was not ↵Gravatar Rustan Leino2015-06-02
| | | | explicitly mentioned in the input. This lets the Dafny IDE know not to add hovertext for these declarations.
* MergeGravatar leino2015-05-29
|\
| * Add an infinite set collection type.Gravatar qunyanm2015-05-29
| |
* | Improvements in traits test caseGravatar leino2015-05-29
| |
* | Improvements to Nipkow and Klein test cases: Changed imap to map, removed ↵Gravatar leino2015-05-29
| | | | | | | | need for Total
* | MergeGravatar leino2015-05-29
|\|
* | Bug fix in type-antecedent for traits in allocation axiomsGravatar leino2015-05-29
| |
| * MergeGravatar Rustan Leino2015-05-29
| |\
| * | Changes to ComputeFreeVariables--bug fix as well as beautificationGravatar Rustan Leino2015-05-29
| | |
| | * Fix build break. Part of the change was not checked in last check-in somehow.Gravatar qunyanm2015-05-19
| | |
| | * Fix issue #81. Pass a call's TypeArgumentSubstitution to CheckCallTermination.Gravatar qunyanm2015-05-18
| | |
| | * DafnyExtension: Added experimental support for diagnosing timeouts.Gravatar wuestholz2015-05-18
| | |
| | * Updated test output after change in Boogie.Gravatar wuestholz2015-05-17
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 04:32:54 +0000