		Search-engine friendly clone of the ACL2 documentation.

Implementation-environments

Ienv-simple

Simplified constructor of implementation environments.

Signature
(ienv-simple short-bytes int-bytes long-bytes llong-bytes plain-chars-signed gcc) → ienv
Arguments: short-bytes — Guard (posp short-bytes).; int-bytes — Guard (posp int-bytes).; long-bytes — Guard (posp long-bytes).; llong-bytes — Guard (posp llong-bytes).; plain-chars-signed — Guard (booleanp plain-chars-signed).; gcc — Guard (booleanp gcc).
Returns: ienv — Type (ienvp ienv).

As explained in implementation-environments, this only depends on the applicable inputs of input-files: see that documentation.

We set the rest of the implementation environment parameters as follows:

Characters (i.e. bytes) are 8 bits.
Signed integers are two's complement.
There are no padding bits.
There are no trap representations.

Definitions and Theorems

Function: ienv-simple

(defun ienv-simple (short-bytes int-bytes long-bytes
                                llong-bytes plain-chars-signed gcc)
 (declare (xargs :guard (and (posp short-bytes)
                             (posp int-bytes)
                             (posp long-bytes)
                             (posp llong-bytes)
                             (booleanp plain-chars-signed)
                             (booleanp gcc))))
 (declare (xargs :guard (and (>= short-bytes 2)
                             (>= int-bytes 2)
                             (>= long-bytes 4)
                             (>= llong-bytes 8)
                             (<= short-bytes int-bytes)
                             (<= int-bytes long-bytes)
                             (<= long-bytes llong-bytes))))
 (let ((__function__ 'ienv-simple))
  (declare (ignorable __function__))
  (b*
   ((uchar-format (c::uchar-format-8))
    (schar-format (c::schar-format-8tcnt))
    (char-format (c::char-format plain-chars-signed))
    (short-format
         (c::integer-format-inc-sign-tcnpnt (* 8 short-bytes)))
    (int-format (c::integer-format-inc-sign-tcnpnt (* 8 int-bytes)))
    (long-format
         (c::integer-format-inc-sign-tcnpnt (* 8 long-bytes)))
    (llong-format
         (c::integer-format-inc-sign-tcnpnt (* 8 llong-bytes)))
    (char+short+int+long+llong-format
         (c::char+short+int+long+llong-format
              uchar-format
              schar-format char-format short-format
              int-format long-format llong-format)))
   (c::make-ienv :char+short+int+long+llong-format
                 char+short+int+long+llong-format
                 :gcc gcc))))

Theorem: ienvp-of-ienv-simple

(defthm ienvp-of-ienv-simple
  (b* ((ienv (ienv-simple short-bytes int-bytes long-bytes
                          llong-bytes plain-chars-signed gcc)))
    (ienvp ienv))
  :rule-classes :rewrite)