• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
    • Kestrel-books
      • Crypto-hdwallet
      • Apt
      • Error-checking
      • Fty-extensions
      • Isar
      • Kestrel-utilities
      • Set
      • Soft
      • C
        • Syntax-for-tools
        • Atc
          • Atc-implementation
            • Atc-abstract-syntax
            • Atc-pretty-printer
            • Atc-event-and-code-generation
            • Fty-pseudo-term-utilities
            • Atc-term-recognizers
            • Atc-input-processing
              • Atc-process-target
              • Atc-process-const-name
              • Atc-process-function
              • Atc-process-target-list
              • Atc-process-inputs
              • Atc-process-file-name
              • Atc-process-const-name-aux
              • Atc-process-targets
              • Atc-process-print
              • Atc-process-pretty-printing
              • Atc-remove-called-fns
              • Atc-process-output-dir
              • Atc-process-proofs
              • Atc-process-header
              • *atc-allowed-pretty-printing-options*
              • *atc-allowed-options*
            • Atc-shallow-embedding
            • Atc-process-inputs-and-gen-everything
            • Atc-table
            • Atc-fn
            • Atc-pretty-printing-options
            • Atc-types
            • Atc-macro-definition
          • Atc-tutorial
        • Language
        • Representation
        • Transformation-tools
        • Insertion-sort
        • Pack
      • Bv
      • Imp-language
      • Event-macros
      • Java
      • Bitcoin
      • Ethereum
      • Yul
      • Zcash
      • ACL2-programming-language
      • Prime-fields
      • Json
      • Syntheto
      • File-io-light
      • Cryptography
      • Number-theory
      • Lists-light
      • Axe
      • Builtins
      • Solidity
      • Helpers
      • Htclient
      • Typed-lists-light
      • Arithmetic-light
    • X86isa
    • Axe
    • Execloader
  • Math
  • Testing-utilities

• Atc-input-processing

Atc-process-file-name

Process the :file-name input.

Signature

(atc-process-file-name options output-dir state) 
  → 
(mv erp file-name path-wo-ext state)

Arguments

options — Guard (symbol-alistp options).

output-dir — Guard (stringp output-dir).

Returns

file-name — Type (stringp file-name).

path-wo-ext — Type (stringp path-wo-ext).

If successful, return, besides the file name itself as a string, the full path of the file(s), without the .c or .h extension, consisting of the output directory and the file name without extension.

We make sure that, after adding each of the .h and .c extensions, either the file does not exist in the file system or is a file and not a directory (i.e. has the right kind).

Due to the use of the file utilities, we also need to return state.

Definitions and Theorems

Function: atc-process-file-name

(defun atc-process-file-name (options output-dir state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (symbol-alistp options)
                             (stringp output-dir))))
 (let ((__function__ 'atc-process-file-name))
  (declare (ignorable __function__))
  (b*
   (((reterr) "" "" state)
    (file-name-option (assoc-eq :file-name options))
    ((unless (consp file-name-option))
     (reterr
      (msg
       "The :FILE-NAME input must be present, ~
                      but it is absent instead.")))
    (file-name (cdr file-name-option))
    ((unless (stringp file-name))
     (reterr
      (msg
       "The :FILE-NAME input must be a string, ~
                      but ~x0 is not a string."
       file-name)))
    ((when (equal file-name ""))
     (reterr
        (msg "The :FILE-NAME input must not be the empty string.")))
    ((unless (str::letter/digit/uscore/dash-charlist-p
                  (acl2::explode file-name)))
     (reterr
      (msg
       "The :FILE-NAME input must consists of only ~
                      ASCII letters, digits, underscores, and dashes, ~
                      but ~s0 violates this condition."
       file-name)))
    (path-wo-ext (oslib::catpath output-dir file-name))
    (path.c (str::cat path-wo-ext ".c"))
    ((mv msg? existsp state)
     (oslib::path-exists-p path.c))
    ((when msg?)
     (reterr
      (msg
       "The existence of the file path ~x0 ~
                                  cannot be tested.  ~
                                  ~@1"
       path.c msg?)))
    ((when (not existsp))
     (retok file-name path-wo-ext state))
    ((mv msg? kind state)
     (oslib::file-kind path.c))
    ((when msg?)
     (reterr
      (msg
       "The kind of the file path ~x0 ~
                                  cannot be tested.  ~
                                  ~@1"
       path.c msg?)))
    ((unless (eq kind :regular-file))
     (reterr
      (msg
       "The file path ~x0 ~
                      is not a regular file; it has kind ~x1 instead."
       path.c kind))))
   (retok file-name path-wo-ext state))))

Theorem: stringp-of-atc-process-file-name.file-name

(defthm stringp-of-atc-process-file-name.file-name
  (b* (((mv acl2::?erp
            ?file-name ?path-wo-ext acl2::?state)
        (atc-process-file-name options output-dir state)))
    (stringp file-name))
  :rule-classes :rewrite)

Theorem: stringp-of-atc-process-file-name.path-wo-ext

(defthm stringp-of-atc-process-file-name.path-wo-ext
  (b* (((mv acl2::?erp
            ?file-name ?path-wo-ext acl2::?state)
        (atc-process-file-name options output-dir state)))
    (stringp path-wo-ext))
  :rule-classes :rewrite)