[WP] Fix typing errors during export with driver which use builtins

src/plugins/wp/tests/wp_plugin/bit_test.driver

+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;

src/plugins/wp/tests/wp_plugin/bit_test.i

+/* 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;
+}

src/plugins/wp/tests/wp_plugin/oracle/bit_test.res.oracle

+# 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).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/bit_test.res.oracle

+# 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%
+-------------------------------------------------------------

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