Imported Upstream version 0.2

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

diff --git a/extracted/semantics.ml b/extracted/semantics.ml
index 221a22e2f8959b9cff698d4dbdf85ac301487220..c49e25f6045d968ca2ff091454a95d33f5fc00ab 100644 (file)
--- a/extracted/semantics.ml
+++ b/extracted/semantics.ml
@@ -14,12 +14,12 @@ open Interpret
 
 open ASMCosts
 
-open Assembly
-
 open Status
 
 open Fetch
 
+open Assembly
+
 open PolicyFront
 
 open PolicyStep
@@ -315,38 +315,38 @@ type preclassified_system_pass =
 (** val preclassified_system_pass_rect_Type4 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_25220 =
-  let pcs_pcs = x_25220 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type4 p h_mk_preclassified_system_pass x_3 =
+  let pcs_pcs = x_3 in h_mk_preclassified_system_pass pcs_pcs __
 
 (** val preclassified_system_pass_rect_Type5 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_25222 =
-  let pcs_pcs = x_25222 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type5 p h_mk_preclassified_system_pass x_5 =
+  let pcs_pcs = x_5 in h_mk_preclassified_system_pass pcs_pcs __
 
 (** val preclassified_system_pass_rect_Type3 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_25224 =
-  let pcs_pcs = x_25224 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type3 p h_mk_preclassified_system_pass x_7 =
+  let pcs_pcs = x_7 in h_mk_preclassified_system_pass pcs_pcs __
 
 (** val preclassified_system_pass_rect_Type2 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_25226 =
-  let pcs_pcs = x_25226 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type2 p h_mk_preclassified_system_pass x_9 =
+  let pcs_pcs = x_9 in h_mk_preclassified_system_pass pcs_pcs __
 
 (** val preclassified_system_pass_rect_Type1 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_25228 =
-  let pcs_pcs = x_25228 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type1 p h_mk_preclassified_system_pass x_11 =
+  let pcs_pcs = x_11 in h_mk_preclassified_system_pass pcs_pcs __
 
 (** val preclassified_system_pass_rect_Type0 :
     Compiler.pass -> (Measurable.preclassified_system -> __ -> 'a1) ->
     preclassified_system_pass -> 'a1 **)
-let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_25230 =
-  let pcs_pcs = x_25230 in h_mk_preclassified_system_pass pcs_pcs __
+let rec preclassified_system_pass_rect_Type0 p h_mk_preclassified_system_pass x_13 =
+  let pcs_pcs = x_13 in h_mk_preclassified_system_pass pcs_pcs __
 
 (** val pcs_pcs :
     Compiler.pass -> preclassified_system_pass ->
@@ -433,8 +433,8 @@ let preclassified_system_of_pass = function
     Joint_fullexec.joint_preclassified_system LIN_semantics.lIN_semantics)
 | Compiler.Assembly_pass ->
   (fun prog ->
-    let { Types.fst = eta32049; Types.snd = policy } = Obj.magic prog in
-    let { Types.fst = code; Types.snd = sigma } = eta32049 in
+    let { Types.fst = eta4; Types.snd = policy } = Obj.magic prog in
+    let { Types.fst = code; Types.snd = sigma } = eta4 in
     Interpret2.aSM_preclassified_system code sigma policy)
 | Compiler.Object_code_pass ->
   (fun prog -> Interpret2.oC_preclassified_system (Obj.magic prog))