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)