Access the |EXLD|::|SHNDX| field of a elf32_sym bit structure.
(elf32_sym->shndx x) → shndx
Function:
(defun elf32_sym->shndx (x) (declare (xargs :guard (elf32_sym-p x))) (mbe :logic (let ((x (elf32_sym-fix x))) (part-select x :low 112 :width 16)) :exec (the (unsigned-byte 16) (logand (the (unsigned-byte 16) 65535) (the (unsigned-byte 16) (ash (the (unsigned-byte 128) x) -112))))))
Theorem:
(defthm elf_bits16-p-of-elf32_sym->shndx (b* ((shndx (elf32_sym->shndx x))) (elf_bits16-p shndx)) :rule-classes :rewrite)
Theorem:
(defthm elf32_sym->shndx-of-elf32_sym-fix-x (equal (elf32_sym->shndx (elf32_sym-fix x)) (elf32_sym->shndx x)))
Theorem:
(defthm elf32_sym->shndx-elf32_sym-equiv-congruence-on-x (implies (elf32_sym-equiv x x-equiv) (equal (elf32_sym->shndx x) (elf32_sym->shndx x-equiv))) :rule-classes :congruence)
Theorem:
(defthm elf32_sym->shndx-of-elf32_sym (equal (elf32_sym->shndx (elf32_sym name value size info other shndx)) (elf_bits16-fix shndx)))
Theorem:
(defthm elf32_sym->shndx-of-write-with-mask (implies (and (fty::bitstruct-read-over-write-hyps x elf32_sym-equiv-under-mask) (elf32_sym-equiv-under-mask x y fty::mask) (equal (logand (lognot fty::mask) 340277174624079928635746076935438991360) 0)) (equal (elf32_sym->shndx x) (elf32_sym->shndx y))))