Generate a C expression from an ACL2 variable.
(atc-gen-expr-var var gin state) → gout
An ACL2 variable is translated to a C variable. Its information is looked up in the symbol table.
If the variable has pointer or array type and is not an external object,
its correctness theorem equates it to the
Function:
(defun atc-gen-expr-var (var gin state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (symbolp var) (expr-ginp gin)))) (let ((__function__ 'atc-gen-expr-var)) (declare (ignorable __function__)) (b* (((expr-gin gin) gin) (info (atc-get-var var gin.inscope)) ((when (not info)) (raise "Internal error: the variable ~x0 in function ~x1 ~ has no associated information." var gin.fn) (irr-expr-gout)) (type (atc-var-info->type info)) (var-thm (atc-var-info->thm info)) (expr (expr-ident (make-ident :name (symbol-name var)))) ((when (not gin.proofs)) (make-expr-gout :expr expr :type type :term var :events nil :thm-name nil :thm-index gin.thm-index :names-to-avoid gin.names-to-avoid)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons var-thm '(exec-expr-pure-when-ident (:e expr-kind) (:e expr-ident->get) exec-ident-open-via-object (:e identp) (:e ident->name) objdesign-of-var-of-const-identifier)) 'nil)) 'nil))) 'nil)) (objdes (cons 'objdesign-of-var (cons (cons 'ident (cons (cons 'quote (cons (symbol-name var) 'nil)) 'nil)) (cons gin.compst-var 'nil)))) ((mv thm-event thm-name thm-index names-to-avoid) (atc-gen-expr-pure-correct-thm gin.fn gin.fn-guard gin.context expr type (if (and (or (type-case type :pointer) (type-case type :array)) (not (atc-var-info->externalp info))) (add-suffix-to-fn var "-PTR") var) var objdes gin.compst-var hints nil gin.prec-tags gin.thm-index gin.names-to-avoid state))) (make-expr-gout :expr expr :type type :term var :events (list thm-event) :thm-name thm-name :thm-index thm-index :names-to-avoid names-to-avoid))))
Theorem:
(defthm expr-goutp-of-atc-gen-expr-var (b* ((gout (atc-gen-expr-var var gin state))) (expr-goutp gout)) :rule-classes :rewrite)