Map a token that is a function specifier to the corresponding function specifier.
Function:
(defun token-to-function-specifier (token) (declare (xargs :guard (tokenp token))) (declare (xargs :guard (token-function-specifier-p token))) (let ((__function__ 'token-to-function-specifier)) (declare (ignorable __function__)) (cond ((token-keywordp token "inline") (fun-spec-inline (keyword-uscores-none))) ((token-keywordp token "__inline") (fun-spec-inline (keyword-uscores-start))) ((token-keywordp token "__inline__") (fun-spec-inline (keyword-uscores-both))) ((token-keywordp token "_Noreturn") (fun-spec-noreturn)) (t (prog2$ (impossible) (irr-fun-spec))))))
Theorem:
(defthm fun-specp-of-token-to-function-specifier (b* ((funspec (token-to-function-specifier token))) (fun-specp funspec)) :rule-classes :rewrite)