GitLab

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)