Changeset 2653


Ignore:
Timestamp:
Feb 8, 2013, 1:45:22 PM (6 years ago)
Author:
sacerdot
Message:

...

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Policy.ma

    r2652 r2653  
    199199   | #Heq lapply (refl ? (jump_expansion_internal program (S (S n))))
    200200     whd in match (jump_expansion_internal program (S (S n))) in ⊢ (???% → ?); >Seq
    201      normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq; (*320s*)
     201     normalize nodelta #Teq >Teq -Teq cases (jump_expansion_step program ??) in Heq Seq ⊢ ?; (*320s*)
    202202     #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol
    203203     [ normalize nodelta #HSn #Heq #Seq cases Heq
  • src/ASM/PolicyFront.ma

    r2652 r2653  
    202202 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map.
    203203 ∀i.i < |prefix| →
    204  let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
     204 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in
    205205 ∀dest.is_jump_to instr dest →
    206206 let paddr ≝ lookup_def … labels dest 0 in
Note: See TracChangeset for help on using the changeset viewer.