1 2 3 4 5 6 7 8 9 10
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 );