Skip to content

Error in Type.pp_ml_name with Datatype.String.Set.ty

ID0001127: This issue was created automatically from Mantis Issue 1127. Further discussion may take place here.


Id Project Category View Due Date Updated
ID0001127 Frama-C Kernel public 2012-03-21 2014-02-12
Reporter Anne Assigned To signoles Resolution fixed
Priority normal Severity minor Reproducibility have not tried
Platform - OS - OS Version -
Product Version Frama-C Nitrogen-20111001 Target Version - Fixed in Version Frama-C Fluorine-20130401

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.

Attachments

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information