Changeset 3105


Ignore:
Timestamp:
Apr 6, 2013, 6:38:22 PM (4 years ago)
Author:
sacerdot
Message:

Pretty printing changed.
There is still an inefficiency left: activate the commented out prerr_endline
to understand it.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • driver/extracted/policy.ml

    r3001 r3105  
    9595  let labels = PolicyFront.create_label_map (Types.pi1 program) in
    9696  let rec aux res =
    97 prerr_endline "JEI_start";
     97prerr_endline "JEI";
    9898   let { Types.fst = no_ch; Types.snd = z } = res in
    9999    match z with
     
    109109               op))
    110110  in
     111prerr_endline "JES";
     112let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in
    111113   aux
    112114    { Types.fst = Bool.False; Types.snd =
    113        (Types.pi1
    114          (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
     115       (Types.pi1 init) }
    115116(*
    116117  (match n with
     
    181182           Types.snd = Assembly.Short_jump }).Types.fst
    182183       in
     184(*prerr_endline "Z3";*)
    183185       Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
    184186         (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
Note: See TracChangeset for help on using the changeset viewer.