Ensure that there are no calls of array write methods in a block.
The two transformations described in atj-post-translation-remove-array-write-calls should remove all the calls of array write methods. Since this has not been formally proved, we check whether this is the case, via this predicate.
Function:
(defun atj-ensure-no-array-write-calls (block) (declare (xargs :guard (jblockp block))) (let ((__function__ 'atj-ensure-no-array-write-calls)) (declare (ignorable __function__)) (not (intersectp-equal (jblock-methods block) *atj-primarray-write-method-names*))))
Theorem:
(defthm booleanp-of-atj-ensure-no-array-write-calls (b* ((yes/no (atj-ensure-no-array-write-calls block))) (booleanp yes/no)) :rule-classes :rewrite)