Changeset 2760 for src/ASM/ASMCosts.ma


Ignore:
Timestamp:
Mar 2, 2013, 1:29:41 AM (7 years ago)
Author:
sacerdot
Message:
  1. Many files repaired.
  2. 3 new daemons: 2 in Assembly.ma, 1 in StructuredTraces?.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCosts.ma

    r2756 r2760  
    1414    mk_abstract_status
    1515      (Status code_memory)
    16       (λs. return (execute_1 … s))
    17       ?
     16      (λs1,s2. execute_1 … s1 = s2)
    1817      word_deqset
    1918      (program_counter …)
     
    391390      ]
    392391    ]
    393   change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     392  change with (ASM_classify0 ? = ?) in classifier_assm;
    394393  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    395394  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    450449    #final_status_refl #the_trace_refl destruct @⊥
    451450  ]
    452   change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     451  change with (ASM_classify0 ? = ?) in classifier_assm;
    453452  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    454453  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    587586    ]
    588587  ]
    589   try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    590   try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     588  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     589  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    591590  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    592591  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
     
    636635    #classifier_assm
    637636    destruct @⊥
    638     change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;
     637    change with (ASM_classify0 ? = ?) in classifier_assm;
    639638    cases (current_instruction ??) in classifier_assm;
    640639    [7: #preinstruction cases preinstruction ]
    641     try(#addr1 #addr2 #absurd destruct(absurd))
    642     try(#addr #absurd destruct(absurd))
    643     #absurd destruct(absurd)
     640    try(#addr1 #addr2 #absurd normalize in absurd; destruct(absurd))
     641    try(#addr #absurd normalize in absurd; destruct(absurd))
     642    #absurd normalize in absurd; destruct(absurd)
    644643  |5:
    645644    #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     
    653652    #final_status_refl #the_trace_refl destruct @⊥
    654653  ]
    655   try (change with (Some ? (ASM_classify0 ?) = ? ∨ Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
    656   try (change with (Some ? (ASM_classify0 ?) = ?) in classifier_assm;)
     654  try (change with (ASM_classify0 ? = ? ∨ ASM_classify0 ? = ?) in classifier_assm;)
     655  try (change with (ASM_classify0 ? = ?) in classifier_assm;)
    657656  whd in match current_instruction in classifier_assm; normalize nodelta in classifier_assm;
    658657  whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm;
Note: See TracChangeset for help on using the changeset viewer.