[WIP: Coq compilation broken] Stub for Asmgen

1 files changed, 9 insertions, 5 deletions

diff --git a/aarch64/Asmblock.v b/aarch64/Asmblock.v
index 71c0dba3..d52f3c24 100644
--- a/aarch64/Asmblock.v
+++ b/aarch64/Asmblock.v
@@ -475,11 +475,6 @@ Inductive instruction: Type :=
   | Pcfi_adjust (ofs: int)                                            (**r .cfi_adjust debug directive *)
   | Pcfi_rel_offset (ofs: int)                                        (**r .cfi_rel_offset debug directive *)
 .
-
-Definition code := list instruction.
-Record function : Type := mkfunction { fn_sig: signature; fn_code: code }.
-Definition fundef := AST.fundef function.
-Definition program := AST.program fundef unit.
 *)
 
 
@@ -541,6 +536,15 @@ Fixpoint set_res (res: builtin_res preg) (v: val) (rs: regset) : regset :=
   | BR_splitlong hi lo => set_res lo (Val.loword v) (set_res hi (Val.hiword v) rs)
   end.
 
+
+(** FIXME: not clear howto deal with these axioms in Asmblock.
+    The dependency over genv will get us in troubles...
+
+TODO: The solution is probably to put [symbol_low] and [symbol_high] [symbol_high_low]  with any dependency on "ge"
+as an hypothesis in RELSEM section.
+
+*)
+
 (** The two functions below axiomatize how the linker processes
   symbolic references [symbol + offset].  It computes the
   difference between the address and the PC, and splits it into: