Changeset 2056 for src

Timestamp:

Jun 13, 2012, 1:01:05 PM (8 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:

• src/ASM/Interpret.ma (modified) (3 diffs)

src/ASM/Interpret.ma

@@ -1221 +1221 @@
 qed.
 
-definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝
-  λticks_of,cm,s.
-  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in
+definition execute_1_pseudo_instruction:
+ (Word → nat × nat) → ∀cm. ∀s:PseudoStatus cm.
+   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
+    PseudoStatus cm
+≝
+  λticks_of,cm,s,pc_ok.
+  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
   let ticks ≝ ticks_of (program_counter … s) in
    execute_1_pseudo_instruction0 ticks cm s instr pc.
@@ -1233 +1237 @@
     ].
 
+(* CSC: No way to have a total function because of function pointers call!
+   The new pc after the execution can fall outside the program length.
+   Luckily, this function is never actually used because we are only
+   interested in structured traces.
 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
   match n with
@@ -1238 +1246 @@
     | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
     ].
+*)