- Timestamp:
- Jul 25, 2012, 5:54:59 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2261 r2262 917 917 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 918 918 whd in match execute_1_preinstruction; normalize nodelta 919 [ (*1,2: (* ADD and ADDC *)919 [1,2: (* ADD and ADDC *) 920 920 (* XXX: work on the right hand side *) 921 921 (* XXX: switch to the left hand side *) … … 989 989 >status_refl 990 990 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) 991 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %991 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] % 992 992 |3: 993 993 >status_refl 994 994 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) 995 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %995 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] % 996 996 ] 997 997 |2: … … 1003 1003 >status_refl 1004 1004 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 1005 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %1005 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] % 1006 1006 |3: 1007 1007 >status_refl 1008 1008 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 1009 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %1009 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] % 1010 1010 ] 1011 1011 |3: … … 1031 1031 @I 1032 1032 |3: 1033 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) 1034 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try % 1033 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) try % 1035 1034 <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) % 1036 1035 ] … … 2251 2250 ] 2252 2251 |*)43: (* POP *) 2252 cases daemon 2253 2253 |44: 2254 2254 >EQP -P normalize nodelta … … 2417 2417 ] 2418 2418 ] 2419 |47: (* POP *) 2420 |48: (* XCH *) 2421 |49: (* XCHD *) 2422 |50: (* RET *) 2423 |51: (* RETI *) 2424 |52: (* NOP *) 2419 |47: (* RETI *) 2420 cases daemon 2421 |48: (* NOP *) 2425 2422 >EQP -P normalize nodelta 2426 2423 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 2432 2429 @set_clock_status_of_pseudo_status % 2433 2430 ] 2434 cases daemon2435 2431 qed. 2436 2432
Note: See TracChangeset
for help on using the changeset viewer.