Discussion:
The license of runtime/klee-libc
Jonathan Neuschäfer
2013-06-25 14:01:09 UTC
Permalink
Hello,

the top-level LICENSE.TXT file states:

The klee software contains code written by third parties. Such software will
have its own individual LICENSE.TXT file in the directory in which it appears.
This file will describe the copyrights, license, and restrictions which apply
to that code.

The disclaimer of warranty in the University of Illinois Open Source License
applies to all code in the klee Distribution, and nothing in any of the other
licenses gives permission to use the names of the klee Team or Stanford
University to endorse or promote products derived from this Software.

The following pieces of software have additional or alternate copyrights,
licenses, and/or restrictions:

Program Directory
------- ---------
klee-libc runtime/klee-libc

Yet, runtime/klee-libc doesn't contain a LICENSE.TXT file.

The following files in this directory don't have the standard KLEE
license comment:

FILE COMPLEXITY AUTHOR
atoi.c: trivial Berkeley
memchr.c: trivial Chris Torek / Berkeley
memcmp.c: trivial Chris Torek / Berkeley
stpcpy.c: trivial David E. O'Brien / Berkeley
strcat.c: trivial Berkeley
strncmp.c: trivial Berkeley
strncpy.c: trivial Chris Torek / Berkeley
strtol.c: non-trivial Berkeley
strtoul.c: non-trivial Berkeley

I propose:
- either adding a LICENSE.TXT file to runtime/klee-libc,
- or replacing the above files with files that may carry the KLEE
license comment.

Please let me know what you think.


Thanks,
Joanthan Neuschäefer
Daniel Dunbar
2013-06-25 23:01:40 UTC
Permalink
Hi Jonathan,

Where did you derive the author information from?

If you can verify that the implementations we have are from a particular
source then we should probably import their license. If we can't verify the
right source license, then my recommendation would be to try and find BSD
licensed ones we could import (and include license, if need be).

- Daniel


On Tue, Jun 25, 2013 at 7:01 AM, Jonathan Neuschäfer
Post by Jonathan Neuschäfer
Hello,
The klee software contains code written by third parties. Such software will
have its own individual LICENSE.TXT file in the directory in which it appears.
This file will describe the copyrights, license, and restrictions which apply
to that code.
The disclaimer of warranty in the University of Illinois Open Source License
applies to all code in the klee Distribution, and nothing in any of the other
licenses gives permission to use the names of the klee Team or Stanford
University to endorse or promote products derived from this Software.
The following pieces of software have additional or alternate copyrights,
Program Directory
------- ---------
klee-libc runtime/klee-libc
Yet, runtime/klee-libc doesn't contain a LICENSE.TXT file.
The following files in this directory don't have the standard KLEE
FILE COMPLEXITY AUTHOR
atoi.c: trivial Berkeley
memchr.c: trivial Chris Torek / Berkeley
memcmp.c: trivial Chris Torek / Berkeley
stpcpy.c: trivial David E. O'Brien / Berkeley
strcat.c: trivial Berkeley
strncmp.c: trivial Berkeley
strncpy.c: trivial Chris Torek / Berkeley
strtol.c: non-trivial Berkeley
strtoul.c: non-trivial Berkeley
- either adding a LICENSE.TXT file to runtime/klee-libc,
- or replacing the above files with files that may carry the KLEE
license comment.
Please let me know what you think.
Thanks,
Joanthan Neuschäefer
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Jonathan Neuschäfer
2013-06-25 23:56:17 UTC
Permalink
Post by Daniel Dunbar
Hi Jonathan,
Where did you derive the author information from?
If you can verify that the implementations we have are from a particular
source then we should probably import their license. If we can't verify the
right source license, then my recommendation would be to try and find BSD
licensed ones we could import (and include license, if need be).
I took the authorship information from the license comments in these
files. They are all under the 4-clause BSD license, which is quite
problematic for its advertising clause:

"3. All advertising materials mentioning features or use of this
software must display the following acknowledgement: This product
includes software developed by the University of California,
Berkeley and its contributors."

The NetBSD libc seems to suite our purpose, it's 2- or 3-clause BSD
licensed: ftp://ftp.netbsd.org/pub/NetBSD/NetBSD-current/src/lib/libc/
I haven't reviewed the code in question yet, though.


Thanks,
Jonathan
Cristian Cadar
2013-06-26 14:44:09 UTC
Permalink
Thanks for the detailed info, Jonathan.

I agree that we could replace klee-libc with other code, but first of
all, I am wondering whether we still need it in the first place. My
impression is that everyone uses klee either standalone or with uclibc,
but please let me know if there are any users who need the "--libc=klee"
option.

Unless I hear otherwise, my suggestion would be to remove that directory
from the mainline, and perhaps just offer it as a separate external
library, as we do with uclibc.

Best,
Cristian
Post by Jonathan Neuschäfer
Post by Daniel Dunbar
Hi Jonathan,
Where did you derive the author information from?
If you can verify that the implementations we have are from a particular
source then we should probably import their license. If we can't verify the
right source license, then my recommendation would be to try and find BSD
licensed ones we could import (and include license, if need be).
I took the authorship information from the license comments in these
files. They are all under the 4-clause BSD license, which is quite
"3. All advertising materials mentioning features or use of this
software must display the following acknowledgement: This product
includes software developed by the University of California,
Berkeley and its contributors."
The NetBSD libc seems to suite our purpose, it's 2- or 3-clause BSD
licensed: ftp://ftp.netbsd.org/pub/NetBSD/NetBSD-current/src/lib/libc/
I haven't reviewed the code in question yet, though.
Thanks,
Jonathan
_______________________________________________
klee-dev mailing list
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
Jonathan Neuschäfer
2013-06-26 22:28:05 UTC
Permalink
Post by Cristian Cadar
Thanks for the detailed info, Jonathan.
I agree that we could replace klee-libc with other code, but first
of all, I am wondering whether we still need it in the first place.
My impression is that everyone uses klee either standalone or with
uclibc, but please let me know if there are any users who need the
"--libc=klee" option.
Good point; I can say almost nothing about KLEE's user base.
Post by Cristian Cadar
Unless I hear otherwise, my suggestion would be to remove that
directory from the mainline, and perhaps just offer it as a separate
external library, as we do with uclibc.
Preferably with a SVN (or Git) repo, but that's just a humble wish of
mine. :-)


Jonathan
Post by Cristian Cadar
Best,
Cristian
Post by Jonathan Neuschäfer
Post by Daniel Dunbar
Hi Jonathan,
Where did you derive the author information from?
If you can verify that the implementations we have are from a particular
source then we should probably import their license. If we can't verify the
right source license, then my recommendation would be to try and find BSD
licensed ones we could import (and include license, if need be).
I took the authorship information from the license comments in these
files. They are all under the 4-clause BSD license, which is quite
"3. All advertising materials mentioning features or use of this
software must display the following acknowledgement: This product
includes software developed by the University of California,
Berkeley and its contributors."
The NetBSD libc seems to suite our purpose, it's 2- or 3-clause BSD
licensed: ftp://ftp.netbsd.org/pub/NetBSD/NetBSD-current/src/lib/libc/
I haven't reviewed the code in question yet, though.
Thanks,
Jonathan
Loading...