		Search-engine friendly clone of the ACL2 documentation.

Parse-yul-json

Solc-json-file-to-irs

Extracts Yul IR surface syntax strings from the file named by json-filename.

Signature
(solc-json-file-to-irs json-filename state) → (mv erp irs-pair state)
Arguments: json-filename — Guard (stringp json-filename).
Returns: erp — Type (booleanp erp).; irs-pair — Type (consp irs-pair).

Definitions and Theorems

Function: solc-json-file-to-irs

(defun solc-json-file-to-irs (json-filename state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp json-filename)))
  (let ((__function__ 'solc-json-file-to-irs))
    (declare (ignorable __function__))
    (b* (((mv erp j state)
          (acl2::parse-file-as-json json-filename state))
         ((when erp) (mv t '("" . "") state))
         ((mv erp tj) (json::parsed-to-value j))
         ((when erp) (mv t '("" . "") state))
         ((mv erp ir-pair) (json-to-irs tj))
         ((when (or erp (not (consp ir-pair))))
          (mv t '("" . "") state)))
      (mv nil ir-pair state))))

Theorem: booleanp-of-solc-json-file-to-irs.erp

(defthm booleanp-of-solc-json-file-to-irs.erp
  (b* (((mv ?erp ?irs-pair acl2::?state)
        (solc-json-file-to-irs json-filename state)))
    (booleanp erp))
  :rule-classes :rewrite)

Theorem: consp-of-solc-json-file-to-irs.irs-pair

(defthm consp-of-solc-json-file-to-irs.irs-pair
  (b* (((mv ?erp ?irs-pair acl2::?state)
        (solc-json-file-to-irs json-filename state)))
    (consp irs-pair))
  :rule-classes :rewrite)