		Search-engine friendly clone of the ACL2 documentation.

Vl-lintresult

Make-vl-lintresult

Basic constructor macro for vl-lintresult structures.

Syntax

(make-vl-lintresult [:design <design>] 
                    [:design0 <design0>] 
                    [:design-orig <design-orig>] 
                    [:sv-modalist <sv-modalist>] 
                    [:reportcard <reportcard>] 
                    [:sd-probs <sd-probs>])

This is the usual way to construct vl-lintresult structures. It simply conses together a structure with the specified fields.

This macro generates a new vl-lintresult structure from scratch. See also change-vl-lintresult, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-vl-lintresult

(defmacro make-vl-lintresult (&rest args)
  (std::make-aggregate 'vl-lintresult
                       args
                       '((:design)
                         (:design0)
                         (:design-orig)
                         (:sv-modalist)
                         (:reportcard)
                         (:sd-probs))
                       'make-vl-lintresult
                       nil))

Function: vl-lintresult

(defun vl-lintresult (design design0 design-orig
                             sv-modalist reportcard sd-probs)
  (declare (xargs :guard (and (vl-design-p design)
                              (vl-design-p design0)
                              (vl-design-p design-orig)
                              (sv::modalist-p sv-modalist)
                              (vl-reportcard-p reportcard)
                              (sd-problemlist-p sd-probs))))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-lintresult))
    (declare (ignorable __function__))
    (b* ((design (mbe :logic (vl-design-fix design)
                      :exec design))
         (design0 (mbe :logic (vl-design-fix design0)
                       :exec design0))
         (design-orig (mbe :logic (vl-design-fix design-orig)
                           :exec design-orig))
         (sv-modalist (mbe :logic (sv::modalist-fix sv-modalist)
                           :exec sv-modalist))
         (reportcard (mbe :logic (vl-reportcard-fix reportcard)
                          :exec reportcard))
         (sd-probs (mbe :logic (sd-problemlist-fix sd-probs)
                        :exec sd-probs)))
      (cons :vl-lintresult (list (cons 'design design)
                                 (cons 'design0 design0)
                                 (cons 'design-orig design-orig)
                                 (cons 'sv-modalist sv-modalist)
                                 (cons 'reportcard reportcard)
                                 (cons 'sd-probs sd-probs))))))