Frama-C Bug Tracking System - Frama-C
View Issue Details
0002214Frama-CPlug-in > wppublic2016-03-03 16:472016-06-21 14:08
davyg 
correnson 
normalmajoralways
closedfixed 
All
Frama-C Magnesium 
Frama-C Aluminium 
0002214: Reals are bad encoded for coq
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.
I think that any coq proof you try to prove with wp containing real constant should have the error
No tags attached.
Issue History
2016-03-03 16:47davygNew Issue
2016-03-03 16:47davygStatusnew => assigned
2016-03-03 16:47davygAssigned To => correnson
2016-03-29 14:40corrensonStatusassigned => resolved
2016-03-29 14:40corrensonResolutionopen => fixed
2016-06-21 14:08signolesFixed in Version => Frama-C Aluminium
2016-06-21 14:08signolesStatusresolved => closed

There are no notes attached to this issue.