From 61410a182bfeb82043c1cb519b81d3dc8f4e997e Mon Sep 17 00:00:00 2001
From: Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr>
Date: Mon, 20 Jul 2020 11:47:06 +0200
Subject: Add dynamically checked assumption to simplify Asmgenproof

Previously Asmblock.label_pos and Asm.label_pos could point to different
memory location for the same label.
---
 aarch64/Asm.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'aarch64/Asm.v')

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 369e6f3b..dc1faddd 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -240,7 +240,7 @@ Fixpoint label_pos (lbl: label) (pos: Z) (c: code) {struct c} : option Z :=
   match c with
   | nil => None
   | instr :: c' =>
-      if is_label lbl instr then Some (pos + 1) else label_pos lbl (pos + 1) c'
+      if is_label lbl instr then Some pos else label_pos lbl (pos + 1) c'
   end.
 
 Definition nextinstr (rs: regset) :=
-- 
cgit