Imported Upstream version 0.2

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

diff --git a/extracted/abstractStatus.ml b/extracted/abstractStatus.ml
index 61faf8d75c99295b93ba4ed379a96bf4b382d402..bc6bf1c0970960c06cf9556e38c063c922bd4764 100644 (file)
--- a/extracted/abstractStatus.ml
+++ b/extracted/abstractStatus.ml
@@ -160,22 +160,15 @@ let aSM_classify0 = function
 | ASM.MOVC (x, x0) -> StructuredTraces.Cl_other
 | ASM.RealInstruction pre -> aSM_classify00 pre
 
-(** val current_instruction0 :
-    BitVector.byte BitVectorTrie.bitVectorTrie -> BitVector.word ->
-    ASM.instruction **)
-let current_instruction0 code_memory program_counter =
-  (Fetch.fetch code_memory program_counter).Types.fst.Types.fst
-
 (** val current_instruction :
     BitVector.byte BitVectorTrie.bitVectorTrie -> Status.status ->
     ASM.instruction **)
 let current_instruction code_memory s =
-  current_instruction0 code_memory s.Status.program_counter
+  (Fetch.fetch code_memory s.Status.program_counter).Types.fst.Types.fst
 
 (** val current_instruction_label :
-    BitVector.byte BitVectorTrie.bitVectorTrie -> CostLabel.costlabel
-    BitVectorTrie.bitVectorTrie -> Status.status -> CostLabel.costlabel
-    Types.option **)
+    BitVector.byte BitVectorTrie.bitVectorTrie -> ASM.costlabel_map ->
+    Status.status -> CostLabel.costlabel Types.option **)
 let current_instruction_label code_memory cost_labels s =
   let pc = s.Status.program_counter in
   BitVectorTrie.lookup_opt (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S (Nat.S