summaryrefslogtreecommitdiff
path: root/Source
Commit message (Expand)AuthorAge
* 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
* DafnyExtension: Fixed an error list issue.Gravatar wuestholz2013-07-12
* Fixed printer bug to handle static receivers in function call expressions. (T...Gravatar chmaria2013-07-11
* Because of neighboring parse conflict handlers, must call ResetPeek()Gravatar Rustan Leino2013-07-10
* Look through paren expressions when determining a default loop decreases clauseGravatar Rustan Leino2013-07-10
* MergeGravatar Rustan Leino2013-07-10
|\
* | Fixed parsing bug in "if" and "while" guardsGravatar Rustan Leino2013-07-10
| * Did some refactoring of the interaction with the Boogie execution engine.Gravatar wuestholz2013-07-10
|/
* DafnyExtension: Fixed flickering of errors in the error list.Gravatar wuestholz2013-07-10
* DafnyExtension: Integrated support for multiple Z3 instances in Boogie (incl....Gravatar wuestholz2013-07-09
* Datatypes with ghost fields (that is, with constructors with ghost parameters...Gravatar Rustan Leino2013-07-09
* Fixed an issue in the computation of checksums.Gravatar wuestholz2013-07-07
* Merge.Gravatar Unknown2013-07-05
|\
* | No need to remove lit on RHSs now that Boogie's AI knows about Lit.Gravatar Unknown2013-07-05
| * DafnyExtension: Enabled verification result caching by default.Gravatar wuestholz2013-07-02
|/
* MergeGravatar Unknown2013-07-04
|\
* \ MergeGravatar Unknown2013-07-04
|\ \
| | * Fixed bugs reported as Issue 20.Gravatar Rustan Leino2013-07-04
| |/ |/|
| * Computations!Gravatar Unknown2013-07-04
* | Fixed bug with substitutions in let-such-that expressions. This cures Issue 22.Gravatar Rustan Leino2013-07-04
|/
* Fixed bug of inappropriate Boogie nameGravatar Rustan Leino2013-07-01
* Fixed soundness bug with co-recursive calls: co-recursive calls may now no l...Gravatar Rustan Leino2013-06-29
* Fixed unsoundness (and also allowed other, sound cases) in the admissability ...Gravatar Rustan Leino2013-06-28
* Changed ranking function for Seq, so that it's compatible with data types.Gravatar Unknown2013-06-26
* Fixed an issue in the computation of checksums.Gravatar wuestholz2013-06-25
* MergeGravatar Rustan Leino2013-06-25
|\
* | Fixed some Code Contract type errorsGravatar Rustan Leino2013-06-25
| * Fixed compilation bug where C# keywords were not being escapedGravatar Rustan Leino2013-06-25
| * DafnyExtension: Fixed a memory leak.Gravatar wuestholz2013-06-24
| * Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-24
|/
* DafnyExtension: Use tracking spans instead of regular spans.Gravatar wuestholz2013-06-21
* DafnyExtension: Made it display verification errors incrementally.Gravatar wuestholz2013-06-20
* Fixed a problem where changes to a substMap were not being undone, curing Iss...Gravatar Rustan Leino2013-06-20
* MergeGravatar Rustan Leino2013-06-20
|\
| * Beefed up axioms about cardinality and the empty (multi)set, which fixes Issu...Gravatar Rustan Leino2013-06-20
* | MergeGravatar Rustan Leino2013-06-20
|\ \
* | | Fixed some incorrectly formed Boogie code generated as a result of a "break" ...Gravatar Rustan Leino2013-06-20
| |/ |/|
* | Make "datatype constructor cases" axiom available whenever the discriminator ...Gravatar Rustan Leino2013-06-20
* | Fixed a contract.Gravatar wuestholz2013-06-20
* | Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-19
* | Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-19
* | Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-19
* | Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-18
* | Did some refactoring of the error reporting functionality.Gravatar wuestholz2013-06-18
* | DafnyExtension: Fixed an issue in the verification result caching.Gravatar wuestholz2013-06-17
* | DafnyExtension: Disabled the default console printer for Boogie.Gravatar wuestholz2013-06-13