From f136beaf95fda574f120619b0d6b2dba46072032 Mon Sep 17 00:00:00 2001
From: Cyril SIX <cyril.six@kalray.eu>
Date: Wed, 5 Dec 2018 16:34:49 +0100
Subject: Moving size_blocks from Asmblockgen to Asmblock

---
 mppa_k1c/Asmblock.v    | 8 ++++++++
 mppa_k1c/Asmblockgen.v | 9 ---------
 2 files changed, 8 insertions(+), 9 deletions(-)

(limited to 'mppa_k1c')

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 1040d4c0..912a02d5 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -492,6 +492,14 @@ Proof.
 
 Definition bblocks := list bblock.
 
+Fixpoint size_blocks (l: bblocks): Z :=
+  match l with
+  | nil => 0
+  | b :: l =>
+     (size b) + (size_blocks l)
+  end
+  .
+
 Record function : Type := mkfunction { fn_sig: signature; fn_blocks: bblocks }.
 Definition fundef := AST.fundef function.
 Definition program := AST.program fundef unit.
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index 8bcbc712..a4d0526d 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -924,21 +924,12 @@ Definition transl_function (f: Machblock.function) :=
          Pget GPRA RA ::b
          storeind_ptr GPRA SP f.(fn_retaddr_ofs) ::b lb)).
 
-Fixpoint size_blocks (l: bblocks): Z :=
-  match l with
-  | nil => 0
-  | b :: l =>
-     (size b) + (size_blocks l)
-  end
-  .
-
 Definition transf_function (f: Machblock.function) : res Asmblock.function :=
   do tf <- transl_function f;
   if zlt Ptrofs.max_unsigned (size_blocks tf.(fn_blocks))
   then Error (msg "code size exceeded")
   else OK tf.
 
-
 Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef :=
   transf_partial_fundef transf_function f.
 
-- 
cgit