Frama-C Bug Tracking System - Frama-C
View Issue Details
0001806Frama-CPlug-in > wppublic2014-06-12 09:532020-02-17 18:08
davyg 
correnson 
normalminorhave not tried
closedfixed 
Frama-C Neon-20140301 
Frama-C 20-Calcium 
0001806: Error in coq code generated by wp
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".
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)
No tags attached.
Issue History
2014-06-12 09:53davygNew Issue
2014-06-12 09:53davygStatusnew => assigned
2014-06-12 09:53davygAssigned To => correnson
2014-06-12 12:53corrensonRelationship addedduplicate of 0001587
2014-06-12 12:55corrensonRelationship deleted0001587
2019-10-17 14:35corrensonNote Added: 0006885
2019-10-17 14:35corrensonStatusassigned => resolved
2019-10-17 14:35corrensonResolutionopen => fixed
2019-10-17 14:35corrensonNote Edited: 0006885View Revisions
2020-02-17 18:06signolesFixed in Version => Frama-C 20-Calcium
2020-02-17 18:08signolesStatusresolved => closed
2020-02-17 18:08signolesNote Added: 0006946

Notes
(0006885)
correnson   
2019-10-17 14:35   
Fixed in upcoming 20.0 (Calcium) release
(0006946)
signoles   
2020-02-17 18:08   
Fixed in Frama-C 20.0 (Calcium).