- Timestamp:
- Feb 8, 2013, 1:45:22 PM (7 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Policy.ma
r2652 r2653 199 199 | #Heq lapply (refl ? (jump_expansion_internal program (S (S n)))) 200 200 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*) 202 202 #x cases x -x #Sno_ch #Spol normalize nodelta cases Spol 203 203 [ normalize nodelta #HSn #Heq #Seq cases Heq -
src/ASM/PolicyFront.ma
r2652 r2653 202 202 λold_sigma:ppc_pc_map.λsigma:ppc_pc_map. 203 203 ∀i.i < |prefix| → 204 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in204 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in 205 205 ∀dest.is_jump_to instr dest → 206 206 let paddr ≝ lookup_def … labels dest 0 in
Note: See TracChangeset
for help on using the changeset viewer.