Comment by kevin_thibedeau

It doesn't matter what form it takes. Compiled binaries of GPL code are being distributed. The recipients of that binary are entitled to the source of the GPL portions in a usable form:

  "The source code for a work means the preferred form of the work for making modifications to it. For an executable work, complete source code means all the source code for all modules it contains, plus any associated interface definition files, plus the scripts used to control compilation and installation of the executable."

The GPL here doesn't extend beyond the kernel boundary. Userland is isolated unless they have GPL code linked in there as well. If they were careless about the linkage boundaries then that's on them.