Changeset 3002

Timestamp:

Mar 28, 2013, 1:05:20 PM (5 years ago)

Author:

tranquil

Message:

fixed previous commit

Files:

• driver/printer.ml (modified) (1 diff)
• extracted/untrusted/glue.ml (modified) (2 diffs)
• extracted/untrusted/glue.mli (modified) (2 diffs)

driver/printer.ml

@@ -254 +254 @@
    | Extracted.Compiler.Rtl_separate_pass ->
       beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params)
-   | Extracted.Compiler.Rtl_separate_pass ->
-      beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params)
    | Extracted.Compiler.Rtl_uniq_pass ->
       beprint (Extracted.RTL_printer.print_RTL_program rTL_printing_params)

extracted/untrusted/glue.ml

@@ -17 +17 @@
  | Positive.P1 v -> int_of_matitapos v * 2 + 1
 
+let int_of_matitaZ =
+ function
+   Z.OZ -> 0
+ | Z.Pos p -> int_of_matitapos p
+ | Z.Neg p -> -(int_of_matitapos p)
+
 let option_of_matitaoption =
  function
@@ -31 +37 @@
     Nat.O -> 0
   | Nat.S n -> int_of_matitanat n + 1
+
+let int_pair_of_pointer { Pointers.pblock = bl ; Pointers.poff = off } =
+  (int_of_matitaZ bl, int_of_bitvector off)

extracted/untrusted/glue.mli

@@ -2 +2 @@
 
 val int_of_matitapos : Positive.pos -> int
+
+val int_of_matitaZ : Z.z -> int
 
 val option_of_matitaoption: 'a Types.option -> 'a option
@@ -8 +10 @@
 
 val int_of_matitanat : Nat.nat -> int
+
+val int_pair_of_pointer : Pointers.pointer -> int * int