From efe258316dd9a956d2afcfcf8a4ec65b8eb6ca96 Mon Sep 17 00:00:00 2001
From: Basile Desloges <basile.desloges@cea.fr>
Date: Wed, 10 Jun 2020 16:29:19 +0200
Subject: [PATCH] [eacsl] Add a function to check if a type is any of the GMP
 types

---
 src/plugins/e-acsl/src/libraries/gmp_types.ml  | 3 +++
 src/plugins/e-acsl/src/libraries/gmp_types.mli | 3 +++
 2 files changed, 6 insertions(+)

diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml
index 6b89bba5193..2022682fa13 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.ml
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml
@@ -123,6 +123,9 @@ let init () =
   end in
   try Cil.visitCilFileSameGlobals set_mp_t (Ast.get ()) with Exit -> ()
 
+let is_t ty =
+  Z.is_t ty || Q.is_t ty
+
 (*
 Local Variables:
 compile-command: "make -C ../../../../.."
diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.mli b/src/plugins/e-acsl/src/libraries/gmp_types.mli
index 3c9db48c536..fc818fbe4b6 100644
--- a/src/plugins/e-acsl/src/libraries/gmp_types.mli
+++ b/src/plugins/e-acsl/src/libraries/gmp_types.mli
@@ -27,6 +27,9 @@ open Cil_types
 val init: unit -> unit
 (** Must be called before any use of GMP *)
 
+val is_t: typ -> bool
+(** @return true iff the given type is equivalent to one of the GMP type. *)
+
 (**************************************************************************)
 (******************************** Types ***********************************)
 (**************************************************************************)
-- 
GitLab