|
|
|---|
|
|
|
|---|
Customizable hook to run at the end of VL Lint.
This is an attachment that allows you to extend VL Lint with support additional, customized (e.g., methodology-specific) checks and custom reports.
It gets called as the last step of run-vl-lint and has access to the entire vl-lintconfig and the corresponding vl-loadconfig, the full vl-loadresult, and also the full vl-lintresult which contains all the warnings and the final, fully processed design.
Theorem:
(defthm state-p1-of-vl-lint-extra-actions (implies (state-p1 state) (state-p1 (vl-lint-extra-actions lintconfig loadconfig loadresult lintresult state))))