| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix issue 136. Less aggressive Lit wrap for assert/assume. |  qunyanm | 2016-02-26 |
| | | |||
| * | Merge |  Clément Pit--Claudel | 2015-09-02 |
| |\ | |||
| * | | Suppress many warnings in the test suite. | Clément Pit--Claudel | 2015-08-28 |
| | | | | | | | | | | | We already have separate tests for those, and we want the output to be the same with and without /autoTriggers. | ||
| | * | Added tests for Boogie's new /verifySnapshots:3, which will be used by the ↵ | Rustan Leino | 2015-08-28 |
| |/ | | | | Dafny emacs mode | ||
| * | Add change missing from bd47e3cdb79c | Clément Pit--Claudel | 2015-08-23 |
| | | |||
| * | Replace b || !b by true in Snapshots5.v1.dfy | Clément Pit--Claudel | 2015-08-23 |
| | | | | | | | We can't prove `exists b: bool :: b || !b` when splitting is enabled, at least for now, and there's already a separate test for that particular issue in wishlist/ | ||
| * | Add quotes in snapshot tests. | Clément Pit--Claudel | 2015-07-30 |
| | | | | | Thanks Valentin for elucidating this issue! | ||
| * | Fix: Unify column numbers in Dafny's errors | Clément Pit--Claudel | 2015-07-23 |
| | | | | | | | | | | Dafny counts from 0, but Boogie counts from 1. Tokens are 1-based. Thus when we print tokens, we need to decrement the column number. This was done for resolver errors, but not for verification or parsing errors. In addition, parsing errors were inconsistent with resolution errors case-wise. Unfortunately, the fix affects the output of many tests. | ||
| * | Split snapshot tests into separate files and add support for %S in runTests.py | Clément Pit--Claudel | 2015-07-20 |
| | | |||
| * | Updated test output after change in Boogie. | wuestholz | 2015-05-17 |
| | | |||
| * | This changeset changes the default visibility of a function/predicate body ↵ | leino | 2015-03-09 |
| | | | | | | | | | | | outside the module that declares it. The body is now visible across the module boundary. To contain the knowledge of the body inside the module, mark the function/predicate as 'protected'. Semantics of 'protected': * The definition (i.e., body) of a 'protected' function is not visible outside the defining module * The idea is that inside the defining module, a 'protected' function may or may not be opaque. However, this will be easier to support once opaque/reveal are language primitives. Therefore, for the time being, {:opaque} is not allowed to be applied to 'protected' functions. * In order to extend the definition of a predicate in a refinement module, the predicate must be 'protected' * The 'protected' status of a function must be preserved in refinement modules | ||
| * | Did some refactoring to improve the name generation. | wuestholz | 2015-01-27 |
| | | |||
| * | Did some refactoring to improve the name generation. | wuestholz | 2015-01-27 |
| | | |||
| * | Updated test output after change in Boogie. | wuestholz | 2015-01-24 |
| | | |||
| * | Merge | leino | 2015-01-03 |
| |\ | |||
| | * | Updated test output after change in Boogie. | wuestholz | 2014-12-28 |
| | | | |||
| * | | Language change: All functions and methods declared lexically outside any ↵ | leino | 2014-12-12 |
| |/ | | | | | | | | | | class are now automatically static, and fields are no longer allowed to be declared there. Stated differently, all heap state must now be declared inside an explicitly declared class, and functions and methods declared outside any class can be viewed as belonging to the module. The motivating benefit of this change is to no longer need the 'static' keyword when declaring a module of functions and methods. | ||
| * | Fixed two crashes in resolver | leino | 2014-12-10 |
| | | | | | Corrected merge | ||
| * | Merge | leino | 2014-12-09 |
| |\ | |||
| * | | Snapshot, to be continued | leino | 2014-12-02 |
| | | | |||
| | * | Updated test output after change in Boogie. | wuestholz | 2014-11-25 |
| |/ | |||
| * | Updated test output after change in Boogie. | wuestholz | 2014-11-16 |
| | | |||
| * | Fixed test output after refactoring in Boogie. | wuestholz | 2014-11-03 |
| | | |||
| * | Fixed test output after refactoring in Boogie. | wuestholz | 2014-11-02 |
| | | |||
| * | Minor change | wuestholz | 2014-10-19 |
| | | |||
| * | Minor change | wuestholz | 2014-10-18 |
| | | |||
| * | Made it use the '/traceCaching' flag for the 'snapshots' tests. | wuestholz | 2014-10-18 |
| | | |||
| * | Re-included lost calls to CheckEqualityTypes_Type | leino | 2014-08-13 |
| | | | | | Modified syntax in some tests, since predicates now require parentheses (without parentheses refers to a predicate, not an application of the predicate) | ||
| * | Added more tests. | wuestholz | 2014-07-15 |
| | | |||
| * | Added a test. | wuestholz | 2014-07-13 |
| | | |||
| * | Added more tests for the more advanced verification result caching. | wuestholz | 2014-07-10 |
| | | |||
| * | Worked on the more advanced verification result caching. | wuestholz | 2014-07-09 |
| | | |||
| * | Changed "dummy" checksums to "stable" and added more tests for the ↵ | wuestholz | 2014-07-03 |
| | | | | | verification result caching. | ||
| * | Added support for verifying Dafny program snapshots from the command-line. | wuestholz | 2014-07-01 |
 |
index : debian-dafny | |
| Debian packaging for Dafny |
| summaryrefslogtreecommitdiff |