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})
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