Changeset 2056


Ignore:
Timestamp:
Jun 13, 2012, 1:01:05 PM (5 years ago)
Author:
sacerdot
Message:

Repaired, ported to new fetch_pseudo_assembly.
The execute_n is commented out because it only exists in partial form
(see the comment in the code).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2051 r2056  
    12211221qed.
    12221222
    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
     1223definition 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
    12261230  let ticks ≝ ticks_of (program_counter … s) in
    12271231   execute_1_pseudo_instruction0 ticks cm s instr pc.
     
    12331237    ].
    12341238
     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.
    12351243let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
    12361244  match n with
     
    12381246    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
    12391247    ].
     1248*)
Note: See TracChangeset for help on using the changeset viewer.