From 3136a5071d92ba5dfa304d8a7177cda266f501e1 Mon Sep 17 00:00:00 2001
From: David Monniaux <david.monniaux@univ-grenoble-alpes.fr>
Date: Sat, 28 Mar 2020 23:24:16 +0100
Subject: pass to insert a "nop" at head of each function

---
 backend/FirstNop.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'backend/FirstNop.v')

diff --git a/backend/FirstNop.v b/backend/FirstNop.v
index 3d2211bc..f7e5261e 100644
--- a/backend/FirstNop.v
+++ b/backend/FirstNop.v
@@ -3,7 +3,7 @@ Require Import AST Linking.
 Require Import Memory Registers Op RTL.
 
 Definition transf_function (f: function) : function :=
-  let start_pc := max_pc_function f in
+  let start_pc := Pos.succ (max_pc_function f) in
   {| fn_sig := f.(fn_sig);
      fn_params := f.(fn_params);
      fn_stacksize := f.(fn_stacksize);
-- 
cgit