Check array indices against the corresponding array bounds.
(vl-follow-hidexpr-dimscheck name indices dims &key strictp) → err
Function:
(defun vl-follow-hidexpr-dimscheck-fn (name indices dims strictp) (declare (xargs :guard (and (stringp name) (vl-exprlist-p indices) (vl-packeddimensionlist-p dims) (booleanp strictp)))) (let ((__function__ 'vl-follow-hidexpr-dimscheck)) (declare (ignorable __function__)) (b* (((when (atom dims)) (if (atom indices) nil (cat "indexing into non-array " name))) ((when (atom indices)) (cat "no indices given for array " name)) ((when (same-lengthp indices dims)) (vl-follow-hidexpr-dimscheck-aux name indices dims :strictp strictp)) (found (len indices)) (need (len dims)) ((when (< found need)) (cat "too many indices for array " name))) (cat "not enough indices for array " name))))
Theorem:
(defthm maybe-stringp-of-vl-follow-hidexpr-dimscheck (b* ((err (vl-follow-hidexpr-dimscheck-fn name indices dims strictp))) (maybe-stringp err)) :rule-classes :type-prescription)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-of-str-fix-name (equal (vl-follow-hidexpr-dimscheck-fn (str-fix name) indices dims strictp) (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-fn name-equiv indices dims strictp))) :rule-classes :congruence)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-of-vl-exprlist-fix-indices (equal (vl-follow-hidexpr-dimscheck-fn name (vl-exprlist-fix indices) dims strictp) (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-vl-exprlist-equiv-congruence-on-indices (implies (vl-exprlist-equiv indices indices-equiv) (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-fn name indices-equiv dims strictp))) :rule-classes :congruence)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-of-vl-packeddimensionlist-fix-dims (equal (vl-follow-hidexpr-dimscheck-fn name indices (vl-packeddimensionlist-fix dims) strictp) (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-vl-packeddimensionlist-equiv-congruence-on-dims (implies (vl-packeddimensionlist-equiv dims dims-equiv) (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-fn name indices dims-equiv strictp))) :rule-classes :congruence)
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-of-bool-fix-strictp (equal (vl-follow-hidexpr-dimscheck-fn name indices dims (acl2::bool-fix strictp)) (vl-follow-hidexpr-dimscheck-fn name indices dims strictp)))
Theorem:
(defthm vl-follow-hidexpr-dimscheck-fn-iff-congruence-on-strictp (implies (iff strictp strictp-equiv) (equal (vl-follow-hidexpr-dimscheck-fn name indices dims strictp) (vl-follow-hidexpr-dimscheck-fn name indices dims strictp-equiv))) :rule-classes :congruence)