Errors in coq files generated by WP
ID0001603: This issue was created automatically from Mantis Issue 1603. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0001603 | Frama-C | Plug-in > wp | public | 2014-01-16 | 2014-03-13 |
| Reporter | Anne | Assigned To | correnson | Resolution | fixed |
| Priority | normal | Severity | major | Reproducibility | have not tried |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Fluorine-20130601 | Target Version | - | Fixed in Version | Frama-C Neon-20140301 |
Description :
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
Additional Information :
The example is the foo.c file posted on [Frama-c-discuss] by David Mentre yesterday evening (15/01/2014 - 18:30)