Analysis which computes an annotation for each function whether
The annotation for information about verification.
Debugging code to print sets of invariants
Get verification information for this function.
