extern /*@observer@*/ /*@null@*/ const dcroid_t* dcrp_oidget ( /*@in@*/ const char* h, /*@in@*/const char* t ) /*@ensures maxRead(result) >= 0@*/; extern /*@observer@*/const char* dcrp_oidlabel ( /*@in@*/const dcroid_t* oid );