diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 46942381492b89e23c8e684a97e9003fd9e9790c..fc88b1aedb83c77f621a146ca8366298faad33a1 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -94,10 +94,13 @@ 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 f_bit_stdlib = Lang.extern_p ~library ~bool:"bit_testb" ~prop:"bit_test" ()
+let f_bit = 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
(* -------------------------------------------------------------------------- *)
@@ -465,7 +468,13 @@ 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 [e;k]
+let smp_intro_bitk_positive = function
+ | [ a ; k ] when is_positive_or_null k -> 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
@@ -753,6 +762,7 @@ let () =
begin
let mk_builtin n f ?eq ?leq smp = n, { f ; eq; leq; smp } in
+ let bi_lbit_stdlib = mk_builtin "f_bit_stdlib" f_bit_stdlib smp_intro_bitk_positive in
let bi_lbit = mk_builtin "f_bit" f_bit smp_bitk_positive in
let bi_lnot = mk_builtin "f_lnot" f_lnot ~eq:smp_eq_with_lnot
(smp1 Integer.lognot) in
@@ -777,7 +787,7 @@ 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]
end
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%
-------------------------------------------------------------