ID0001806: **This issue was created automatically from Mantis Issue 1806. Further discussion may take place here.** --- | **Id** | **Project** | **Category** | **View** | **Due Date** | **Updated** | | --- | --- | --- | --- | --- | --- | | ID0001806 | Frama-C | Plug-in > wp | public | 2014-06-12 | 2020-02-17 | | | | | | | | | --- | --- | --- | --- | --- | --- | | **Reporter** | davyg | **Assigned To** | correnson | **Resolution** | fixed | | **Priority** | normal | **Severity** | minor | **Reproducibility** | have not tried | | **Platform** | - | **OS** | - | **OS Version** | - | | **Product Version** | Frama-C Neon-20140301 | **Target Version** | - | **Fixed in Version** | Frama-C 20-Calcium | ### Description : There is a typing error with some code generated by wp. For example this script : _Bool g() { return 0; } //@ensures x == (!!\result == !!x); _Bool f(_Bool x) { return g(); } When using prover coq from wp generates : Goal forall (f_0 x_0 : Z), ((is_uint32 f_0%Z)) -> ((is_uint32 x_0%Z)) -> ((((Zneq_bool 0 x_0)) = ((Zeq_bool ((Zneq_bool 0 f_0)) ((Zneq_bool 0 x_0)))))%Z)%Z. Proof. (* auto with zarith. *) Qed. which produce this coq error on "Zneq_bool 0 f_0": Error: In environment f_0 : int x_0 : int The term "Zneq_bool 0 f_0" has type "bool" while it is expected to have type "int". ### Steps To Reproduce : Just use the C example with wp/coq as prover (with the gui for example because else wp consider that the script fails and does not print the error)