diff options
| author | James Pollard <james@pollard.dev> | 2020-06-11 14:47:52 +0100 |
|---|---|---|
| committer | James Pollard <james@pollard.dev> | 2020-06-11 14:47:52 +0100 |
| commit | d0257b0a47ad998e01715e9bc6ba612b834765f1 (patch) | |
| tree | a356047d4cc1a0f6fb008d63512184d4075ee4e4 /src/translation/HTLgen.v | |
| parent | d3be4601c9bc68fddaf4dc08c648f03d95a39e1d (diff) | |
| download | vericert-d0257b0a47ad998e01715e9bc6ba612b834765f1.tar.gz vericert-d0257b0a47ad998e01715e9bc6ba612b834765f1.zip | |
Working on proof.
Diffstat (limited to 'src/translation/HTLgen.v')
| -rw-r--r-- | src/translation/HTLgen.v | 7 |
1 files changed, 4 insertions, 3 deletions
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). |