I have a question about the Real-time Clock component (RTC) for the x86 VMM found here: https://github.com/SEL4PROJ/global-components/blob/master/components/RTC/RTC... Here is the text of the camkes file: import <RTC.idl4>; import <PutChar.idl4>; component CMOS { hardware; provides IOPort cmos_address; provides IOPort cmos_data; attribute string cmos_address_attributes = "0x70:0x70"; attribute string cmos_data_attributes = "0x71:0x71"; } component RTC { provides RTC rtc; maybe uses PutChar putchar; uses IOPort cmos_address; uses IOPort cmos_data; attribute int heap_size = 0; /* Connect the hardware RTC to the RTC component */ composition { component CMOS cmos; connection seL4HardwareIOPort rtc_cmos_address(from cmos_address, to cmos.cmos_address); connection seL4HardwareIOPort rtc_cmos_data(from cmos_data, to cmos.cmos_data); } configuration { cmos.cmos_address_attributes <- cmos_address_attributes; cmos.cmos_data_attributes <- cmos_data_attributes; } } What is the meaning of the last two statements in the configuration block? what is the scoping rules for the "cmos_address_attributes" and "cmos_data_attributes" variables? It looks like these attributes are already set in the definition of the CMOS component? They seemed to be assigned again in the configuration block? - John