diff options
Diffstat (limited to 'LICENSE')
| -rw-r--r-- | LICENSE | 12 |
1 files changed, 10 insertions, 2 deletions
@@ -12,7 +12,7 @@ The latter is a separate contract document. The INRIA Non-Commercial License Agreement is a non-free license that grants you the right to use the CompCert verified compiler for educational, research or evaluation purposes only, but prohibits -any commercial uses. +any commercial use. For commercial use you need a Software Usage Agreement from AbsInt Angewandte Informatik GmbH. @@ -29,11 +29,14 @@ option) any later version: common/Errors.v common/Events.v common/Globalenvs.v + common/Linking.v common/Memdata.v common/Memory.v common/Memtype.v common/Smallstep.v + common/Subtyping.v common/Switch.v + common/Unityping.v common/Values.v cfrontend/Clight.v @@ -43,7 +46,8 @@ option) any later version: cfrontend/Cstrategy.v cfrontend/Csyntax.v cfrontend/Ctypes.v - + cfrontend/Ctyping.v + backend/Cminor.v backend/CMlexer.mli backend/CMlexer.mll @@ -51,6 +55,10 @@ option) any later version: backend/CMtypecheck.ml backend/CMtypecheck.mli + arm/Archi.v + ia32/Archi.v + powerpc/Archi.v + all files in the cparser/ directory all files in the exportclight/ directory |