diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index e54f95810601d05af5828bf7ea15f183ce797813..e04178b798290d3d7e3cb651dba0533eafe2f9fb 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -203,6 +203,7 @@ share/libc/__fc_define_wchar_t.h: CEA_LGPL
share/libc/__fc_define_wint_t.h: CEA_LGPL
share/libc/__fc_gcc_builtins.h: CEA_LGPL
share/libc/__fc_inet.h: CEA_LGPL
+share/libc/__fc_integer.h: CEA_LGPL
share/libc/__fc_machdep.h: CEA_LGPL
share/libc/__fc_machdep_linux_shared.h: CEA_LGPL
share/libc/__fc_runtime.c: CEA_LGPL
diff --git a/share/libc/__fc_integer.h b/share/libc/__fc_integer.h
new file mode 100644
index 0000000000000000000000000000000000000000..1dc5b29c85ecb486d3c65e5cd18f8ea208f50978
--- /dev/null
+++ b/share/libc/__fc_integer.h
@@ -0,0 +1,36 @@
+/**************************************************************************/
+/* */
+/* This file is part of Frama-C. */
+/* */
+/* Copyright (C) 2007-2019 */
+/* CEA (Commissariat à l'énergie atomique et aux énergies */
+/* alternatives) */
+/* */
+/* you can redistribute it and/or modify it under the terms of the GNU */
+/* Lesser General Public License as published by the Free Software */
+/* Foundation, version 2.1. */
+/* */
+/* It is distributed in the hope that it will be useful, */
+/* but WITHOUT ANY WARRANTY; without even the implied warranty of */
+/* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the */
+/* GNU Lesser General Public License for more details. */
+/* */
+/* See the GNU Lesser General Public License version 2.1 */
+/* for more details (enclosed in the file licenses/LGPLv2.1). */
+/* */
+/**************************************************************************/
+
+
+#ifndef Frama_C_INTEGER
+#define Frama_C_INTEGER
+#include "features.h"
+__PUSH_FC_STDLIB
+
+/*@
+
+ logic boolean bit_test(integer x, integer pos) = (boolean)(x & (1<<pos));
+
+ */
+
+__POP_FC_STDLIB
+#endif
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 46942381492b89e23c8e684a97e9003fd9e9790c..572ea84ed4bb57d943d9e72db76deabeeaa559b8 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -94,11 +94,18 @@ let f_land = Lang.extern_f ~library ~result ~category:(Operator op_land) ~balanc
let f_lxor = Lang.extern_f ~library ~result ~category:(Operator op_lxor) ~balance "lxor"
let f_lsl = Lang.extern_f ~library ~result "lsl"
let f_lsr = Lang.extern_f ~library ~result "lsr"
-let f_bit = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
let f_bitwised = [ f_lnot ; f_lor ; f_land ; f_lxor ; f_lsl ; f_lsr ]
-let () = let open LogicBuiltins in add_builtin "\\bit_test" [Z;Z] f_bit
+(* [f_bit_stdlib] is related to the function [bit_test] of Frama-C StdLib *)
+let f_bit_stdlib = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
+(* [f_bit_positive] is actually exported in forgoting the fact the position is positive *)
+let f_bit_positive = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
+(* At export, some constructs such as [e & (1 << k)] are written into [f_bit_export] construct *)
+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
(* -------------------------------------------------------------------------- *)
(* --- Matching utilities for simplifications --- *)
@@ -213,6 +220,10 @@ let match_list_head match_f = function
| [] -> raise Not_found
| e::es -> (match_f e), es
+let match_binop_one_arg1 binop e = match F.repr e with
+ | Logic.Fun( f , [one; e2] ) when Fun.equal f binop && one == e_one -> e2
+ | _ -> raise Not_found
+
let match_list_extraction match_f =
let match_f_opt n = try Some (match_f n) with Not_found -> None in
let rec aux rs = function
@@ -232,6 +243,8 @@ let match_positive_or_null_integer_arg2 =
let match_integer_extraction = match_list_head match_integer
let match_power2_extraction = match_list_extraction match_power2
+let match_binop_one_extraction binop = match_list_extraction (match_binop_one_arg1 binop)
+
(* -------------------------------------------------------------------------- *)
(* --- Conversion Symbols --- *)
@@ -465,7 +478,17 @@ let smp2 f zf = (* f(c1,c2) ~> zf(c1,c2), f(c1,c2,...) ~> f(zf(c1,c2),...) *)
end
| _ -> raise Not_found
-let bitk_positive k e = e_fun f_bit [e;k]
+let bitk_positive k e = F.e_fun f_bit_positive [e;k]
+let smp_mk_bit_stdlib = function
+ | [ a ; k ] when is_positive_or_null k ->
+ (* No need to expand the logic definition of the ACSL stdlib symbol when
+ [k] is positive (the definition must comply with that simplification). *)
+ bitk_positive k a
+ | [ a ; k ] ->
+ (* TODO: expand the current logic definition of the ACSL stdlib symbol *)
+ F.e_neq F.e_zero (F.e_fun f_land [a; (F.e_fun f_lsl [F.e_one;k])])
+ | _ -> raise Not_found
+
let smp_bitk_positive = function
| [ a ; k ] -> (* requires k>=0 *)
begin
@@ -738,6 +761,15 @@ let smp_leq_with_lsr a0 b0 =
else
smp_cmp_with_lsr e_leq a0 b0
+(* Rewritting at export *)
+let export_eq_with_land a b =
+ let es = match_fun f_land a in
+ if b == e_zero then
+ let k,_,es = match_binop_one_extraction f_lsl es in
+ (* e1 & ... & en & (1 << k) = 0 <==> !bit_test(e1 & ... & en, k) *)
+ e_not (e_fun f_bit_export [e_fun f_land es ; k ])
+ else raise Not_found
+
(* ACSL Semantics *)
type l_builtin = {
f: lfun ;
@@ -753,7 +785,10 @@ let () =
begin
let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
- let bi_lbit = mk_builtin "f_bit" f_bit smp_bitk_positive in
+ (* From [smp_mk_bit_stdlib], the built-in [f_bit_stdlib] is such that there is
+ no creation of [e_fun f_bit_stdlib args] *)
+ let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_mk_bit_stdlib in
+ let bi_lbit = mk_builtin "f_bit" f_bit_positive smp_bitk_positive in
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
(smp1 Integer.lognot) in
let bi_lxor = mk_builtin "f_lxor" f_lxor ~eq:smp_eq_with_lxor
@@ -777,8 +812,9 @@ let () =
| None -> ()
| Some leq -> F.set_builtin_leq f leq)
end
- [bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr]
+ [bi_lbit_stdlib ; bi_lbit; bi_lnot; bi_lxor; bi_lor; bi_land; bi_lsl; bi_lsr];
+ Lang.For_export.set_builtin_eq f_land export_eq_with_land
end
end
diff --git a/src/plugins/wp/Cint.mli b/src/plugins/wp/Cint.mli
index a78c5b919096d068d016650c23cfdbca586f78bc..be94baad52b5c7285e47f53342ba4fa9ec609a62 100644
--- a/src/plugins/wp/Cint.mli
+++ b/src/plugins/wp/Cint.mli
@@ -71,9 +71,8 @@ val f_lxor : lfun
val f_lor : lfun
val f_lsl : lfun
val f_lsr : lfun
-val f_bit : lfun
-val f_bitwised : lfun list (** All except f_bit *)
+val f_bitwised : lfun list (** All except f_bit_positive *)
(** Simplifiers *)
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 2ba8603148d81bef9b2ec9b53360ab91c4c5bf55..b5b2010ef36b168df4281e1a6034a921e207da51 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -1001,6 +1001,10 @@ module For_export = struct
add_init (fun () -> QZERO.set_builtin f c)
let set_builtin' f c =
add_init (fun () -> QZERO.set_builtin' f c)
+ let set_builtin_eq f c =
+ add_init (fun () -> QZERO.set_builtin_eq f c)
+ let set_builtin_leq f c =
+ add_init (fun () -> QZERO.set_builtin_leq f c)
let in_state f v = QZERO.in_state (get_state ()) f v
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index af9ac3bb08b228a2aed5effed33e13389dfdddff..f4eb792d3209e0adb160e7de564dd092fd698625 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -604,6 +604,9 @@ module For_export : sig
val set_builtin : Fun.t -> (term list -> term) -> unit
val set_builtin' : Fun.t -> (term list -> tau option -> term) -> unit
+ val set_builtin_eq : Fun.t -> (term -> term -> term) -> unit
+ val set_builtin_leq : Fun.t -> (term -> term -> term) -> unit
+
val in_state: ('a -> 'b) -> 'a -> 'b
end
diff --git a/src/plugins/wp/share/wp.driver b/src/plugins/wp/share/wp.driver
index 59acd4e6da61d3c1fb19e5782ed52a1dfc6fa941..a14b3702ffc32e1ad33dd031ac38724ca1d0ed72 100644
--- a/src/plugins/wp/share/wp.driver
+++ b/src/plugins/wp/share/wp.driver
@@ -86,6 +86,7 @@ why3.import += "frama_c_wp.cint.Cint";
altergo.file += "ergo/Cint.mlw";
library cbits: cint
+logic boolean "bit_test"(integer,integer) := \bit_test_stdlib;
coq.file += "coqwp/Cbits.v";
altergo.file += "ergo/Cbits.mlw";
why3.import += "frama_c_wp.cbits.Cbits";
diff --git a/src/plugins/wp/tests/wp_plugin/bit_test.i b/src/plugins/wp/tests/wp_plugin/bit_test.c
similarity index 80%
rename from src/plugins/wp/tests/wp_plugin/bit_test.i
rename to src/plugins/wp/tests/wp_plugin/bit_test.c
index 60be3f23f9fe9c4367687374d7f00e60dd730eea..b0b19bf9b8c72db53bc2885dc90e402987c6cb08 100644
--- a/src/plugins/wp/tests/wp_plugin/bit_test.i
+++ b/src/plugins/wp/tests/wp_plugin/bit_test.c
@@ -31,3 +31,14 @@ void check2(int order1, int order2)
{
return;
}
+
+
+#include "__fc_integer.h"
+
+/*@
+ ensures ko: bit_test(order1, 0) ≡ bit_test(order2, 0);
+ */
+void check3(int order1, int order2)
+{
+ return;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
index 5d4dc91a0c92256b4dc83327de57f2058f7ecd46..e56158295b1cdb7d71133f15a396221cf4c508d0 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
@@ -1,5 +1,5 @@
# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/bit_test.i (no preprocessing)
+[kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
@@ -21,3 +21,12 @@ Assume { Type: is_sint32(order1_0) /\ is_sint32(order2_0). }
Prove: bit_test(order2_0, 0) <-> bit_test(order1_0, 0).
------------------------------------------------------------
+------------------------------------------------------------
+ Function check3
+------------------------------------------------------------
+
+Goal Post-condition 'ko' in 'check3':
+Assume { Type: is_sint32(order1_0) /\ is_sint32(order2_0). }
+Prove: bit_test(order2_0, 0) <-> bit_test(order1_0, 0).
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
index a336b257ec30f532260cf835cfd9f1e94c0d3a06..40432fecac9796bf6a8309e254f86d77942b22df 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
@@ -1,17 +1,19 @@
# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
-[kernel] Parsing tests/wp_plugin/bit_test.i (no preprocessing)
+[kernel] Parsing tests/wp_plugin/bit_test.c (with preprocessing)
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] 2 goals scheduled
+[wp] 3 goals scheduled
[wp] [Alt-Ergo 2.0.0] Goal typed_bit_test_check1_ensures_ko : Typechecked
[wp] [Alt-Ergo 2.0.0] Goal typed_bit_test_check2_ensures_ko : Typechecked
-[wp] Proved goals: 0 / 2
- Alt-Ergo 2.0.0: 0 (unsuccess: 2)
+[wp] [Alt-Ergo 2.0.0] Goal typed_bit_test_check3_ensures_ko : Typechecked
+[wp] Proved goals: 0 / 3
+ Alt-Ergo 2.0.0: 0 (unsuccess: 3)
[wp] Report in: 'tests/wp_plugin/oracle_qualif/bit_test.0.report.json'
[wp] Report out: 'tests/wp_plugin/result_qualif/bit_test.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
check1 - - 1 0.0%
check2 - - 1 0.0%
+check3 - - 1 0.0%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
index b3c763edb42b9d083a39c28e18b6e075d7b9f32b..d26be5ba50b3a72e23c8e952854f323150b5fc78 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_bitwise.0.res.oracle
@@ -23,10 +23,10 @@
[wp] Report out: 'tests/wp_typed/result_qualif/user_bitwise.0.report.json'
-------------------------------------------------------------
Functions WP Alt-Ergo Total Success
-rl1 1 1 (48..60) 2 100%
-rr1 - 2 (44..56) 2 100%
-rln32 - 2 (96..120) 2 100%
-rrn32 - 2 (96..120) 2 100%
-rln64 - 2 (96..120) 2 100%
-rrn64 - 2 (96..120) 2 100%
+rl1 1 1 (52..64) 2 100%
+rr1 - 2 (52..64) 2 100%
+rln32 - 2 (64..88) 2 100%
+rrn32 - 2 (64..88) 2 100%
+rln64 - 2 (64..88) 2 100%
+rrn64 - 2 (64..88) 2 100%
-------------------------------------------------------------
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index fc16d42e53565a5da65a9dd3e84c11aa488a48c9..e85ef1cf9e12a1987c8e2da16cd1ca85923d016b 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -36,6 +36,7 @@
[kernel] Parsing share/libc/__fc_define_wint_t.h (with preprocessing)
[kernel] Parsing share/libc/__fc_gcc_builtins.h (with preprocessing)
[kernel] Parsing share/libc/__fc_inet.h (with preprocessing)
+[kernel] Parsing share/libc/__fc_integer.h (with preprocessing)
[kernel] Parsing share/libc/__fc_machdep.h (with preprocessing)
skipping share/libc/__fc_machdep_linux_shared.h
[kernel] Parsing share/libc/__fc_select.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..73dac90425a73c971fb285476320f30bc36be7d1 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -0,0 +1 @@
+#include "__fc_integer.h"