Skip to content

Dafny Auditor 3.9.0

Latest
Compare
Choose a tag to compare
@atomb atomb released this 14 Oct 21:19
· 5 commits to main since this release

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.