diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml index 6b89bba519386a97b974f290eca81a5e3ba0933b..2022682fa13c33f0c73268591b97b0181baaa564 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 3c9db48c536ba039e7e9bba155e2824170828161..fc818fbe4b66450710ded247878f46daa944102a 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 ***********************************) (**************************************************************************)