Changeset 2209 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jul 18, 2012, 2:56:12 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2197 r2209 473 473 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 474 474 | INDIRECT i ⇒ 475 let d ≝ get_register … s [[false;false;i]] in 476 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) 475 let d ≝ get_register … s [[false;false;i]] in 476 let address ≝ bit_address_of_register … s [[false;false;i]] in 477 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧ 478 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 477 479 | EXT_INDIRECT _ ⇒ true 478 480 | REGISTER r ⇒
Note: See TracChangeset
for help on using the changeset viewer.