2021-03-02 02:21 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001603Frama-CPlug-in > wppublic2014-03-13 15:57
ReporterAnne 
Assigned Tocorrenson 
PrioritynormalSeveritymajorReproducibilityhave not tried
StatusclosedResolutionfixed 
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
+Relationships

-Notes

~0004423

Anne (reporter)

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)

Fixed in trunk development version

~0004494

correnson (manager)

Fixed during why-3 migration
+Notes

-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
+Issue History