From 86f42b92d87020875e2a7ef4ba40de12d261685f Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Fri, 12 Jun 2020 14:40:15 +0100
Subject: Add declaration of loads

---
 src/translation/HTLgen.v | 1 +
 1 file changed, 1 insertion(+)

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

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index bbce47c..a891d6c 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -363,6 +363,7 @@ Definition transf_instr (fin rtrn stack: reg) (ni: node * instruction) : mon uni
       add_instr n n' (nonblock dst instr)
     | Iload mem addr args dst n' =>
       do src <- translate_arr_access mem addr args stack;
+      do _ <- declare_reg None dst 32;
       add_instr n n' (block dst src)
     | Istore mem addr args src n' =>
       do dst <- translate_arr_access mem addr args stack;
-- 
cgit