Merge tag 'upstream/0.2'

[pkg-cerco/acc-trusted.git] / extracted / policy.ml

diff --git a/extracted/policy.ml b/extracted/policy.ml
index 194fc73ffd6b740df40272e74998a7a340c79b47..e13f645185838e571aae30106e4425e0b59cbc32 100644 (file)
--- a/extracted/policy.ml
+++ b/extracted/policy.ml
@@ -94,7 +94,7 @@ open PolicyStep
 let rec jump_expansion_internal program n =
   let labels = PolicyFront.create_label_map (Types.pi1 program) in
   let rec aux res =
-prerr_endline "JEI_start";
+prerr_endline "JEI";
    let { Types.fst = no_ch; Types.snd = z } = res in
     match z with
      | Types.None ->
@@ -108,10 +108,11 @@ prerr_endline "JEI_start";
              (PolicyStep.jump_expansion_step program (Types.pi1 labels)
                op))
   in
+prerr_endline "JES";
+let init =(PolicyFront.jump_expansion_start program (Types.pi1 labels)) in
    aux
     { Types.fst = Bool.False; Types.snd =
-       (Types.pi1
-         (PolicyFront.jump_expansion_start program (Types.pi1 labels))) }
+       (Types.pi1 init) }
 (*
   (match n with
    | Nat.O ->
@@ -180,6 +181,7 @@ let jump_expansion' program =
            (Nat.S Nat.O)))))))))))))))) ppc x.Types.snd { Types.fst = Nat.O;
            Types.snd = Assembly.Short_jump }).Types.fst
        in
+(*prerr_endline "Z3";*)
        Arithmetic.bitvector_of_nat (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S
          (Nat.S Nat.O)))))))))))))))) pc); Types.snd = (fun ppc ->