2021-02-24 18:38 CET
  

View Issue Details [ Jump to Notes ] [ Issue History ] [ Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0001127Frama-CKernelpublic2012-03-21 10:352014-02-12 16:53
ReporterAnne 
Assigned Tosignoles 
PrioritynormalSeverityminorReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Nitrogen-20111001 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001127: Error in Type.pp_ml_name with Datatype.String.Set.ty
Description[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.
TagsNo tags attached.
Attached Files
  • ? file icon test.ml (195 bytes) 2012-03-21 10:52 - 
    let print ty = 
  Kernel.feedback "%s@.%t" (Type.name ty) (Type.pp_ml_name ty Type.Basic)

let main () = 
  print Datatype.String.ty;
  print Datatype.String.Set.ty

let () = Db.Main.extend main
    ? file icon test.ml (195 bytes) 2012-03-21 10:52 +

-Relationships
+Relationships

-Notes

~0002781

Anne (reporter)

2012-03-21 10:43

 Similar problem with:
  (Datatype.option Datatype.string)
which is printed:
  (Type.Option.instantiate Datatype.String.ty)

~0002782

signoles (manager)

2012-03-21 10:51

 Your guessing is right... I attach a simple reproducible script.

~0002973

Anne (reporter)

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 (manager)

2012-04-26 15:13

 Just resolved. Will be in Oxygen.

~0003481

Anne (reporter)

2012-10-02 15:07

 Same problem with Datatype.pair in Oxygen.
+Notes

-Issue History
Date Modified Username Field Change
2012-03-21 10:35 Anne New Issue
2012-03-21 10:43 Anne Note Added: 0002781
2012-03-21 10:50 signoles Status new => assigned
2012-03-21 10:50 signoles Assigned To => signoles
2012-03-21 10:51 signoles Note Added: 0002782
2012-03-21 10:51 signoles Status assigned => confirmed
2012-03-21 10:52 signoles File Added: test.ml
2012-03-21 10:54 Anne Description Updated
2012-04-26 13:44 Anne Note Added: 0002973
2012-04-26 15:13 signoles Note Added: 0002977
2012-04-26 15:13 signoles Status confirmed => resolved
2012-04-26 15:13 signoles Fixed in Version => Frama-C Oxygen-2012xx01
2012-04-26 15:13 signoles Resolution open => fixed
2012-09-19 17:16 signoles Status resolved => closed
2012-10-02 15:07 Anne Note Added: 0003481
2012-10-02 15:07 Anne Status closed => feedback
2012-10-02 15:07 Anne Resolution fixed => reopened
2012-10-16 15:30 svn
2012-10-16 15:30 signoles Status feedback => resolved
2012-10-16 15:30 signoles Resolution reopened => fixed
2013-04-19 11:05 signoles Fixed in Version Frama-C Oxygen-20120901 => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-05-06 13:43 svn
2013-05-06 15:25 svn
2013-12-19 01:11 signoles Source_changeset_attached => framac master c336941c
2013-12-19 01:11 signoles Source_changeset_attached => framac master 1ad43c33
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon c336941c
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon 1ad43c33
+Issue History