		Search-engine friendly clone of the ACL2 documentation.

Validator

Valid-sizeof/alignof

Validate a sizeof operator applied to a type name, or an alignof operator, given the type denoted by the argument type name.

Signature
(valid-sizeof/alignof expr type) → (mv erp type1)
Arguments: expr — Guard (exprp expr).; type — Guard (typep type).
Returns: erp — Type (maybe-msgp erp).; type1 — Type (typep type1).

The sizeof operator applied to an type name requires a non-function complete type [C17:6.5.3.4/1]. In our current approximate type system, we just exclude function types, but we do not have a notion of complete types yet. The result has type size_t [C17:6.5.3.4/5], whose definition is implementation-defined, so for now we just return the unknown type; we will need to extend implementation environments with information about the definition of size_t.

Definitions and Theorems

Function: valid-sizeof/alignof

(defun valid-sizeof/alignof (expr type)
 (declare (xargs :guard (and (exprp expr) (typep type))))
 (declare (xargs :guard (or (expr-case expr :sizeof)
                            (expr-case expr :alignof))))
 (b*
  (((reterr) (irr-type))
   ((when (type-case type :function))
    (retmsg$
     "In the ~s0 type expression ~x1, ~
                  the argument ~x2 is a function type."
     (case (expr-kind expr)
       (:sizeof "sizeof")
       (:alignof "_Alignof")
       (t (impossible)))
     (expr-fix expr)
     (type-fix type))))
  (retok (type-unknown))))

Theorem: maybe-msgp-of-valid-sizeof/alignof.erp

(defthm maybe-msgp-of-valid-sizeof/alignof.erp
  (b* (((mv acl2::?erp ?type1)
        (valid-sizeof/alignof expr type)))
    (maybe-msgp erp))
  :rule-classes :rewrite)

Theorem: typep-of-valid-sizeof/alignof.type1

(defthm typep-of-valid-sizeof/alignof.type1
  (b* (((mv acl2::?erp ?type1)
        (valid-sizeof/alignof expr type)))
    (typep type1))
  :rule-classes :rewrite)

Theorem: valid-sizeof/alignof-of-expr-fix-expr

(defthm valid-sizeof/alignof-of-expr-fix-expr
  (equal (valid-sizeof/alignof (expr-fix expr)
                               type)
         (valid-sizeof/alignof expr type)))

Theorem: valid-sizeof/alignof-expr-equiv-congruence-on-expr

(defthm valid-sizeof/alignof-expr-equiv-congruence-on-expr
  (implies (expr-equiv expr expr-equiv)
           (equal (valid-sizeof/alignof expr type)
                  (valid-sizeof/alignof expr-equiv type)))
  :rule-classes :congruence)

Theorem: valid-sizeof/alignof-of-type-fix-type

(defthm valid-sizeof/alignof-of-type-fix-type
  (equal (valid-sizeof/alignof expr (type-fix type))
         (valid-sizeof/alignof expr type)))

Theorem: valid-sizeof/alignof-type-equiv-congruence-on-type

(defthm valid-sizeof/alignof-type-equiv-congruence-on-type
  (implies (type-equiv type type-equiv)
           (equal (valid-sizeof/alignof expr type)
                  (valid-sizeof/alignof expr type-equiv)))
  :rule-classes :congruence)