summaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
...
* | | Removed specContextOnly parameter from ResolveStatement.Gravatar leino2015-09-28
* | | Removed the 'inSpecOnlyContext' map that had been part of the resolution ofGravatar leino2015-09-28
* | | Renamed CheckIsNonGhost to CheckIsCompilable.Gravatar leino2015-09-28
* | | Removed more traces of the previous resolution checks that happened during pa...Gravatar leino2015-09-28
* | | Additional testsGravatar leino2015-09-28
* | | Whitespace changes in test fileGravatar leino2015-09-28
* | | Improvements in proofsGravatar leino2015-09-28
* | | Changed computation of ghosts until pass 2 of resolution.Gravatar leino2015-09-28
| | * merge headsGravatar Michael Lowell Roberts2015-09-23
| | |\
| | * | fixed bugs related to identifying newtypes as types of integers and reals.Gravatar Michael Lowell Roberts2015-09-23
| | | * Revert part of 1899 (47fd7d09d605, "Fix a check that occasionally led to ...")Gravatar Clément Pit--Claudel2015-09-23
| | |/
| * | Fixed typo in INSTALL fileGravatar leino2015-09-23
* | | A test file with an example of least vs greatest fixpoints.Gravatar leino2015-09-22
| | * fix for warnings related to deprecated z3 options (please update to the lates...Gravatar Michael Lowell Roberts2015-09-22
* | | Removed unused code (old code from previous ghost-statement handling)Gravatar leino2015-09-21
* | | Moved premature uses of .IsGhost for Statement'sGravatar leino2015-09-21
| | * Auto-merged heads.Gravatar Michael Lowell Roberts2015-09-21
| | |\
| | * | merged IronDafny updates. two unit tests related to traits do not pass if ENA...Gravatar Michael Lowell Roberts2015-09-21
* | | | Added back in various ghost testsGravatar leino2015-09-20
* | | | Changes that only affect line numbers in test caseGravatar leino2015-09-20
* | | | Removed tabs from test fileGravatar leino2015-09-20
* | | | Adjusted (corrected, I think) test outputGravatar leino2015-09-20
* | | | Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
| | | * Fix a check that occasionally led to an out of bounds exception in the extensionGravatar Bryan Parno2015-09-17
| | |/ | |/|
| | * Fix for soundness bug discovered in SeqFromArray.Gravatar Michael Lowell Roberts2015-09-17
| | * Only print extraneous comments if asked.Gravatar Michael Lowell Roberts2015-09-17
| |/
* | MergeGravatar leino2015-09-11
|\|
| * Fix #90Gravatar Clément Pit--Claudel2015-09-09
| * Proof that Ackermann can be curried and that it is monotonic in both arguments.Gravatar Rustan Leino2015-09-08
| * MergeGravatar Clément Pit--Claudel2015-09-02
| |\
* | | Refactored most of UnifyTypes calls into a ConstrainTypes method, preparing f...Gravatar leino2015-08-31
| | * fix for comparison error in prelude when using /optimize.Gravatar Michael Lowell Roberts2015-08-31
| |/ |/|
| * Fix some tests by locally disabling auto triggersGravatar Clément Pit--Claudel2015-08-28
| * Align the server's default kill time with the one of the VS extensionGravatar Clément Pit--Claudel2015-08-28
| * Add a small test from a discussion with BryanGravatar Clément Pit--Claudel2015-08-28
| * Implement workarounds for some tests that fail with /autoTriggers.Gravatar Clément Pit--Claudel2015-08-28
| * Suppress many warnings in the test suite.Gravatar Clément Pit--Claudel2015-08-28
| * Clarify a commentGravatar Clément Pit--Claudel2015-08-28
| * Implement {:nowarn}, clarify some messages, and add a few testsGravatar Clément Pit--Claudel2015-08-28
| * Put contents od release packages into a dafny/ directoryGravatar Clément Pit--Claudel2015-08-28
* | MergeGravatar Rustan Leino2015-08-28
|\|
* | Added tests for Boogie's new /verifySnapshots:3, which will be used by the Da...Gravatar Rustan Leino2015-08-28
* | Fixed spelling mistake in test fileGravatar Rustan Leino2015-08-28
| * Add a small test from the IronClad notebookGravatar Clément Pit--Claudel2015-08-27
| * Tiny cleanup in TriggersCollectorGravatar Clément Pit--Claudel2015-08-27
| * Add a tip to the packaging scriptGravatar Clément Pit--Claudel2015-08-27
| * Update INSTALL to reflect the latest packaging changesGravatar Clément Pit--Claudel2015-08-27
| * package.py: Keep z3's exec bits, and set the exec bit on the dafny/ scriptGravatar Clément Pit--Claudel2015-08-27
| * More fixes to the packaging scriptGravatar Clément Pit--Claudel2015-08-27
| * Make the packaging script Windows-compatibleGravatar Clément Pit--Claudel2015-08-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 02:25:00 +0000