[wp] export bit-tests lfuns

src/plugins/wp/Cint.ml

@@ -107,6 +107,11 @@ let f_bit_export   = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" (
 let () = let open LogicBuiltins in add_builtin "\\bit_test_stdlib" [Z;Z] f_bit_stdlib
 let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit_positive
 
+let f_bits = [ f_bit_stdlib ; f_bit_positive ; f_bit_export ]
+
+let bit_test e k =
+  F.e_fun (if k <= 0 then f_bit_positive else f_bit_stdlib) [e ; e_int k]
+
 (* -------------------------------------------------------------------------- *)
 (* --- Matching utilities for simplifications                             --- *)
 (* -------------------------------------------------------------------------- *)

src/plugins/wp/Cint.mli

@@ -73,6 +73,9 @@ val f_lsl  : lfun
 val f_lsr  : lfun
 
 val f_bitwised : lfun list (** All except f_bit_positive *)
+val f_bits : lfun list (** All bit-test functions *)
+
+val bit_test : term -> int -> term
 
 (** Simplifiers *)