be_get_default_isa
return ((strcmp((char *)be_get_default_isa(), name) == 0));
char *be_get_default_isa(void);