diff --git a/src/plugins/wp/tests/wp_plugin/bit_test.driver b/src/plugins/wp/tests/wp_plugin/bit_test.driver
new file mode 100644
index 0000000000000000000000000000000000000000..2a03e83b656e0d541afaa5b8cef601278779f058
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/bit_test.driver
@@ -0,0 +1,11 @@
+library c2fc_bit : cbits;
+
+logic boolean lbtest (integer, integer) = "bit_testb";
+
+predicate btest (integer, integer) =
+ "bit_test";
+
+
+logic boolean lbtest_qed (integer, integer) := \bit_test;
+
+predicate btest_qed (integer, integer) := \bit_test;
diff --git a/src/plugins/wp/tests/wp_plugin/bit_test.i b/src/plugins/wp/tests/wp_plugin/bit_test.i
new file mode 100644
index 0000000000000000000000000000000000000000..60be3f23f9fe9c4367687374d7f00e60dd730eea
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/bit_test.i
@@ -0,0 +1,33 @@
+/* run.config
+ OPT: -wp-driver tests/wp_plugin/bit_test.driver
+ */
+
+/* run.config_qualif
+ OPT: -wp-driver tests/wp_plugin/bit_test.driver -wp-prover why3:alt-ergo -wp-check
+*/
+
+/*@
+axiomatic btest {
+ logic 𔹠lbtest(ℤ v, ℤ n) ;
+ predicate btest(ℤ v, ℤ n) ;
+ logic 𔹠lbtest_qed(ℤ v, ℤ n) ;
+ predicate btest_qed(ℤ v, ℤ n) ;
+
+ }
+ */
+
+/*@
+ ensures ko: lbtest(order1, 0) ≡ lbtest(order2, 0);
+ */
+void check1(int order1, int order2)
+{
+ return;
+}
+
+/*@
+ ensures ko: lbtest_qed(order1, 0) ≡ lbtest_qed(order2, 0);
+ */
+void check2(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
new file mode 100644
index 0000000000000000000000000000000000000000..5d4dc91a0c92256b4dc83327de57f2058f7ecd46
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle
@@ -0,0 +1,23 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/bit_test.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function check1
+------------------------------------------------------------
+
+Goal Post-condition 'ko' in 'check1':
+Assume { Type: is_sint32(order1_0) /\ is_sint32(order2_0). }
+Prove: bit_testb(order2_0, 0) = bit_testb(order1_0, 0).
+
+------------------------------------------------------------
+------------------------------------------------------------
+ Function check2
+------------------------------------------------------------
+
+Goal Post-condition 'ko' in 'check2':
+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
new file mode 100644
index 0000000000000000000000000000000000000000..a336b257ec30f532260cf835cfd9f1e94c0d3a06
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle
@@ -0,0 +1,17 @@
+# frama-c -wp -wp-timeout 45 -wp-steps 1500 [...]
+[kernel] Parsing tests/wp_plugin/bit_test.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 2 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] 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%
+-------------------------------------------------------------
diff --git a/src/plugins/wp/why3_api.ml b/src/plugins/wp/why3_api.ml
index 66212e3543ecc6151fcb45833f14f61ae37e3a58..1287186af6f4c34a75f4e4aa8e612e2516ce2291 100644
--- a/src/plugins/wp/why3_api.ml
+++ b/src/plugins/wp/why3_api.ml
@@ -435,25 +435,28 @@ let rec of_term ~cnv expected t : Why3.Term.term =
let t_app ls l r =
Why3.Term.t_app ls l r
in
- let apply_from_ns s l =
- match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)), sort with
- | ls, (Prop | Bool) -> t_app ls l (of_tau cnv sort)
- | ls, _ -> t_app ls l (of_tau cnv expected)
+ let apply_from_ns s l sort =
+ match Why3.Theory.(ns_find_ls (get_namespace cnv.th) (cut_path s)), expected with
+ | ls, (Prop | Bool) ->
+ coerce ~cnv sort expected $
+ t_app ls l (of_tau cnv sort)
+ | ls, _ ->
+ coerce ~cnv sort expected $
+ t_app ls l (of_tau cnv sort)
| exception Not_found -> Wp_parameters.fatal "Can't find [%s] in why3 namespace" s
in
let apply_from_ns' s l =
apply_from_ns s (List.map (fun e -> of_term' cnv e) l)
in
- coerce ~cnv sort expected $
match lfun_name f, expected with
- | F_call s, _ -> apply_from_ns' s l
+ | F_call s, _ -> apply_from_ns' s l sort
| Qed.Engine.F_subst _, _ -> Wp_parameters.not_yet_implemented "lfun with subst"
| Qed.Engine.F_left s, _ | Qed.Engine.F_assoc s, _ ->
let rec aux = function
| [] -> Wp_parameters.fatal "Empty application"
| [a] -> of_term cnv expected a
| a::l ->
- apply_from_ns s [of_term' cnv a; aux l]
+ apply_from_ns s [of_term' cnv a; aux l] sort
in
aux l
| Qed.Engine.F_right s, _ ->
@@ -461,18 +464,18 @@ let rec of_term ~cnv expected t : Why3.Term.term =
| [] -> Wp_parameters.fatal "Empty application"
| [a] -> of_term cnv expected a
| a::l ->
- apply_from_ns s [aux l;of_term' cnv a]
+ apply_from_ns s [aux l;of_term' cnv a] sort
in
aux (List.rev l)
| Qed.Engine.F_list (fcons,fnil), _ ->
let rec aux = function
- | [] -> apply_from_ns fnil []
+ | [] -> apply_from_ns fnil [] sort
| a::l ->
- apply_from_ns fcons [of_term' cnv a;aux l]
+ apply_from_ns fcons [of_term' cnv a;aux l] sort
in
aux l
| Qed.Engine.F_bool_prop (s,_), Bool | Qed.Engine.F_bool_prop (_,s), Prop ->
- apply_from_ns' s l
+ apply_from_ns' s l expected
| Qed.Engine.F_bool_prop (_,_), _ ->
Wp_parameters.fatal "badly expected type %a for term %a"
Lang.F.pp_tau expected Lang.F.pp_term t