|
A tool to prove pre- or postconditions via an SMT solver (Z3) and to remove the statically proven conditions from a program.
Author: Michael Hanus
Version: September 2019
Constructors:
|
|
|
|
|
|
|
|
|
|
Transform a qualified name into a name of the corresponding function without precondition checking by adding the suffix "'NOCHECK".
|
Drops a possible "'NOCHECK" suffix from a qualified name. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Checks whether a file exists in one of the directories on the PATH. |
|
Shows a text with line numbers preceded: |