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
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel
