diff options
Diffstat (limited to 'LICENSE')
| -rw-r--r-- | LICENSE | 59 |
1 files changed, 37 insertions, 22 deletions
@@ -15,30 +15,41 @@ the INRIA Non-Commercial License Agreement and under the Free Software Foundation GNU General Public License, either version 2 or (at your option) any later version: - backend/Cminor.v common/AST.v - backend/CMlexer.mli common/Errors.v - backend/CMlexer.mll common/Events.v - backend/CMparser.mly common/Globalenvs.v - backend/CMtypecheck.ml common/Mem.v - backend/CMtypecheck.mli common/Smallstep.v - cfrontend/C2C.ml common/Switch.v - cfrontend/Cop.v common/Values.v - cfrontend/Ctypes.v lib/Coqlib.v - cfrontend/Csem.v lib/Floats.v - cfrontend/Csyntax.v lib/Integers.v - cfrontend/Cstrategy.v lib/Maps.v - cfrontend/Clight.v lib/Parmov.v - cfrontend/PrintCsyntax.ml lib/Camlcoq.ml - cfrontend/PrintClight.ml - exportclight/Clightdefs.v - exportclight/ExportClight.ml - - all files in the runtime/ directory - all files in the cparser/ directory + all files in the lib/ directory + + common/AST.v + common/Behaviors.v + common/Errors.v + common/Events.v + common/Globalenvs.v + common/Memdata.v + common/Memory.v + common/Memtype.v + common/Smallstep.v + common/Switch.v + common/Values.v + + cfrontend/Clight.v + cfrontend/ClightBigstep.v + cfrontend/Cop.v + cfrontend/Csem.v + cfrontend/Cstrategy.v + cfrontend/Csyntax.v + cfrontend/Ctypes.v + + backend/Cminor.v + backend/CMlexer.mli + backend/CMlexer.mll + backend/CMparser.mly + backend/CMtypecheck.ml + backend/CMtypecheck.mli + + all files in the cparser/ directory (except those listed below which are under a BSD license) -A copy of the GNU General Public License version 2 is included below. + all files in the exportclight/ directory +A copy of the GNU General Public License version 2 is included below. The choice between the two licenses for the files listed above is left to the user. If you opt for the GNU General Public License, these files are free software and can be used both in commercial and @@ -52,6 +63,10 @@ terms of the GNU Lesser General Public Licence, either version 3 of the licence, or (at your option) any later version. A copy of the GNU Lesser General Public Licence version 3 is included below. +The files contained in the runtime/ directory and its subdirectories +are Copyright 2013 INRIA and distributed under the terms of the BSD +license, included below. + Finally, the following files are taken from the CIL library: cparser/Cabs.ml cparser/Lexer.mli @@ -496,7 +511,7 @@ Public License instead of this License. ---------------------------------------------------------------------- - BSD License for the CIL library + BSD License Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met: |