Rules related to C identifiers.
During symbolic execution,
C identifiers in the computation state
have the canonical form
In the course of symbolic execution,
terms appears of the form
Theorem:
(defthm equal-of-ident-and-const (implies (and (syntaxp (and (quotep x) (quotep c))) (identp c)) (equal (equal (ident x) c) (equal (str-fix x) (ident->name c)))))
Theorem:
(defthm equal-of-const-and-ident (implies (and (syntaxp (and (quotep x) (quotep c))) (identp c)) (equal (equal c (ident x)) (equal (str-fix x) (ident->name c)))))
Theorem:
(defthm equal-of-ident-and-ident (equal (equal (ident x) (ident y)) (equal (str-fix x) (str-fix y))))
Theorem:
(defthm <<-of-ident-and-ident (equal (<< (ident x) (ident y)) (<< (str-fix x) (str-fix y))))
Theorem:
(defthm exec-fun-of-const-identifier (implies (and (syntaxp (quotep fun)) (identp fun)) (equal (exec-fun fun args compst fenv limit) (exec-fun (ident (ident->name fun)) args compst fenv limit))))
Theorem:
(defthm read-static-var-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (read-static-var var compst) (read-static-var (ident (ident->name var)) compst))))
Theorem:
(defthm create-var-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (create-var var val compst) (create-var (ident (ident->name var)) val compst))))
Theorem:
(defthm read-var-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (read-var var compst) (read-var (ident (ident->name var)) compst))))
Theorem:
(defthm write-var-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (write-var var val compst) (write-var (ident (ident->name var)) val compst))))
Theorem:
(defthm write-static-var-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (write-static-var var val compst) (write-static-var (ident (ident->name var)) val compst))))
Theorem:
(defthm type-struct-of-const-identifier (implies (and (syntaxp (quotep tag)) (identp tag)) (equal (type-struct tag) (type-struct (ident (ident->name tag))))))
Theorem:
(defthm exec-member-of-const-identifier (implies (and (syntaxp (quotep mem)) (identp mem)) (equal (exec-member val mem) (exec-member val (ident (ident->name mem))))))
Theorem:
(defthm exec-memberp-of-const-identifier (implies (and (syntaxp (quotep mem)) (identp mem)) (equal (exec-memberp val mem compst) (exec-memberp val (ident (ident->name mem)) compst))))
Theorem:
(defthm exec-arrsub-of-member-of-const-identifier (implies (and (syntaxp (quotep mem)) (identp mem)) (equal (exec-arrsub-of-member str mem sub compst) (exec-arrsub-of-member str (ident (ident->name mem)) sub compst))))
Theorem:
(defthm exec-arrsub-of-memberp-of-const-identifier (implies (and (syntaxp (quotep mem)) (identp mem)) (equal (exec-arrsub-of-memberp str mem sub compst) (exec-arrsub-of-memberp str (ident (ident->name mem)) sub compst))))
Theorem:
(defthm objdesign-of-var-of-const-identifier (implies (and (syntaxp (quotep var)) (identp var)) (equal (objdesign-of-var var compst) (objdesign-of-var (ident (ident->name var)) compst))))