Changeset 2679


Ignore:
Timestamp:
Feb 19, 2013, 3:15:41 PM (6 years ago)
Author:
mckinna
Message:

Further tweak to Brian's changes: no normalization reqd at all!

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2676 r2679  
    635635    #classifier_assm
    636636    destruct @⊥
    637     try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    638     try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    639     cases (current_instruction ??) in classifier_assm; normalize #A #B try #C destruct
    640     cases A in B; normalize #D try #E try #F destruct
     637    change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     638    cases (current_instruction ??) in classifier_assm;
     639    [8:
     640      #preinstruction cases preinstruction
     641    ]
     642    try(#addr1 #addr2 #absurd destruct(absurd))
     643    try(#addr #absurd destruct(absurd))
     644    #absurd destruct(absurd)
    641645  |5:
    642646    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    652656  try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    653657  try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    654   (*
    655   try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
    656   try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    657   *)
    658658  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    659659  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
Note: See TracChangeset for help on using the changeset viewer.