aboutsummaryrefslogtreecommitdiffstats
path: root/LICENSE
diff options
context:
space:
mode:
Diffstat (limited to 'LICENSE')
-rw-r--r--LICENSE21
1 files changed, 14 insertions, 7 deletions
diff --git a/LICENSE b/LICENSE
index 21670791..5ffb39ab 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,14 +1,21 @@
All files in this distribution are part of the CompCert verified compiler.
-The CompCert verified compiler is Copyright 2004, 2005, 2006, 2007,
-2008, 2009, 2010, 2011, 2012, 2013, 2014, 2015 Institut National de
-Recherche en Informatique et en Automatique (INRIA).
+The CompCert verified compiler is Copyright by Institut National de
+Recherche en Informatique et en Automatique (INRIA) and
+AbsInt Angewandte Informatik GmbH.
The CompCert verified compiler is distributed under the terms of the
-INRIA Non-Commercial License Agreement given below. This 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 commercial uses.
+INRIA Non-Commercial License Agreement given below or under the terms
+of a Software Usage Agreement of AbsInt Angewandte Informatik GmbH.
+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.
+
+For commercial use you need a Software Usage Agreement from
+AbsInt Angewandte Informatik GmbH.
The following files in this distribution are dual-licensed both under
the INRIA Non-Commercial License Agreement and under the Free Software