 Timestamp:
 Jun 13, 2012, 1:01:05 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r2051 r2056 1221 1221 qed. 1222 1222 1223 definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝ 1224 λticks_of,cm,s. 1225 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in 1223 definition execute_1_pseudo_instruction: 1224 (Word → nat × nat) → ∀cm. ∀s:PseudoStatus cm. 1225 nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <\snd cm → 1226 PseudoStatus cm 1227 ≝ 1228 λticks_of,cm,s,pc_ok. 1229 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in 1226 1230 let ticks ≝ ticks_of (program_counter … s) in 1227 1231 execute_1_pseudo_instruction0 ticks cm s instr pc. … … 1233 1237 ]. 1234 1238 1239 (* CSC: No way to have a total function because of function pointers call! 1240 The new pc after the execution can fall outside the program length. 1241 Luckily, this function is never actually used because we are only 1242 interested in structured traces. 1235 1243 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝ 1236 1244 match n with … … 1238 1246  S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s) 1239 1247 ]. 1248 *)
Note: See TracChangeset
for help on using the changeset viewer.