summaryrefslogtreecommitdiff
path: root/Source/Dafny/DafnyOptions.cs
Commit message (Collapse)AuthorAge
* Minor change due to a change in BoogieGravatar wuestholz2015-01-13
|
* Added command-line switch /allowGlobals to simplify transition from language ↵Gravatar leino2015-01-07
| | | | changes introduced in changeset c56031307ac1
* Add a DafnyCC option that disables some of Dafny's cleverness to better ↵Gravatar Bryan Parno2014-10-27
| | | | match DafnyCC's capabilities
* Add support for counting spec/impl/proof lines by supressing, e.g., ghost ↵Gravatar Bryan Parno2014-10-27
| | | | statements
* Add an option to allow automatically generated requirements to be printedGravatar Bryan Parno2014-10-27
| | | | to a file, making them easier to inspect and manipulate.
* Add an option to use reduce Z3's knowledge of non-linear arithmetic.Gravatar Bryan Parno2014-10-24
| | | | Results in more manual work, but it also produces more predictable behavior.
* 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.
* Produce "tail recursive" hover text in the IDE only for methods that are ↵Gravatar Rustan Leino2013-12-13
| | | | recursive
* Add a command-line option to disable include directives.Gravatar Bryan Parno2013-12-13
|
* Fixed printing of Dafny version number.Gravatar Rustan Leino2013-01-23
|
* Put all sources under \Source directoryGravatar Rustan Leino2012-10-04
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 20:15:42 +0000