Hello,

I have been trying to generate Isabelle file from CapDL specification. But I run into an error when I'm running the command:

./parse-capDL --isabelle=out.thy --object-sizes=object_sizes.yaml example-arm.cdl 

warning: specifying untyped child multiple times is deprecated: ut = a, child = name
warning: specifying untyped child multiple times is deprecated: ut = b, child = name
warning: specifying untyped child multiple times is deprecated: ut = something, child = rm_ut

parse-capDL: CapDL/PrintIsabelle.hs:180:15-71: Irrefutable pattern failed for pattern ut@(Untyped {maybePaddr = Just utPaddr})

where example-arm.cdl is the example I got from CapDL repo (https://github.com/seL4/capdl/blob/master/capDL-tool/example-arm.cdl)

And object_sizes.yaml contains:

seL4_TCBObject: 10
seL4_EndpointObject: 4
seL4_NotificationObject: 4
seL4_SmallPageObject: 12
seL4_LargePageObject: 16
seL4_ASID_Pool: 12
seL4_ASID_Table: 10
seL4_Slot: 4
seL4_Value_MinUntypedBits: 4
seL4_Value_MaxUntypedBits: 29
seL4_PageTableObject: 10
seL4_PageDirectoryObject: 14
seL4_ARM_SectionObject: 20
seL4_ARM_SuperSectionObject: 24
seL4_IOPageTableObject: 12
seL4_IOPorts: 0
seL4_IODevice: 0
seL4_ARMIODevice: 0
seL4_IRQ: 0
seL4_IOAPICIRQ: 0
seL4_MSIIRQ: 0

The same error also occurs when I used parse-capdL executable generated by Camkes repo.
Is there any step I'm missing? Or does the tool not support the conversion to Isabelle?

Best,
Norrathep
--
Norrathep (Oak) Rattanavipanon
M.S. in Computer Science
University of California - Irvine