summaryrefslogtreecommitdiff
Commit message (Collapse)AuthorAge
* Refactored code for dealing with SCCs in the call graph.Gravatar Rustan Leino2014-02-24
| | | | Fixed bug.
* Minor clean-up in a couple of test files.Gravatar Rustan Leino2014-02-24
|
* Fixed bugs in co-call checksGravatar Rustan Leino2014-02-23
|
* Added another colemma-calls-function-recursively testGravatar Rustan Leino2014-02-23
|
* Fixed some checking of recursive method/copredicate callsGravatar Rustan Leino2014-02-23
|
* Fixed build-break typoGravatar Rustan Leino2014-02-23
|
* Deprecated "comethod" keyword in favor of "colemma". (Also, "prefix method" ↵Gravatar Rustan Leino2014-02-23
| | | | -> "prefix lemma")
* Allow unary minus on realsGravatar Rustan Leino2014-02-13
|
* Syntax highlighting for realsGravatar Rustan Leino2014-02-13
|
* New test file: dafny4/NumberRepresentations.dfyGravatar Rustan Leino2014-02-13
|
* Fixed crash in parserGravatar Rustan Leino2014-02-13
|
* Added to the test suite a Dafny version of Basics.v from the "Software ↵Gravatar Rustan Leino2014-02-13
| | | | Foundations" book (Pierce et al.)
* Increased space around "..." in latex style for Dafny.Gravatar Rustan Leino2014-02-13
|
* Fix soundness bug (Issue #9 on dafny.codeplex.com) in function axiom for ↵Gravatar Rustan Leino2014-02-13
| | | | | | literals. Added axiom to better handle DtAlloc/GenericAlloc correspondence (which improves handling of computations).
* Updated test suite after a Boogie bug fix for realsGravatar Rustan Leino2014-02-10
|
* MergeGravatar Bryan Parno2014-02-10
|\
* | Add basic tests for realsGravatar Bryan Parno2014-02-10
| |
| * Italicize attributes in latex mode for DafnyGravatar Rustan Leino2014-02-10
|/
* Preliminary support for reals in Dafny specs. No compiler suport yet.Gravatar Bryan Parno2014-02-10
|
* Added examples from the Kozen and Silva paper "Practical Coinduction".Gravatar Rustan Leino2014-02-10
|
* Fixed bug in DafnyExtension (hover text computation would crash if ↵Gravatar Rustan Leino2014-02-06
| | | | | | Translator had not been run). Fixed duplicate hover text information for Lines of calc statements.
* Removed some blank lines at the end of hover texts.Gravatar Rustan Leino2014-02-06
|
* MergeGravatar Rustan Leino2014-02-04
|\
* | Mark auto-generated expressions (in "decreases" clauses) and don't use these ↵Gravatar Rustan Leino2014-02-04
| | | | | | | | when figuring out hover text.
| * Provide more detailed feedback for errors involving if-then-elseGravatar Bryan Parno2014-02-03
| |
| * Some simplifications to the proof of GHC MergeSort.Gravatar Rustan Leino2014-02-01
|/
* Fixed bug that misclassified a ghost statementGravatar Rustan Leino2014-01-31
|
* Compile to .exe only if the Main method has no user-defined preconditions.Gravatar Rustan Leino2014-01-31
| | | | If Main is already declared as static, don't produce a second static Main.
* Produce hover text for many of the refinement omissions (i.e., "..." and the ↵Gravatar Rustan Leino2014-01-31
| | | | like).
* Added an alternative statement of the prime theoremGravatar Rustan Leino2014-01-24
|
* Fix a bug in the interaction between opaque and genericsGravatar Bryan Parno2014-01-23
|
* Fix minor issue in compilation of main methods.Gravatar wuestholz2014-01-17
|
* Version 1.8.0.10115 release candidateGravatar Rustan Leino2014-01-15
|
* MergeGravatar Rustan Leino2014-01-14
|\
* | Improve error information by generating "Related location" information that ↵Gravatar Rustan Leino2014-01-14
| | | | | | | | traces into preconditions of called functions
| * Added a missing autoReq resolution stepGravatar Bryan Parno2014-01-14
| |
| * MergeGravatar Bryan Parno2014-01-13
| |\ | |/ |/|
| * Improve autoReq's interactions with opaqueGravatar Bryan Parno2014-01-13
| |
* | Supply C# compiler switch /nowarn:0219, which suppresses any warning CS0219 ↵Gravatar Rustan Leino2014-01-13
| | | | | | | | about variables not being used.
* | MergeGravatar Rustan Leino2014-01-13
|\|
* | Added /compile:3, which compiles in memory and then executes the program (if ↵Gravatar Rustan Leino2014-01-13
| | | | | | | | there is a Main and there are no errors). Primarily intended for use with rise4fun.
| * Small fix to the order in which AutoReq adds its requirements.Gravatar Bryan Parno2014-01-13
|/
* Proof that there is no bound on the size of prime numbersGravatar Rustan Leino2014-01-11
|
* Fixed spurious complaint about assignment to non-ghost variableGravatar Rustan Leino2014-01-11
|
* MergeGravatar Rustan Leino2014-01-11
|\
| * A better fix to deal with StaticReceiverTypes affected by autoReq.Gravatar Bryan Parno2014-01-10
| |
* | MergeGravatar Rustan Leino2014-01-10
|\|
* | GHC-MergeSort: removed lemmas and proof steps rendered unnecessary now that ↵Gravatar Rustan Leino2014-01-09
| | | | | | | | axioms for functions with match'es are no longer specialized
| * MergeGravatar Bryan Parno2014-01-09
| |\ | |/ |/|
| * Fixed a resolve bug for UserDefinedTypesGravatar Bryan Parno2014-01-09
| |
generated by cgit v1.2.3 (git 2.39.1) at 2024-09-09 07:37:13 +0000