I found this stack exchange post to be informative but not actually helpful. I am using SOFA (the C version), but the "correct" ICRF <=> ITRF conversion is not what I need. If ICRF is J2000 (other than the miliarcsecond bias) then ITRF is not the standard ECEF frame, where standard means (lat=0,lon=0,alt=0) converts to ECEF (x=radius at the equator, y=0, z=0), because at J2000.0 (terrestrial time noon on Jan 1, 2000) the earth rotation angle (ERA) is NOT zero (I'm forgetting the exact value of the angle but it's approximately 280 degrees, within a few degrees). The "casual" definition of the J2000 frame is that it was aligned with the standard ECEF frame at J2000.0. The linked to stack exchange post says/implies it is possible to use SOFA to convert between ECEF and ICRF (which I have been using synonymously with J2000, following the convention of NASA's SPICE toolkit) but I have not found any examples as to how to do so in the SOFA cookbooks or anywhere else online. I am already using Bulletin A files, and so far I was just subtracting of the ERA at J2000.0 from the ERA that I feed to the SOFA routines (and doing everything else as per the example of converting between ICRF and ITRF) but that seems hacky and perhaps a little dangerous for using in high consequence systems (involving satellites) and I'm hoping that someone reading this knows SOFA well enough to provide a C source code example of the officially sanctioned way to convert between the standard ECEF and ICRF. Or if ITRF really is the standard ECEF I'm hoping that someone would be able to reconcile the perceived inconsistency between the J2000 frame supposedly being (near) equivalent to ICRF, J2000 being aligned with the standard ECEF at J2000.0, and ERA not being anywhere close to zero at J2000.0. Thank you for your time and assistance.
The casual definition of J2000.0 was incorrect, and due to a misunderstanding on my part of imprecise language of the people I've been working with. The ECEF that J2000 is aligned with at J2000.0 is not "the standard" ECEF but "an" ECEF defined based on the equinox and mean equator. Thanks to Patrick Wallace for setting me straight.