Frama-C Bug Tracking System - Frama-C
View Issue Details
0001127Frama-CKernelpublic2012-03-21 10:352014-02-12 16:53
Anne 
signoles 
normalminorhave not tried
closedfixed 
Frama-C Nitrogen-20111001 
Frama-C Fluorine-20130401 
0001127: Error in Type.pp_ml_name with Datatype.String.Set.ty
[Type.pp_ml_name ty Type.Call] for [ty = Datatype.String.Set.ty] prints [Datatype.String.Set(string).ty] instead of [Datatype.String.Set.ty] which leads to errors when loading some automatically generated scripts. I guess that the problem affects the generated journals, but don't have time to find an example. Sorry.
No tags attached.
? test.ml (195) 2012-03-21 10:52
https://bts.frama-c.com/file_download.php?file_id=360&type=bug
Issue History
2012-03-21 10:35AnneNew Issue
2012-03-21 10:43AnneNote Added: 0002781
2012-03-21 10:50signolesStatusnew => assigned
2012-03-21 10:50signolesAssigned To => signoles
2012-03-21 10:51signolesNote Added: 0002782
2012-03-21 10:51signolesStatusassigned => confirmed
2012-03-21 10:52signolesFile Added: test.ml
2012-03-21 10:54AnneDescription Updated
2012-04-26 13:44AnneNote Added: 0002973
2012-04-26 15:13signolesNote Added: 0002977
2012-04-26 15:13signolesStatusconfirmed => resolved
2012-04-26 15:13signolesFixed in Version => Frama-C Oxygen-2012xx01
2012-04-26 15:13signolesResolutionopen => fixed
2012-09-19 17:16signolesStatusresolved => closed
2012-10-02 15:07AnneNote Added: 0003481
2012-10-02 15:07AnneStatusclosed => feedback
2012-10-02 15:07AnneResolutionfixed => reopened
2012-10-16 15:30svnCheckin
2012-10-16 15:30signolesStatusfeedback => resolved
2012-10-16 15:30signolesResolutionreopened => fixed
2013-04-19 11:05signolesFixed in VersionFrama-C Oxygen-20120901 => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2013-05-06 13:43svnCheckin
2013-05-06 15:25svnCheckin

Notes
(0002781)
Anne   
2012-03-21 10:43   
Similar problem with: (Datatype.option Datatype.string) which is printed: (Type.Option.instantiate Datatype.String.ty)
(0002782)
signoles   
2012-03-21 10:51   
Your guessing is right... I attach a simple reproducible script.
(0002973)
Anne   
2012-04-26 13:44   
Do you think there is a chance to have this fixed in the next version of Frama-C ? (just to know if I have to do a big work-around or if I can just wait ;-) )
(0002977)
signoles   
2012-04-26 15:13   
Just resolved. Will be in Oxygen.
(0003481)
Anne   
2012-10-02 15:07   
Same problem with Datatype.pair in Oxygen.