Maybe warn about deprecated DPI imports/exports. Compatible with seq and styled after vl-parse-warning.
(vl-warn-about-deprecated-dpi spec name importp &key (tokstream 'tokstream)) → (mv errmsg value new-tokstream)
The SystemVerilog-2012 spec (Section 35.5.4, Page 908) requires implementations to generate a compile time warning or error when "DPI" is used instead of "DPI-C". We create this warning here, if necessary.
Function:
(defun vl-warn-about-deprecated-dpi-fn (spec name importp tokstream) (declare (xargs :stobjs (tokstream))) (declare (xargs :guard (and (vl-dpispec-p spec) (vl-idtoken-p name) (booleanp importp)))) (let ((__function__ 'vl-warn-about-deprecated-dpi)) (declare (ignorable __function__)) (b* (((unless (vl-dpispec-equiv spec :vl-dpi)) (mv nil nil tokstream)) (warning (make-vl-warning :type :vl-warn-deprecated-dpi :msg "At ~a0: ~s1 of ~s2: \"DPI\" is deprecated and should ~ be replaced with \"DPI-C\", but note that use of the ~ \"DPI-C\" string may require changes in the DPI ~ application's C code." :args (list (vl-token->loc name) (if importp "import" "export") (vl-idtoken->name name)) :fatalp nil :fn __function__)) (tokstream (vl-tokstream-add-warning warning))) (mv nil nil tokstream))))
Theorem:
(defthm not-of-vl-warn-about-deprecated-dpi.errmsg (b* (((mv ?errmsg acl2::?value ?new-tokstream) (vl-warn-about-deprecated-dpi-fn spec name importp tokstream))) (not errmsg)) :rule-classes :rewrite)
Theorem:
(defthm not-of-vl-warn-about-deprecated-dpi.value (b* (((mv ?errmsg acl2::?value ?new-tokstream) (vl-warn-about-deprecated-dpi-fn spec name importp tokstream))) (not value)) :rule-classes :rewrite)
Theorem:
(defthm vl-tokstream->tokens-of-vl-warn-about-deprecated-dpi (b* (((mv ?errmsg acl2::?value ?new-tokstream) (vl-warn-about-deprecated-dpi-fn spec name importp tokstream))) (equal (vl-tokstream->tokens :tokstream new-tokstream) (vl-tokstream->tokens))) :rule-classes :rewrite)