summaryrefslogtreecommitdiff
path: root/Test
Commit message (Expand)AuthorAge
* 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
* MergeGravatar Clément Pit--Claudel2015-07-28
|\
* | Save failing tests to failing.lst, making it easy to re-run themGravatar Clément Pit--Claudel2015-07-28
| * Renamed "ghost method" to "lemma" whenever appropriate (which is most of the ...Gravatar Rustan Leino2015-07-28
* | Clarify the inlining warning.Gravatar Clément Pit--Claudel2015-07-27
| * Renamed "ghost method" to "lemma" in a couple of test filesGravatar Rustan Leino2015-07-24
|/
* Bump up the time limit in runTests.py and save a bit of space in outputGravatar Clément Pit--Claudel2015-07-23
* Fix: Read clauses should be checked before lit liftingGravatar Clément Pit--Claudel2015-07-23
* Let runTests.py generate expect filesGravatar 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
* Small fix in runTests.pyGravatar Clément Pit--Claudel2015-07-21
* Update z3 to 4.4. One test had to be edited.Gravatar Clément Pit--Claudel2015-07-21
* MergeGravatar Clément Pit--Claudel2015-07-20
|\
* | Fix encoding in Dijkstra.pyGravatar Clément Pit--Claudel2015-07-20
* | runTests.py: Improve reports (show oldest thread) and fix colors on cygwinGravatar 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
|\
* | Clean up runTests after 2015/07/17 meetingGravatar 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
| * MergeGravatar Rustan Leino2015-07-16
| |\
| | * 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 broken interaction between triggers and inlining of function callsGravatar Clément Pit--Claudel2015-07-14
* | | Fix multiple tests that relied on z3 triggering on $BoxGravatar Clément Pit--Claudel2015-07-13
| * | [IronDafny] implemented workaround for "import opened" bug(s).Gravatar Michael Lowell Roberts2015-07-13
| * | Auto-merged heads.Gravatar Michael Lowell Roberts2015-07-08
| |\|
| * | added unit tests for exclusive refinement.Gravatar Michael Lowell Roberts2015-07-08
| | * 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
| |/
| * Added another lemma to a test fileGravatar Rustan Leino2015-07-02
| * MergeGravatar leino2015-07-01
| |\
| * | Fixed bug in BplImp!Gravatar leino2015-07-01
| | * Add the ability to specify how much "fuel" a function should have,Gravatar Bryan Parno2015-07-01
| |/ |/|
| * Fixed bugs in encoding of preconditions of function values, Issue #84.Gravatar leino2015-06-30
| * Additional test case for instance functionsGravatar leino2015-06-30
|/
* MergeGravatar leino2015-06-25
|\
* | Tried to reduce frame-axiom instantiations by saying the earlier heap must be...Gravatar 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
|/
* Changed logical order of requires and reads clauses on functions. Reads clausesGravatar Rustan Leino2015-06-15
* Do postponsed reads checking also for the body of functions -- see Test/dafny...Gravatar Rustan Leino2015-06-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 17:20:45 +0000