CompCert – Formally-verified C compiler
As noted in the License section of the readme,> CompCert is not free software. This non-commercial release can only be used for evaluation, research, educational and personal purposes. A commercial version of CompCert, without this restriction and with professional support and extra features, can be purchased from AbsInt. See the file LICENSE for more information.However, https://github.com/AbsInt/CompCert/blob/master/LICENSE goes onto say that> The following files in this distribution are dual-licensed both under
the INRIA Non-Commercial License Agreement and under the Free Software
Foundation GNU Lesser General Public License, either version 2.1 or
(at your option) any later version: ...and then lists a bunch of specific files and paths, which may or may not (this is the key question) constitute a majority of the repo. Looking around, I see a few references to the LGPL and LGPLv3.The LICENSE also makes clear (immediately following the file list) that> If you opt for the GNU Lesser
General Public License, these files are free software and can be used
both in commercial and non-commercial contexts, subject to the terms
of the GNU Lesser General Public License.So, broadly speaking: am I just looking at a standard smoke-and-mirrors routine (creating just enough uncertainty that most commercial operations would reasonably pursue the custom license) or are there any actual intuition-violating footguns hiding anywhere in the codebase?