Changeset 1539 for Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

Timestamp:

Nov 23, 2011, 1:55:12 PM (9 years ago)

Author:

tranquil

Message:

branch up to date

File:

• Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml (modified) (8 diffs)

Deliverables/D2.2/8051-indexed-labels-branch/src/LTL/LTLInterpret.ml

@@ -31 +31 @@
       renv   : hdw_reg_env ;
       mem    : memory ;
-                        inds   : CostLabel.const_indexing list ;
+      inds   : CostLabel.const_indexing list ;
       trace  : CostLabel.t list }
 
@@ -58 +58 @@
     renv   = I8051.RegisterMap.empty ;
     mem    = Mem.empty ;
-                inds   = [] ;
+    inds   = [] ;
     trace  = [] }
 
@@ -102 +102 @@
 let init_fun_call lbls_offs st ptr def =
   let pc = entry_pc lbls_offs ptr def in
-        let st = new_ind st in
+  let st = new_ind st in
   change_pc st pc
 
@@ -204 +204 @@
   change_pc st next_pc
 
-let interpret_call lbls_offs st f ra =
-  let ptr = Mem.find_global st.mem f in
+let interpret_call lbls_offs st ptr ra =
   match Mem.find_fun_def st.mem ptr with
     | LTL.F_int def ->
@@ -216 +215 @@
 
 let interpret_return lbls_offs st =
-        let st = forget_ind st in
+  let st = forget_ind st in
   let (st, pc) = return_pc st in
   change_pc st pc
@@ -237 +236 @@
 
     | LTL.St_cost (cost_lbl, lbl) ->
-                        let cost_lbl = ev_label st cost_lbl in
+      let cost_lbl = ev_label st cost_lbl in
       let st = add_trace st cost_lbl in
       next_pc st lbl
 
     | LTL.St_ind_0 (i, lbl) ->
-            enter_loop st i;
-            next_pc st lbl
+      enter_loop st i;
+      next_pc st lbl
 
     | LTL.St_ind_inc (i, lbl) ->
@@ -249 +248 @@
       next_pc st lbl
 
-                | LTL.St_int (r, i, lbl) ->
+    | LTL.St_int (r, i, lbl) ->
       let st = add_reg r (Val.of_int i) st in
       next_pc st lbl
@@ -321 +320 @@
 
     | LTL.St_call_id (f, lbl) ->
-      interpret_call lbls_offs st f lbl
+      interpret_call lbls_offs st (Mem.find_global st.mem f) lbl
+
+    | LTL.St_call_ptr lbl ->
+      interpret_call lbls_offs st (dptr st) lbl
 
     | LTL.St_condacc (lbl_true, lbl_false) ->