Hi,
I like the Camkes (3) tool and believe it is essential for making seL4 accessible for developers. However, I have noticed some unexpected limitations that I believe are either bugs or incomplete features.
Issue A: A hierarchical component cannot have a dataport with a custom data type. (However, a non-hierarchical component can have a dataport with a custom data type. Also, a hierarchical component can have a dataport with a built-in data type such as Buf.)
Issue B: A dataport provided by a sub-component cannot be exported as a dataport belonging to the hierarchical component that contains it. (However, the export of event notifications from sub-components works just fine.)
Attached is the relevant code that demonstrates both issues, which is a contrived example to highlight the issues without other stuff getting in the way. Please note that the code as is compiles just fine, however if you comment and uncomment a few lines of code (as instructed in Duck.camkes, Duckherd.camkes and Duckling.camkes), the issues can be demonstrated (separately) as compile failures.
There may be other issues with hierarchical components that I am not yet aware of, as the above issues (unfortunately) have prevented me from experimenting with them further.
Could you please acknowledge if these are issues that you are aware of, and if there is likely to be a fix in a future Camkes 4 release?
Regards, Dr Samuel Chenoweth Cyber Security Researcher DST Group
Note: I would have sent this email from my work email address ( samuel.chenoweth@dst.defence.gov.au), however I sent it from my personal address instead because of issues to do with our email gateway. All the contents of this email are UNCLASSIFIED and non-sensitive.