>The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that t

>The files in question are, from a formal verification standpoint, the interface to CompCert. They are licensed under the non-commercial license (NCL) so that they can be used together with the rest of CompCert (the implementation of the compiler, so to speak), which is NCL-only. >Additionally, the interface files in question are also licensed under the GPL so that they can be used in other, open-source projects such as VST (http://vst.cs.princeton.edu/ http://vst.cs.princeton.edu/) that connect with CompCert. at https://github.com/AbsInt/CompCert/issues/140 https://github.com/AbsInt/CompCert/issues/140 (2016); GPL -> LGPL in a later commit.