Frama-C Bug Tracking System - Frama-C
View Issue Details
0001277Frama-CKernelpublic2012-09-20 12:012014-02-12 16:58
normaltweakhave not tried
Frama-C Oxygen-20120901 
Frama-C Fluorine-20130401 
0001277: Datatype.triple is missing
I used to have :
    Dynamic.register ... (Datatype.func Cil_datatype.Stmt.ty XXX.ty)
    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 ?

No tags attached.
Issue History
2012-09-20 12:01AnneNew Issue
2012-09-20 13:09signolesStatusnew => assigned
2012-09-20 13:09signolesAssigned To => signoles
2012-09-20 15:59svnCheckin
2012-09-20 15:59svnStatusassigned => resolved
2012-09-20 15:59svnResolutionopen => fixed
2012-09-20 16:01signolesNote Added: 0003476
2012-09-20 16:03signolesNote Added: 0003477
2013-04-19 11:05signolesFixed in Version => Frama-C Fluorine
2013-04-19 11:05signolesStatusresolved => closed
2014-02-12 16:58signolesNote Added: 0004615
2014-02-12 16:58signolesStatusclosed => resolved

2012-09-20 16:01   
Workaround :
module A = Datatype.List(Datatype.String)
module XXX = Datatype.Triple(A)(A)(A)

Anyway this workaround is more efficient than your original code.
2012-09-20 16:03   
As you suggested, Datatype.triple and Datatype.quadruple is also added to the Frama-C API by the same commit.
2014-02-12 16:58   
Fix committed to stable/neon branch.