Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002214Frama-CPlug-in > wppublic2016-03-03 16:472016-06-21 14:08
Reporterdavyg 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityalways
StatusclosedResolutionfixed 
PlatformAllOSOS Version
Product VersionFrama-C Magnesium 
Target VersionFixed in VersionFrama-C Aluminium 
Summary0002214: Reals are bad encoded for coq
DescriptionThe 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 ReproduceI think that any coq proof you try to prove with wp containing real constant should have the error
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
There are no notes attached to this issue.

- Issue History
Date Modified Username Field Change
2016-03-03 16:47 davyg New Issue
2016-03-03 16:47 davyg Status new => assigned
2016-03-03 16:47 davyg Assigned To => correnson
2016-03-29 14:40 correnson Status assigned => resolved
2016-03-29 14:40 correnson Resolution open => fixed
2016-06-21 14:08 signoles Fixed in Version => Frama-C Aluminium
2016-06-21 14:08 signoles Status resolved => closed


Copyright © 2000 - 2017 MantisBT Team
Powered by Mantis Bugtracker