Changeset 2262


Ignore:
Timestamp:
Jul 25, 2012, 5:54:59 PM (7 years ago)
Author:
mulligan
Message:

Changes from today.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2261 r2262  
    917917  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    918918  whd in match execute_1_preinstruction; normalize nodelta
    919   [(*1,2: (* ADD and ADDC *)
     919  [1,2: (* ADD and ADDC *)
    920920    (* XXX: work on the right hand side *)
    921921    (* XXX: switch to the left hand side *)
     
    989989          >status_refl
    990990          @(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 …)) % ] %
    992992        |3:
    993993          >status_refl
    994994          @(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 …)) % ] %
    996996        ]
    997997      |2:
     
    10031003          >status_refl
    10041004          @(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 …)) % ] %
    10061006        |3:
    10071007          >status_refl
    10081008          @(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 …)) % ] %
    10101010        ]
    10111011      |3:
     
    10311031          @I
    10321032        |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 %
    10351034          <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) %
    10361035        ]
     
    22512250    ]
    22522251  |*)43: (* POP *)
     2252    cases daemon
    22532253  |44:
    22542254    >EQP -P normalize nodelta
     
    24172417      ]
    24182418    ]
    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 *)
    24252422    >EQP -P normalize nodelta
    24262423    #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
     
    24322429    @set_clock_status_of_pseudo_status %
    24332430  ]
    2434 cases daemon
    24352431qed.
    24362432
Note: See TracChangeset for help on using the changeset viewer.