summaryrefslogtreecommitdiff
path: root/Test/dafny0
Commit message (Expand)AuthorAge
* Preliminary refactoring of ghost-statement computations to after type checkingGravatar leino2015-09-20
* MergeGravatar Clément Pit--Claudel2015-09-02
|\
* | 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
| * Added tests for Boogie's new /verifySnapshots:3, which will be used by the Da...Gravatar Rustan Leino2015-08-28
|/
* Add change missing from bd47e3cdb79cGravatar Clément Pit--Claudel2015-08-23
* Added /autoTriggers to two tests where it only makes a cosmetic differenceGravatar Clément Pit--Claudel2015-08-23
* Replace b || !b by true in Snapshots5.v1.dfyGravatar Clément Pit--Claudel2015-08-23
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect locati...Gravatar Clément Pit--Claudel2015-08-23
* MergeGravatar Rustan Leino2015-08-20
|\
* | Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
| * Merge.Gravatar Clément Pit--Claudel2015-08-20
| |\ | |/ |/|
* | MergeGravatar Rustan Leino2015-08-20
|\ \
| | * Add a test to check that there are as many errors as failed preconditionsGravatar Clément Pit--Claudel2015-08-19
| |/
* | Refactored and improved bounds discoveryGravatar Rustan Leino2015-08-19
| * Merge.Gravatar Clément Pit--Claudel2015-08-19
| |\ | |/ |/|
| * Cleanup indentation of trigger warningsGravatar Clément Pit--Claudel2015-08-19
| * Draft out a more advanced version of trigger generationGravatar Clément Pit--Claudel2015-08-19
* | Change the induction heuristic for lemmas to also look in precondition for cl...Gravatar leino2015-08-12
|/
* MergeGravatar Rustan Leino2015-07-31
|\
| * MergeGravatar leino2015-07-31
| |\
* | | Bug fix: check that assign-such-that constraint is of type booleanGravatar Rustan Leino2015-07-31
| |/ |/|
| * Allow forall statements in refinementsGravatar leino2015-07-31
* | Add quotes in snapshot tests.Gravatar Clément Pit--Claudel2015-07-30
* | Fixed crash in resolution where, after reporting an error, the cases #type an...Gravatar Rustan Leino2015-07-29
* | Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
|/
* Fix: Read clauses should be checked before lit liftingGravatar Clément Pit--Claudel2015-07-23
* Fix: Unify column numbers in Dafny's errorsGravatar Clément Pit--Claudel2015-07-23
* Improved rank axioms for containersGravatar Rustan Leino2015-07-21
* MergeGravatar Clément Pit--Claudel2015-07-20
|\
| * clarified error message that occurs when the "opened" keyword is left off of ...Gravatar Michael Lowell Roberts2015-07-20
* | Split snapshot tests into separate files and add support for %S in runTests.pyGravatar Clément Pit--Claudel2015-07-20
|/
* Add missing .expect fileGravatar Clément Pit--Claudel2015-07-20
* Merge my autoTriggers work into the master branchGravatar Clément Pit--Claudel2015-07-17
|\
* | Enable autoTriggers in LitTriggers and SeqFromArrayGravatar Clément Pit--Claudel2015-07-17
* | Add /autoTriggers to TriggerInPredicate's RUN specificationGravatar Clément Pit--Claudel2015-07-17
| * Fixed bugs in the parsing of explicit type arguments.Gravatar Rustan Leino2015-07-16
* | Minor fixes in .expect filesGravatar Clément Pit--Claudel2015-07-16
* | Strip literals from triggersGravatar Clément Pit--Claudel2015-07-16
* | Fix multiple tests that relied on z3 triggering on $BoxGravatar Clément Pit--Claudel2015-07-13
| * Fixed crashes in overrides checking of function decreases clauses, and improv...Gravatar Rustan Leino2015-07-07
* | Add a new test, with a FIXMEGravatar Clément Pit--Claudel2015-07-06
| * Report warnings only once. (This is the last step in fixing Issue #86.)Gravatar Rustan Leino2015-07-06
| * Added command-line option /warnShadowing, which emits warnings if variables s...Gravatar Rustan Leino2015-07-02
| * Type parameters in method/function signatures are no longer auto-declared. A...Gravatar Rustan Leino2015-07-02
| * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
|/
* MergeGravatar leino2015-06-25
|\
* | Removed unneeded :heapQuantifier from test case (rendinging this attribute cu...Gravatar leino2015-06-25
| * Fix various bugs in nested match patterns listed in issue #83Gravatar qunyanm2015-06-19
|/