Changeset 2676


Ignore:
Timestamp:
Feb 19, 2013, 12:23:49 PM (6 years ago)
Author:
campbell
Message:

Less aggressive normalisation in ASMCosts to prevent memory blowup.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2672 r2676  
    634634    #status_pre_fun_call #status_start_fun_call #status_final #execute_assm
    635635    #classifier_assm
    636     @⊥ normalize in classifier_assm;
    637     cases (classify_instruction ?) in classifier_assm; normalize nodelta
    638     try (#_ #abs) try #abs destruct
     636    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
    639641  |5:
    640642    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
Note: See TracChangeset for help on using the changeset viewer.