2021-02-24 19:02 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001277Frama-CKernelpublic2014-02-12 16:58
ReporterAnne 
Assigned Tosignoles 
PrioritynormalSeveritytweakReproducibilityhave not tried
StatusclosedResolutionfixed 
Product VersionFrama-C Oxygen-20120901 
Target VersionFixed in VersionFrama-C Fluorine-20130401 
Summary0001277: Datatype.triple is missing
DescriptionI used to have :
    Dynamic.register ... (Datatype.func Cil_datatype.Stmt.ty XXX.ty)
with
    module XXX = Datatype.Triple (Datatype.List (Datatype.String))
                                 (Datatype.List (Datatype.String))
                                 (Datatype.List (Datatype.String))

but I guess that was wrong since in the new Oxygen version, it produces :
    "Invalid_argument(\"Descr.of_structural: inconsistent descriptor\")"
when I load my plug-in.

so now I am using :
let ty = Datatype.triple
             (Datatype.list Datatype.string)
             (Datatype.list Datatype.string)
             (Datatype.list Datatype.string)
instead of XXX.ty, and it is working, but I had to patch Datatype since it didn't define 'triple'. Could it be added in a next version, or is there another way of doing it ?

Thanks.
TagsNo tags attached.
Attached Files

-Relationships
+Relationships

-Notes

~0003476

signoles (manager)

Workaround :
module A = Datatype.List(Datatype.String)
module XXX = Datatype.Triple(A)(A)(A)

Anyway this workaround is more efficient than your original code.

~0003477

signoles (manager)

As you suggested, Datatype.triple and Datatype.quadruple is also added to the Frama-C API by the same commit.

~0004615

signoles (manager)

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-09-20 12:01 Anne New Issue
2012-09-20 13:09 signoles Status new => assigned
2012-09-20 13:09 signoles Assigned To => signoles
2012-09-20 15:59 svn
2012-09-20 15:59 svn Status assigned => resolved
2012-09-20 15:59 svn Resolution open => fixed
2012-09-20 16:01 signoles Note Added: 0003476
2012-09-20 16:03 signoles Note Added: 0003477
2013-04-19 11:05 signoles Fixed in Version => Frama-C Fluorine
2013-04-19 11:05 signoles Status resolved => closed
2013-12-19 01:11 signoles Source_changeset_attached => framac master 14ff667c
2014-02-12 16:53 signoles Source_changeset_attached => framac stable/neon 14ff667c
2014-02-12 16:58 signoles Note Added: 0004615
2014-02-12 16:58 signoles Status closed => resolved
+Issue History