Main function the parser uses for creating function declarations.
(vl-make-fundecl-for-parser &key name lifetime rettype inputs decls loaditems body atts loc) → fun
This mainly just adds the
Function:
(defun vl-make-fundecl-for-parser-fn (name lifetime rettype inputs decls loaditems body atts loc) (declare (xargs :guard (and (stringp name) (vl-lifetime-p lifetime) (vl-datatype-p rettype) (vl-portdecllist-p inputs) (vl-blockitemlist-p decls) (vl-portdecl-or-blockitem-list-p loaditems) (vl-stmt-p body) (vl-atts-p atts) (vl-location-p loc)))) (let ((__function__ 'vl-make-fundecl-for-parser)) (declare (ignorable __function__)) (b* ((port-vars (vl-make-hidden-variables-for-portdecls inputs)) (ret-var (make-vl-vardecl :name name :type rettype :atts (list (list (hons-copy "VL_HIDDEN_DECL_FOR_TASKPORT"))) :loc loc)) (decls (append port-vars (list ret-var) decls)) ((mv vardecls paramdecls imports typedefs) (vl-sort-blockitems decls))) (make-vl-fundecl :name name :lifetime lifetime :rettype rettype :portdecls inputs :loaditems loaditems :vardecls vardecls :paramdecls paramdecls :imports imports :typedefs typedefs :body body :atts atts :loc loc))))
Theorem:
(defthm vl-fundecl-p-of-vl-make-fundecl-for-parser (b* ((fun (vl-make-fundecl-for-parser-fn name lifetime rettype inputs decls loaditems body atts loc))) (vl-fundecl-p fun)) :rule-classes :rewrite)