summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* Introduced keywords "lemma" (like a "ghost method", but not allowed to have a...Gravatar Rustan Leino2013-08-02
* More and improved CaptureState infoGravatar Rustan Leino2013-08-02
* Merge adjustmentsGravatar Rustan Leino2013-08-02
|\
* | Added activation antecedents for co-predicate / prefix predicate axioms.Gravatar Rustan Leino2013-08-02
* | Changed the encoding of recursive functions. Previous, three hardcoded layer...Gravatar Rustan Leino2013-08-02
| * DafnyExtension: Fixed a minor issue in the error selection.Gravatar wuestholz2013-08-01
| * Fixed contract build errorsGravatar Rustan Leino2013-08-01
| * DafnyExtension: Fixed a minor issue in the error selection.Gravatar wuestholz2013-08-01
| * DafnyExtension: Made it select the last error state by default when an error ...Gravatar wuestholz2013-08-01
| * DafnyExtension: Made it display if a variable was updated in a given model st...Gravatar wuestholz2013-08-01
| * DafnyExtension: Made it display all variable values from the model.Gravatar wuestholz2013-08-01
| * DafnyExtension: Increased the font size for the BVD tool window.Gravatar wuestholz2013-07-31
| * Added support for more fine-grained generation of unique names.Gravatar wuestholz2013-07-31
| * Regenerated Parser after a merge.Gravatar Nadia Polikarpova2013-07-31
| * MergeGravatar Nadia Polikarpova2013-07-31
| |\
| * | Allowing dangling hints in calculations.Gravatar Nadia Polikarpova2013-07-31
|/ /
| * DafnyExtension: Added support for displaying values from the model as hover t...Gravatar wuestholz2013-07-30
| * Add support for hexidecimal numbers.Gravatar parno2013-07-30
| * Minor changeGravatar wuestholz2013-07-30
|/
* Added "co-recursive call" to drop boxGravatar Rustan Leino2013-07-30
* Simplified the guardedness checking algorithmGravatar Rustan Leino2013-07-30
* Co-recursion, now sounder than ever!Gravatar Rustan Leino2013-07-30
* Fixed issue in the computation of checksums.Gravatar wuestholz2013-07-29
* Fixed distinction between intra/inter-module calls and refined calls.Gravatar Rustan Leino2013-07-29
* MergeGravatar Rustan Leino2013-07-29
|\
* | Make functions and predicates be opaque outside the defining module -- only t...Gravatar Rustan Leino2013-07-29
| * DafnyExtension: Make it possible to enable and disable BVD.Gravatar wuestholz2013-07-28
| * DafnyExtension: Hide the state list and the menu strip in BVD.Gravatar wuestholz2013-07-28
| * DafnyExtension: Avoid allocating too much space for the error model adornments.Gravatar wuestholz2013-07-28
| * DafnyExtension: Update the error model when a new error state is selected.Gravatar wuestholz2013-07-28
| * DafnyExtension: Did some refactoring to integrate the Dafny menu more tightly.Gravatar wuestholz2013-07-28
| * DafnyExtension: minor changeGravatar wuestholz2013-07-26
| * DafnyExtension: Did some refactoring and worked towards integrating the Dafny...Gravatar wuestholz2013-07-26
| * Fixed build failure.Gravatar wuestholz2013-07-25
|/
* MergeGravatar Rustan Leino2013-07-24
|\
* | Allow field names to be sequences of digits (this is nice, for example, to de...Gravatar Rustan Leino2013-07-24
* | Make sure there's at least one CaptureState per method (otherwise BVD doesn't...Gravatar Rustan Leino2013-07-24
| * DafnyExtension: minor fixGravatar wuestholz2013-07-23
|/
* Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-07-22
* Fixed issues due to merge.Gravatar wuestholz2013-07-22
* MergeGravatar Rustan Leino2013-07-22
|\
* | Fixed build failures from recent Boogie refactoring.Gravatar Rustan Leino2013-07-22
| * Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-07-22
|/
* Fixed build failures due to changes in Boogie.Gravatar wuestholz2013-07-22
* DafnyExtension: Worked on improving the error selection and visualization.Gravatar wuestholz2013-07-21
* DafnyExtension: Added support for selecting errors and showing the model in BVD.Gravatar wuestholz2013-07-15
* DafnyExtension: Added support for collecting additional information during re...Gravatar wuestholz2013-07-15
* DafnyExtension: Made the 'ProgressTagger' use tasks instead of threads for in...Gravatar wuestholz2013-07-15
* DafnyExtension: Worked on integrating BVD.Gravatar wuestholz2013-07-14
* DafnyExtension: Enabled model extraction for verification failures.Gravatar wuestholz2013-07-12