1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334
|
Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/
Upstream-Name: frama-c
Source: http://frama-c.cea.fr/download.html
Upstream-Contact: Software Reliability Laboratory (LSL) and INRIA ProVal project
Files: *
Copyright: © 2007-2017 CEA (Commissariat à l'Énergie Atomique)
© 2007-2017 INRIA (Institut National de Recherche en Informatique
et Automatique)
© 2007-2017 INSA (Institut National des Sciences Appliquees)
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: debian/*
Copyright: © 2008-2017 Mehdi Dogguy <mehdi@debian.org>
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: **/configure*
Copyright: © 1992-1996, 1998-2012 Free Software Foundation, Inc.
License: MIT-like
This configure script is free software; the Free Software Foundation
gives unlimited permission to copy, distribute and modify it.
Files: src/plugins/e-acsl/share/e-acsl/e_acsl_printf.h
Copyright: © 2004,2012 Kustaa Nyholm / SpareTimeLabs
License: BSD-3-clause
Files: src/plugins/wp/share/coqwp/BuiltIn.v
src/plugins/wp/share/coqwp/bool/Bool.v
src/plugins/wp/share/coqwp/int/Abs.v
src/plugins/wp/share/coqwp/int/ComputerDivision.v
src/plugins/wp/share/coqwp/int/Int.v
src/plugins/wp/share/coqwp/int/MinMax.v
src/plugins/wp/share/coqwp/map/Map.v
src/plugins/wp/share/coqwp/real/Abs.v
src/plugins/wp/share/coqwp/real/FromInt.v
src/plugins/wp/share/coqwp/real/MinMax.v
src/plugins/wp/share/coqwp/real/Real.v
src/plugins/wp/share/coqwp/real/RealInfix.v
src/plugins/wp/share/coqwp/real/Square.v
src/plugins/wp/share/ergo/bool.Bool.mlw
src/plugins/wp/share/ergo/int.Abs.mlw
src/plugins/wp/share/ergo/int.ComputerDivision.mlw
src/plugins/wp/share/ergo/int.Int.mlw
src/plugins/wp/share/ergo/int.MinMax.mlw
src/plugins/wp/share/ergo/map.Map.mlw
src/plugins/wp/share/ergo/real.Abs.mlw
src/plugins/wp/share/ergo/real.FromInt.mlw
src/plugins/wp/share/ergo/real.MinMax.mlw
src/plugins/wp/share/ergo/real.Real.mlw
src/plugins/wp/share/ergo/real.RealInfix.mlw
src/plugins/wp/share/ergo/real.Square.mlw
src/plugins/wp/why3_xml.mli
src/plugins/wp/why3_xml.mll
Copyright: © 2010-2013 INRIA - CNRS - Paris-Sud University
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: src/kernel_internals/parsing/clexer.mli
src/kernel_internals/parsing/clexer.mll
src/kernel_internals/parsing/cparser.mly
src/kernel_internals/parsing/errorloc.ml
src/kernel_internals/parsing/errorloc.mli
src/kernel_internals/parsing/lexerhack.ml
src/kernel_internals/runtime/machdeps.ml
src/kernel_internals/runtime/machdeps.mli
src/kernel_internals/typing/alpha.ml
src/kernel_internals/typing/alpha.mli
src/kernel_internals/typing/cabs2cil.ml
src/kernel_internals/typing/cabs2cil.mli
src/kernel_internals/typing/cfg.ml
src/kernel_internals/typing/cfg.mli
src/kernel_internals/typing/frontc.ml
src/kernel_internals/typing/frontc.mli
src/kernel_internals/typing/mergecil.ml
src/kernel_internals/typing/mergecil.mli
src/kernel_internals/typing/oneret.ml
src/kernel_internals/typing/oneret.mli
src/kernel_internals/typing/rmtmps.ml
src/kernel_internals/typing/rmtmps.mli
src/kernel_services/analysis/dataflow.ml
src/kernel_services/analysis/dataflow.mli
src/kernel_services/analysis/dataflows.ml
src/kernel_services/analysis/dataflows.mli
src/kernel_services/ast_data/cil_types.mli
src/kernel_services/ast_printing/cprint.ml
src/kernel_services/ast_printing/cprint.mli
src/kernel_services/ast_queries/cil.ml
src/kernel_services/ast_queries/cil.mli
src/kernel_services/ast_queries/cil_const.ml
src/kernel_services/ast_queries/cil_const.mli
src/kernel_services/parsetree/cabs.ml
src/kernel_services/parsetree/cabshelper.ml
src/kernel_services/parsetree/cabshelper.mli
src/kernel_services/visitors/cabsvisit.ml
src/kernel_services/visitors/cabsvisit.mli
src/libraries/utils/cilconfig.ml
src/libraries/utils/cilconfig.mli
src/libraries/utils/escape.ml
src/libraries/utils/escape.mli
share/machdep.c
Copyright: © 2001-2003 George C. Necula <necula@cs.berkeley.edu>
© 2001-2003 Scott McPeak <smcpeak@cs.berkeley.edu>
© 2001-2003 Wes Weimer <weimer@cs.berkeley.edu>
© 2001-2003 Ben Liblit <liblit@cs.berkeley.edu>
License: BSD-3-clause
Files: src/libraries/utils/rangemap.ml
src/libraries/utils/rangemap.mli
Copyright:
© 1996 Institut National de Recherche en Informatique et en Automatique
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: src/aorai/*
Copyright: © 2007-2011 INSA (Institut National des Sciences Appliquees)
© 2007-2011 INRIA (Institut National de Recherche en Informatique
et en Automatique)
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: tests/minix/*
Copyright: © 1987, 1997, 2006, Vrije Universiteit, Amsterdam, The Netherlands
License: BSD-3-clause
Files: tests/spec/purse.c
Copyright: © 2002-2006 Jean-François COUCHOT
© 2002-2006 Mehdi DOGGUY
© 2002-2006 Jean-Christophe FILLIÂTRE
© 2002-2006 Thierry HUBERT
© 2002-2006 Claude MARCHÉ
© 2002-2006 Yannick MOY
License: GPL-2
See `/usr/share/common-licenses/GPL-2'.
Files: share/emacs/acsl.el
Copyright: © 2008-2011 Pierre ROUX
© 2009-2017 CEA LIST
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: tests/bugs/evoting.c
Copyright: © 2004-2009 David MENTRE
License: GPL-3
See `/usr/share/common-licenses/GPL-3'.
Files: share/libc/netinet/tcp.h
Copyright: © 2007-2017 CEA (Commissariat à l'énergie atomique et aux énergies
alternatives)
© 1982, 1986, 1993 The Regents of the University of California.
License: LGPL-2.1
See `/usr/share/common-licenses/LGPL-2.1'.
Files: tests/idct/*
Copyright: © 2001 Renaud Pacalet
License: GPL-2+
See `/usr/share/common-licenses/GPL-2'.
Files: src/libraries/utils/hptmap.ml
src/libraries/utils/hptmap.mli
Copyright: © 2005 Institut National de Recherche en Informatique et en
Automatique
License: QPL-modified
See `./licenses/Q_MODIFIED_LICENSE`.
License: QPL-modified
In the following, "the Library" refers to the following file:
.
standard.mly
.
and "the Generator" refers to all files marked "Copyright INRIA" in the
root directory.
.
The Generator is distributed under the terms of the Q Public License
version 1.0 with a change to choice of law (included below).
.
The Library is distributed under the terms of the GNU Library General
Public License version 2. On a Debian system, this license can be found
in the file `/usr/share/common-licenses/LGPL-2.1` .
.
As a special exception to the Q Public Licence, you may develop
application programs, reusable components and other software items
that link with the original or modified versions of the Generator
and are not made available to the general public, without any of the
additional requirements listed in clause 6c of the Q Public licence.
.
As a special exception to the GNU Library General Public License, you
may link, statically or dynamically, a "work that uses the Library"
with a publicly distributed version of the Library to produce an
executable file containing portions of the Library, and distribute
that executable file under terms of your choice, without any of the
additional requirements listed in clause 6 of the GNU Library General
Public License. By "a publicly distributed version of the Library",
we mean either the unmodified Library as distributed by INRIA, or a
modified version of the Library that is distributed under the
conditions defined in clause 3 of the GNU Library General Public
License. This exception does not however invalidate any other reasons
why the executable file might be covered by the GNU Library General
Public License.
.
THE Q PUBLIC LICENSE version 1.0
.
Copyright (C) 1999 Troll Tech AS, Norway.
Everyone is permitted to copy and
distribute this license document.
.
The intent of this license is to establish freedom to share and change
the software regulated by this license under the open source model.
.
This license applies to any software containing a notice placed by the
copyright holder saying that it may be distributed under the terms of
the Q Public License version 1.0. Such software is herein referred to
as the Software. This license covers modification and distribution of
the Software, use of third-party application programs based on the
Software, and development of free software which uses the Software.
.
Granted Rights
.
1. You are granted the non-exclusive rights set forth in this license
provided you agree to and comply with any and all conditions in this
license. Whole or partial distribution of the Software, or software
items that link with the Software, in any form signifies acceptance of
this license.
.
2. You may copy and distribute the Software in unmodified form
provided that the entire package, including - but not restricted to -
copyright, trademark notices and disclaimers, as released by the
initial developer of the Software, is distributed.
.
3. You may make modifications to the Software and distribute your
modifications, in a form that is separate from the Software, such as
patches. The following restrictions apply to modifications:
.
a. Modifications must not alter or remove any copyright notices
in the Software.
.
b. When modifications to the Software are released under this
license, a non-exclusive royalty-free right is granted to the
initial developer of the Software to distribute your
modification in future versions of the Software provided such
versions remain available under these terms in addition to any
other license(s) of the initial developer.
.
4. You may distribute machine-executable forms of the Software or
machine-executable forms of modified versions of the Software,
provided that you meet these restrictions:
.
a. You must include this license document in the distribution.
.
b. You must ensure that all recipients of the machine-executable
forms are also able to receive the complete machine-readable
source code to the distributed Software, including all
modifications, without any charge beyond the costs of data
transfer, and place prominent notices in the distribution
explaining this.
.
c. You must ensure that all modifications included in the
machine-executable forms are available under the terms of this
license.
.
5. You may use the original or modified versions of the Software to
compile, link and run application programs legally developed by you or
by others.
.
6. You may develop application programs, reusable components and other
software items that link with the original or modified versions of the
Software. These items, when distributed, are subject to the following
requirements:
.
a. You must ensure that all recipients of machine-executable
forms of these items are also able to receive and use the
complete machine-readable source code to the items without any
charge beyond the costs of data transfer.
.
b. You must explicitly license all recipients of your items to
use and re-distribute original and modified versions of the
items in both machine-executable and source code forms. The
recipients must be able to do so without any charges whatsoever,
and they must be able to re-distribute to anyone they choose.
.
c. If the items are not available to the general public, and the
initial developer of the Software requests a copy of the items,
then you must supply one.
.
Limitations of Liability
.
In no event shall the initial developers or copyright holders be
liable for any damages whatsoever, including - but not restricted to -
lost revenue or profits or other direct, indirect, special, incidental
or consequential damages, even if they have been advised of the
possibility of such damages, except to the extent invariable law, if
any, provides otherwise.
.
No Warranty
.
The Software and this license document are provided AS IS with NO
WARRANTY OF ANY KIND, INCLUDING THE WARRANTY OF DESIGN,
MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE.
.
Choice of Law
.
This license is governed by the Laws of France.
License: BSD-3-clause
All rights reserved.
.
Redistribution and use in source and binary forms, with or without
modification, are permitted provided that the following conditions
are met:
.
Redistributions of source code must retain the above copyright
notice, this list of conditions and the following disclaimer.
.
Redistributions in binary form must reproduce the above copyright
notice, this list of conditions and the following disclaimer in the
documentation and/or other materials provided with the distribution.
.
Neither the name of the Kustaa Nyholm or SpareTimeLabs nor the names
of its contributors may be used to endorse or promote products derived
from this software without specific prior written permission.
.
THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
|