CompCert – Formally-verified C compiler
As noted in the <i>License</i> section of the readme,<p>> <i>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.</i><p>However, <a href="https://github.com/AbsInt/CompCert/blob/master/LICENSE" rel="nofollow">https://github.com/AbsInt/CompCert/blob/master/LICENSE</a> goes onto say that<p>> <i>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: ...</i><p>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.<p>The LICENSE also makes clear (immediately following the file list) that<p>> <i>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.</i><p>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?