GitLab

ID0002214: This issue was created automatically from Mantis Issue 2214. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002214	Frama-C	Plug-in > wp	public	2016-03-03	2016-06-21

Reporter	davyg	Assigned To	correnson	Resolution	fixed
Priority	normal	Severity	major	Reproducibility	always
Platform	All	OS	-	OS Version	-
Product Version	Frama-C Magnesium	Target Version	-	Fixed in Version	Frama-C Aluminium

Description :

The definition of real_base(Qedlib) in the coq exporter of wp is incorrect :

There is :

Definition real_base e a n := match n with | 0 => 1%R | Zpos n => (a * pow e (Pos.to_nat n))%R | Zneg n => (a / pow e (Pos.to_nat n))%R end.

in stead of

Definition real_base e a n := match n with | 0 => a | Zpos n => (a * pow e (Pos.to_nat n))%R | Zneg n => (a / pow e (Pos.to_nat n))%R end.

Steps To Reproduce :

I think that any coq proof you try to prove with wp containing real constant should have the error