Changeset 2679
- Timestamp:
- Feb 19, 2013, 3:15:41 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCosts.ma
r2676 r2679 635 635 #classifier_assm 636 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 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) 641 645 |5: 642 646 #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call … … 652 656 try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;) 653 657 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 *)658 658 whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm; 659 659 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
Note: See TracChangeset
for help on using the changeset viewer.