Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001603Frama-CPlug-in > wppublic2014-01-16 08:332014-03-13 15:57
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
PlatformOSOS Version
Product VersionFrama-C Fluorine-20130601 
Target VersionFixed in VersionFrama-C Neon-20140301 
Summary0001603: Errors in coq files generated by WP
DescriptionI 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 InformationThe example is the foo.c file posted on [Frama-c-discuss] by David Mentre yesterday evening (15/01/2014 - 18:30)
TagsNo tags attached.
Attached Files

- Relationships

-  Notes
(0004423)
Anne (reporter)
2014-01-20 09:20

Another error :

Goal
  let a_0 := (shift ((global (G_X_749)%Z)) 0%Z) in ...

Error: The term "global G_X_749" has type "addr"
 while it is expected to have type "nat -> ?1".
(0004493)
correnson (manager)
2014-02-05 13:42

Fixed in trunk development version
(0004494)
correnson (manager)
2014-02-05 13:43

Fixed during why-3 migration

- Issue History
Date Modified Username Field Change
2014-01-16 08:33 Anne New Issue
2014-01-16 08:33 Anne Status new => assigned
2014-01-16 08:33 Anne Assigned To => correnson
2014-01-20 09:20 Anne Note Added: 0004423
2014-02-05 13:42 correnson Note Added: 0004493
2014-02-05 13:43 correnson Note Added: 0004494
2014-02-05 13:43 correnson Status assigned => resolved
2014-02-05 13:43 correnson Resolution open => fixed
2014-03-13 15:56 signoles Fixed in Version => Frama-C Neon-20140301
2014-03-13 15:57 signoles Status resolved => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker