Generate a term representing the result value and a term representing the ending computation state of the execution of a C function call.
(atc-gen-call-result-and-endstate type affect inscope compst-var call) → (mv result new-compst)
If no variables are affected,
the computation state is unchanged,
and the call is the result.
(In this case the type is not
Otherwise, if exactly one variable is affected,
and additionally the function is
Otherwise, there are two cases.
If the function is
Function:
(defun atc-gen-call-endstate (affect inscope compst-var call index) (declare (xargs :guard (and (symbol-listp affect) (atc-symbol-varinfo-alist-listp inscope) (symbolp compst-var) (natp index)))) (let ((__function__ 'atc-gen-call-endstate)) (declare (ignorable __function__)) (b* (((when (endp affect)) compst-var) (var (car affect)) (info (atc-get-var var inscope)) ((when (not info)) (raise "Internal error: variable ~x0 not found." var)) (type (atc-var-info->type info)) ((unless (or (type-case type :pointer) (type-case type :array) (atc-var-info->externalp info))) (raise "Internal error: affected variable ~x0 ~ has type ~x1 and is not an external object." var type))) (if (atc-var-info->externalp info) (cons 'update-static-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons (cons 'mv-nth (cons index (cons call 'nil))) (cons (atc-gen-call-endstate (cdr affect) inscope compst-var call (1+ index)) 'nil)))) (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons (cons 'mv-nth (cons index (cons call 'nil))) (cons (atc-gen-call-endstate (cdr affect) inscope compst-var call (1+ index)) 'nil))))))))
Function:
(defun atc-gen-call-result-and-endstate (type affect inscope compst-var call) (declare (xargs :guard (and (typep type) (symbol-listp affect) (atc-symbol-varinfo-alist-listp inscope) (symbolp compst-var)))) (let ((__function__ 'atc-gen-call-result-and-endstate)) (declare (ignorable __function__)) (b* (((when (endp affect)) (mv call compst-var)) ((when (and (endp (cdr affect)) (type-case type :void))) (b* ((var (car affect)) (info (atc-get-var var inscope)) ((when (not info)) (raise "Internal error: variable ~x0 not found." var) (mv nil nil)) (type (atc-var-info->type info)) ((unless (or (type-case type :pointer) (type-case type :array) (atc-var-info->externalp info))) (raise "Internal error: affected variable ~x0 ~ has type ~x1 and is not an external object." var type) (mv nil nil)) (new-compst (if (atc-var-info->externalp info) (cons 'update-static-var (cons (cons 'ident (cons (symbol-name var) 'nil)) (cons call (cons compst-var 'nil)))) (cons 'update-object (cons (add-suffix-to-fn var "-OBJDES") (cons call (cons compst-var 'nil))))))) (mv nil new-compst)))) (if (type-case type :void) (mv nil (atc-gen-call-endstate affect inscope compst-var call 0)) (mv (cons 'mv-nth (cons '0 (cons call 'nil))) (atc-gen-call-endstate affect inscope compst-var call 1))))))