From 6b9b16b077a596c01c7c01a48e7b7341bb374029 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Wed, 24 Mar 2021 14:16:29 -0700
Subject: [PATCH] [sledge] Drop calls to llvm.dbg.label

Summary:
They only attach debug info to labels, and have no execution
behavior. At some later point it would be good to scan for these and
gather the attached debug info.

Reviewed By: jvillard

Differential Revision: D27262516

fbshipit-source-id: 2eb91a475
---
 sledge/cli/frontend.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index e070d7d91..27de3f81a 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -1145,7 +1145,7 @@ let xlate_instr :
               emit_term ~prefix:(pop loc @ pre) (Term.throw ~exc ~loc)
           | ["__llair_unreachable"] -> emit_term Term.unreachable
           (* dropped / handled elsewhere *)
-          | ["llvm"; "dbg"; ("declare" | "value")]
+          | ["llvm"; "dbg"; ("declare" | "label" | "value")]
            |"llvm" :: ("lifetime" | "invariant") :: ("start" | "end") :: _
             ->
               nop ()