Map a token that is an assembler qualifier to the corresponding assembler qualifier.
Function:
(defun token-to-asm-qualifier (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-asm-qualifier-p token))) (let ((__function__ 'token-to-asm-qualifier)) (declare (ignorable __function__)) (cond ((token-keywordp token "volatile") (asm-qual-volatile (keyword-uscores-none))) ((token-keywordp token "__volatile") (asm-qual-volatile (keyword-uscores-start))) ((token-keywordp token "__volatile__") (asm-qual-volatile (keyword-uscores-both))) ((token-keywordp token "inline") (asm-qual-inline (keyword-uscores-none))) ((token-keywordp token "__inline") (asm-qual-inline (keyword-uscores-start))) ((token-keywordp token "__inline__") (asm-qual-inline (keyword-uscores-both))) ((token-keywordp token "goto") (asm-qual-goto)) (t (prog2$ (impossible) (irr-asm-qual))))))
Theorem:
(defthm asm-qualp-of-token-to-asm-qualifier (b* ((asmqual (token-to-asm-qualifier token))) (asm-qualp asmqual)) :rule-classes :rewrite)