From fb094ab04609e5f8e69017295ac78dffe38e7fcb Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Thu, 12 Nov 2020 16:38:16 -0800
Subject: [PATCH] [sledge] Detect and fail invoke instrs that call inline asm

Summary:
Calling an inline asm function that might raise is not currently
supported.

Reviewed By: jvillard

Differential Revision: D24846675

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

diff --git a/sledge/cli/frontend.ml b/sledge/cli/frontend.ml
index 50d1c5326..c15a19745 100644
--- a/sledge/cli/frontend.ml
+++ b/sledge/cli/frontend.ml
@@ -1176,6 +1176,8 @@ let xlate_instr :
       (* unimplemented *)
       | "llvm" :: "experimental" :: "gc" :: "statepoint" :: _ ->
           todo "statepoints:@ %a" pp_llvalue instr ()
+      | _ when Poly.equal (Llvm.classify_value llfunc) InlineAsm ->
+          todo "inline asm: @ %a" pp_llvalue instr ()
       (* general function call that may throw *)
       | _ ->
           let pre_0, callee = xlate_func_name x llfunc in