Reals are bad encoded for coq
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