|
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: October 2024
Constructors:
Type synonym: TransStateM a = StateT TransState IO a
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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. |
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Returns the path of a file provided as an argument in the |
Checks whether a file exists in one of the directories on the PATH. |
|
Shows a text with line numbers preceded: |
The value of
|