summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Shallow-copy quantifier attributes when splittingGravatar Clément Pit--Claudel2015-08-23
|
* Add a sanity check in QuantifiersCollectionGravatar Clément Pit--Claudel2015-08-23
|
* Improve error reporting for split quantifiersGravatar Clément Pit--Claudel2015-08-23
|
* Allow MultiSelectExpr as quantifier headsGravatar Clément Pit--Claudel2015-08-23
|
* Trivial code cleanupGravatar Clément Pit--Claudel2015-08-23
|
* Exclude axiom-profiler.html and z3.log files in the Test directoryGravatar Clément Pit--Claudel2015-08-23
|
* Fix: multi-dimensional OOB errors were sometimes reported on incorrect ↵Gravatar Clément Pit--Claudel2015-08-23
| | | | locations.
* Ignore .bpl files in the Test directoryGravatar Clément Pit--Claudel2015-08-22
|
* Add one more wish: it would be nice to be able to prove exists b: bool :: bGravatar Clément Pit--Claudel2015-08-22
| | | | | This is an issue because splitting `exists b: bool :: b || !b` produces two quantifiers that we don't know how to prove.
* Grant "wishlist/useless-casts-in-decreases-clauses.dfy"Gravatar Clément Pit--Claudel2015-08-22
|
* Add more wishes to the wishlistGravatar Clément Pit--Claudel2015-08-22
|
* Ignore flycheck_ and .orig filesGravatar Clément Pit--Claudel2015-08-22
|
* Look at the full quantifier to find loops, not just the term.Gravatar Clément Pit--Claudel2015-08-22
|
* Set exec flag on Binaries/z3Gravatar Clément Pit--Claudel2015-08-22
|
* Add a 'tutorial' folder to the distribution, with an initial example.Gravatar Clément Pit--Claudel2015-08-22
| | | | | | | | | | It would be nice to gather neat Dafny examples there; each new feature could have its own small file that demoes it, and we could also have examples that showcase stuff that we think is impressive. I'm adding this as a test folder, because it's important to check that these cool examples don't break, but the focus probably shouldn't be on exhaustively testing the features being demoed.
* MergeGravatar Clément Pit--Claudel2015-08-21
|\
* | Make `old` a special case for trigger generation.Gravatar Clément Pit--Claudel2015-08-21
| | | | | | | | | | | | Old is particular, because in old(g(f(x))), the triggers are old(g(x)) and old(f(x)). This has a number of implications; see the new tests files for more information.
* | Rephrase the message about triggers being rejected because they are too strongGravatar Clément Pit--Claudel2015-08-21
| |
* | Add a few things to the wishlistGravatar Clément Pit--Claudel2015-08-21
| |
* | Adjust WF checks to use unsplit quantifiers.Gravatar Clément Pit--Claudel2015-08-21
| | | | | | | | | | | | | | | | | | | | | | | | | | The logic about split quantifiers is that Boogie (and z3) should never realize that there was an unsplit quantifier. The WF check code does not produce a quantifier, at least in it's checking part; thus, it should use original quantifier. This fixes a problem in VerifyThis2015/Problem2.dfy with a null check, and a problem spotted by Chris, made into a test case saved in triggers/wf-checks-use-the-original-quantifier.dfy. The issue boiled down to being able to verify (forall x :: x != null && x.a == 0). Of course, the assumption that WF checks produce for a quantifier is a quantifier, so it uses the split expression.
* | Add some diversity to Dafny's alimentationGravatar Clément Pit--Claudel2015-08-21
| |
| * Make use of new syntax in a test fileGravatar Rustan Leino2015-08-21
| |
* | Interleave stderr output with test results; this allows one to print stuffGravatar Clément Pit--Claudel2015-08-21
| | | | | | | | directly to stderr in Dafny without breaking tests
* | Ignore flycheck_* files in runTestsGravatar Clément Pit--Claudel2015-08-21
| |
* | Add tests for display expressions used as triggersGravatar Clément Pit--Claudel2015-08-21
| |
* | Give up on trying to set the console's input encoding to UTF8Gravatar Clément Pit--Claudel2015-08-21
| | | | | | | | Fortunately, the server spec already assumes an ASCII input channel.
* | Allow display expressions as trigger termsGravatar Clément Pit--Claudel2015-08-21
| |
* | Add /printTooltips to trigger testsGravatar Clément Pit--Claudel2015-08-21
| |
* | Cleanup a number of FIXMEs that I had left in the codeGravatar Clément Pit--Claudel2015-08-20
| |
| * MergeGravatar Rustan Leino2015-08-20
| |\ | |/ |/|
| * Changed equality tests involving traits from using strings to using ↵Gravatar Rustan Leino2015-08-20
| | | | | | | | reference equality
| * Minor refactoringGravatar Rustan Leino2015-08-20
| |
| * Fixed compilation that involve enumeration over native-type newtype values.Gravatar Rustan Leino2015-08-20
| |
* | Make the dependency that DafnyServer has on DafnyPipeline explicitGravatar Clément Pit--Claudel2015-08-20
| |
* | Fix a typoGravatar Clément Pit--Claudel2015-08-20
| |
* | Implement the SelectTrigger method, removing redundant triggers.Gravatar Clément Pit--Claudel2015-08-20
| | | | | | | | | | | | | | | | | | The idea is that we define an partial order on triggers (which may contain multiple terms), and find all the maximal elements. The algorithm as implemented is rather inefficient; in particular, is does not look at the structure of the graph of the relation (thus is does many redundant comparisons). See triggers/useless-triggers-are-removed.dfy for an example where such a filter is useful.
* | Merge.Gravatar Clément Pit--Claudel2015-08-20
|\|
* | Move indentation of error messages to the ConsoleErrorReporterGravatar Clément Pit--Claudel2015-08-20
| | | | | | | | This indentation is just needed by CLI-based clients
* | Discard error messages that refer to a non-nested TokenWrapper.Gravatar Clément Pit--Claudel2015-08-20
| | | | | | | | | | | | | | | | The VS extension already did that, but it also filtered out nested tokens. That prevented info about triggers from being reported. Other interfaces (the CLI and Emacs, in particular) should have the same ability. Surprinsingly, this doesn't cause any tests failures.
| * Fixed bug in type unificationGravatar Rustan Leino2015-08-20
| |
| * MergeGravatar Rustan Leino2015-08-20
| |\
* | | Add unit tests for trigger-related error messagesGravatar Clément Pit--Claudel2015-08-20
| | |
* | | Simplify error reporting in the trigger generator to get cleaner messagesGravatar Clément Pit--Claudel2015-08-20
| | |
* | | Mark a few reporting functions as staticGravatar Clément Pit--Claudel2015-08-20
| | |
* | | Add a test to show how trigger splitting balances the downsides of loop ↵Gravatar Clément Pit--Claudel2015-08-20
| | | | | | | | | | | | detection
* | | Allow users to disable quantifier splitting by with a {:split false} attributeGravatar Clément Pit--Claudel2015-08-20
| | |
* | | Add a wishlist folder to the test suite, with things that we do not support ↵Gravatar Clément Pit--Claudel2015-08-19
| | | | | | | | | | | | | | | | | | | | | (yet!) The curent examples include semi-bugs regarding calc statements and strings, and stuff about sequences
* | | Add a test to check that there are as many errors as failed preconditionsGravatar Clément Pit--Claudel2015-08-19
| | |
* | | Add tests for quantifier splitting and trigger generationGravatar Clément Pit--Claudel2015-08-19
| | |
* | | Print matches for triggers as they appear in the bufferGravatar Clément Pit--Claudel2015-08-19
| | | | | | | | | | | | | | | Triggers themselves, however, are printed exactly as used. For example, a term (x !in s) yields a trigger (x in s).
generated by cgit v1.2.3 (git 2.39.1) at 2024-10-01 06:26:36 +0000