From 32e31b63ed94e1330476a378c776190d5a9134e1 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr> Date: Mon, 25 Nov 2019 16:38:25 +0100 Subject: [PATCH] [wp] export bit-tests lfuns --- src/plugins/wp/Cint.ml | 5 +++++ src/plugins/wp/Cint.mli | 3 +++ 2 files changed, 8 insertions(+) diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml index c6d48f85cc3..f1e5eb696a3 100644 --- a/src/plugins/wp/Cint.ml +++ b/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 --- *) (* -------------------------------------------------------------------------- *) diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli index be94baad52b..2b830151f31 100644 --- a/src/plugins/wp/Cint.mli +++ b/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 *) -- GitLab