Frama-C Bug Tracking System - Frama-C
View Issue Details
0001603Frama-CPlug-in > wppublic2014-01-16 08:332014-03-13 15:57
Anne 
correnson 
normalmajorhave not tried
closedfixed 
Frama-C Fluorine-20130601 
Frama-C Neon-20140301 
0001603: Errors in coq files generated by WP
I noticed some errors in the coq files generated by WP: - real_of_int not defined, - is_float32 : R -> Prop but used as bool (is_float32 f_0%R))%R=true) - let x_0 := ((Zeq_bool 1 t_0))%Z in ... x_0 used both as bool and as Prop
The example is the foo.c file posted on [Frama-c-discuss] by David Mentre yesterday evening (15/01/2014 - 18:30)
No tags attached.
Issue History
2014-01-16 08:33AnneNew Issue
2014-01-16 08:33AnneStatusnew => assigned
2014-01-16 08:33AnneAssigned To => correnson
2014-01-20 09:20AnneNote Added: 0004423
2014-02-05 13:42corrensonNote Added: 0004493
2014-02-05 13:43corrensonNote Added: 0004494
2014-02-05 13:43corrensonStatusassigned => resolved
2014-02-05 13:43corrensonResolutionopen => fixed
2014-03-13 15:56signolesFixed in Version => Frama-C Neon-20140301
2014-03-13 15:57signolesStatusresolved => closed

Notes
(0004423)
Anne   
2014-01-20 09:20   
Another error : Goal let a_0 := (shift ((global (G_X_749)%Z)) 0%Z) in ... Error: The term "global G_X_749" has type "addr" while it is expected to have type "nat -> ?1".
(0004493)
correnson   
2014-02-05 13:42   
Fixed in trunk development version
(0004494)
correnson   
2014-02-05 13:43   
Fixed during why-3 migration