Check if a Java block consists of
a single
If the check is successful,
we return the expression of the
Function:
(defun atj-check-single-return-with-expr (block) (declare (xargs :guard (jblockp block))) (let ((__function__ 'atj-check-single-return-with-expr)) (declare (ignorable __function__)) (b* (((fun (fail)) (mv nil (jexpr-name ""))) ((unless (= (len block) 1)) (fail)) (statem (car block)) ((unless (jstatem-case statem :return)) (fail)) (expr? (jstatem-return->expr? statem)) ((unless expr?) (fail))) (mv t expr?))))
Theorem:
(defthm booleanp-of-atj-check-single-return-with-expr.yes/no (b* (((mv ?yes/no ?expr) (atj-check-single-return-with-expr block))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm jexprp-of-atj-check-single-return-with-expr.expr (b* (((mv ?yes/no ?expr) (atj-check-single-return-with-expr block))) (jexprp expr)) :rule-classes :rewrite)