Skip to content

Releases: dafny-lang/compiler-bootstrap

Dafny Auditor 3.9.0

14 Oct 21:19
Compare
Choose a tag to compare

This is the first release of a plugin for Dafny (v3.9.0 or later) that will identify and report on assumptions in Dafny programs. To use, unpack somewhere convenient and run

dafny /plugin:path/to/DafnyAuditor.dll <any other options you want, including .dfy files>

In this mode, it will issue a warning for every assumption it detects. It can also log a table of assumptions to a file. To generate an HTML log, run

dafny /plugin:path/to/DafnyAuditor.dll,report.html <any other options you want, including .dfy files>

This will result in an HTML table in report.html.