From e3613e0614ccc93c1013f7c39b58cffb6c21a76c Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Mon, 10 May 2021 17:49:29 +0200
Subject: new strong_state predicate and lemma

---
 scheduling/BTL.v | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'scheduling/BTL.v')

diff --git a/scheduling/BTL.v b/scheduling/BTL.v
index a87f674b..bc0f0815 100644
--- a/scheduling/BTL.v
+++ b/scheduling/BTL.v
@@ -786,6 +786,11 @@ Definition verify_function dupmap f f' : res unit :=
   do _ <- verify_is_copy dupmap (fn_entrypoint f) (RTL.fn_entrypoint f');
   verify_cfg dupmap (fn_code f) (RTL.fn_code f').
 
+Definition is_goto (ib: iblock): bool :=
+  match ib with
+  | Bgoto _ => true
+  | _ => false
+  end.
 
 Definition is_atom (ib: iblock): bool :=
  match ib with
-- 
cgit