Changeset 3105 for driver/extracted
 Timestamp:
 Apr 6, 2013, 6:38:22 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

driver/extracted/policy.ml
r3001 r3105 95 95 let labels = PolicyFront.create_label_map (Types.pi1 program) in 96 96 let rec aux res = 97 prerr_endline "JEI _start";97 prerr_endline "JEI"; 98 98 let { Types.fst = no_ch; Types.snd = z } = res in 99 99 match z with … … 109 109 op)) 110 110 in 111 prerr_endline "JES"; 112 let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in 111 113 aux 112 114 { Types.fst = Bool.False; Types.snd = 113 (Types.pi1 114 (PolicyFront.jump_expansion_start program (Types.pi1 labels))) } 115 (Types.pi1 init) } 115 116 (* 116 117 (match n with … … 181 182 Types.snd = Assembly.Short_jump }).Types.fst 182 183 in 184 (*prerr_endline "Z3";*) 183 185 Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S 184 186 (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.