Don Armstrong <don@donarmstrong.com>:
It seems rather clear that those "source" files are just machine
code for the device firmware, and as such, are not the prefered
form for modification.
Agreed. So the files are not DFSG-free.
That pretty much precludes the linking of that code with the rest
of the kernel and/or forming a derivative work of the kernel and
our distribution of such a resultant work, well before we even
get into the DFSG §2 discussion.[1]
The situation is somewhat ambiguous. One might argue that the
device driver code is not part of the kernel even though it's
included in the source tree for practical reasons and that there is
therefore no problem with the GPL. However, there's no point in
discussing that question in debian-legal as the code has to be
separated in any case, because it is not DFSG-free.
Edmund