From 868a8b85266cfc8f19eacabd3af3618c2d2d6c8f Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 6 Nov 2020 06:15:47 -0800
Subject: [PATCH] [sledge] Interpret conversions between pointer types as
identity
Summary:
Since non-integral address spaces are not currently supported anyhow,
this does not introduce additional infidelity.
Reviewed By: da319
Differential Revision: D24746234
fbshipit-source-id: 1f6887a78
---
sledge/src/llair_to_Fol.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/sledge/src/llair_to_Fol.ml b/sledge/src/llair_to_Fol.ml
index 48493a7a9..5ede842a4 100644
--- a/sledge/src/llair_to_Fol.ml
+++ b/sledge/src/llair_to_Fol.ml
@@ -86,6 +86,7 @@ and term : Llair.Exp.t -> T.t =
| Some fml -> F.inject fml
| _ -> uap1 (Unsigned bits) a
else uap1 (Unsigned bits) a
+ | Ap1 (Convert {src= Pointer _}, Pointer _, e) -> term e
| Ap1 (Convert {src}, dst, e) ->
let s =
Format.asprintf "convert_%a_of_%a" Llair.Typ.pp dst Llair.Typ.pp src