From d0257b0a47ad998e01715e9bc6ba612b834765f1 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Thu, 11 Jun 2020 14:47:52 +0100
Subject: Working on proof.

---
 src/translation/HTLgen.v | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'src/translation/HTLgen.v')

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index b573b06..d5a8af2 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -398,9 +398,9 @@ Lemma create_arr_state_incr:
          (st_controllogic s)).
 Proof. constructor; simpl; auto with htlh. Qed.
 
-Definition create_arr (sz : nat) (ln : nat) : mon reg :=
+Definition create_arr (sz : nat) (ln : nat) : mon (reg * nat) :=
   fun s => let r := s.(st_freshreg) in
-           OK r (mkstate
+           OK (r, ln) (mkstate
                    s.(st_st)
                    (Pos.succ r)
                    (st_freshstate s)
@@ -413,7 +413,7 @@ Definition create_arr (sz : nat) (ln : nat) : mon reg :=
 Definition transf_module (f: function) : mon module :=
   do fin <- create_reg 1;
   do rtrn <- create_reg 32;
-  do stack <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
+  do (stack, stack_len) <- create_arr 32 (Z.to_nat (f.(fn_stacksize) / 4));
   do _ <- collectlist (transf_instr fin rtrn stack) (Maps.PTree.elements f.(RTL.fn_code));
   do start <- create_reg 1;
   do rst <- create_reg 1;
@@ -426,6 +426,7 @@ Definition transf_module (f: function) : mon module :=
          f.(fn_entrypoint)
          current_state.(st_st)
          stack
+         stack_len
          fin
          rtrn).
 
-- 
cgit