		Search-engine friendly clone of the ACL2 documentation.

Compilation-database

Comp-db-escape-for-shell

Escape strings in arguments of a compilation-database for use in the shell.

Signature
(comp-db-escape-for-shell db) → db$
Arguments: db — Guard (comp-dbp db).
Returns: db$ — Type (comp-dbp db$).

Definitions and Theorems

Function: comp-db-escape-for-shell

(defun comp-db-escape-for-shell (db)
  (declare (xargs :guard (comp-dbp db)))
  (b*
   ((db (comp-db-fix db))
    ((when (endp db)) nil)
    (file (car (first db)))
    ((comp-db-entry entry) (cdr (first db)))
    (arguments (comp-db-arguments-escape-for-shell entry.arguments))
    (entry (change-comp-db-entry entry
                                 :arguments arguments)))
   (acons file entry
          (comp-db-escape-for-shell (rest db)))))

Theorem: comp-dbp-of-comp-db-escape-for-shell

(defthm comp-dbp-of-comp-db-escape-for-shell
  (b* ((db$ (comp-db-escape-for-shell db)))
    (comp-dbp db$))
  :rule-classes :rewrite)

Theorem: comp-db-escape-for-shell-of-comp-db-fix-db

(defthm comp-db-escape-for-shell-of-comp-db-fix-db
  (equal (comp-db-escape-for-shell (comp-db-fix db))
         (comp-db-escape-for-shell db)))

Theorem: comp-db-escape-for-shell-comp-db-equiv-congruence-on-db

(defthm comp-db-escape-for-shell-comp-db-equiv-congruence-on-db
  (implies (comp-db-equiv db db-equiv)
           (equal (comp-db-escape-for-shell db)
                  (comp-db-escape-for-shell db-equiv)))
  :rule-classes :congruence)