		Search-engine friendly clone of the ACL2 documentation.

Tshell

Tshell-call-fn1

Logical story for tshell-call.

We use the :partial-theory feature of define-trusted-clause-processor to introduce a function, tshell-call-fn1, about which we assume nothing.

BOZO this probably isn't sound. Don't we get the equality axioms for tshell-call-fn1? But those aren't necessarily satisfied by command-line programs. We should probably be using oracle reads instead, but then we'll need to involve state.

Definitions and Theorems

Theorem: return-type-of-tshell-call-fn1

(defthm return-type-of-tshell-call-fn1
        (b* (((mv status lines)
              (tshell-call-fn1 cmd print save)))
            (and (natp status)
                 (string-listp lines))))