Error in coq code generated by wp

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)