		Search-engine friendly clone of the ACL2 documentation.

Input-files-implementation

Input-files-preprocess-arg-std

Return the -std= flag reflecting the implementation environment.

Signature
(input-files-preprocess-arg-std ienv) → preprocess-arg
Arguments: ienv — Guard (ienvp ienv).
Returns: preprocess-arg — Type (stringp preprocess-arg).

Definitions and Theorems

Function: input-files-preprocess-arg-std

(defun input-files-preprocess-arg-std (ienv)
  (declare (xargs :guard (ienvp ienv)))
  (let ((__function__ 'input-files-preprocess-arg-std))
    (declare (ignorable __function__))
    (b* (((ienv ienv) ienv))
      (c::version-case ienv.version
                       :c17 "-std=c17"
                       :c23 "-std=c23"
                       :c17+gcc "-std=gnu17"
                       :c23+gcc "-std=gnu23"))))

Theorem: stringp-of-input-files-preprocess-arg-std

(defthm stringp-of-input-files-preprocess-arg-std
  (b* ((preprocess-arg (input-files-preprocess-arg-std ienv)))
    (stringp preprocess-arg))
  :rule-classes :rewrite)