Define and check license requirements

[PhilippWendler]

We should discuss what licenses are acceptable for benchmarks, i.e., what kind of rights to we need to be granted in the license.

I would list at least the following requirements:

• use the files
• change the files (e.g., preprocessing, when we find a bug, or change some __VERIFIER_* specifics)
• redistribute, both original and changed
• do all of this commercially (we don't want to prevent authors of commercial tools to do this)

When this is answered, it should also be added to the documentation.

Furthermore, we should check for all existing directories whether their license grants the necessary rights:

• array-examples
• array-industry-pattern
• array-memsafety
• bitvector
• bitvector-loops
• bitvector-regression
• busybox-1.22.0
• ddv-machzwd
• eca-rers2012
• float-benchs
• floats-cbmc-regression
• floats-cdfpl
• floats-esbmc-regression
• forester-heap
• heap-manipulation
• ldv-challenges
• ldv-commit-tester
• ldv-consumption
• ldv-linux-3.0
• ldv-linux-3.12-rc1
• ldv-linux-3.14
• ldv-linux-3.16-rc1
• ldv-linux-3.4-simple
• ldv-linux-3.7.3
• ldv-linux-4.0-rc1-mav
• ldv-linux-4.2-rc1
• ldv-memsafety
• ldv-memsafety-bitfields
• ldv-multiproperty
• ldv-races
• ldv-regression
• ldv-validator-v0.6
• ldv-validator-v0.8
• list-ext-properties
• list-properties
• locks
• loop-acceleration
• loop-industry-pattern
• loop-invgen
• loop-lit
• loop-new
• loops
• memory-alloca
• memsafety
• memsafety-ext
• ntdrivers
• ntdrivers-simplified
• product-lines
• psyco
• pthread
• pthread-atomic
• pthread-ext
• pthread-lit
• pthread-wmm
• recursive
• recursive-simple
• reducercommutativity
• seq-mthreaded
• seq-pthread
• signedintegeroverflow-regression
• ssh
• ssh-simplified
• systemc
• termination-15
• termination-crafted
• termination-crafted-lit
• termination-libowfat
• termination-memory-alloca
• termination-numeric
• termination-recursive-malloc
• termination-restricted-15

[dbeyer]

Requirements added to description.

[tautschnig]

@PhilippWendler What is the procedure here? I would be happy to contribute the information for the missing float-* (BSD license), but I don't know how to take action.

[PhilippWendler]

@tautschnig Just add a PR with a LICENSE.txt in the respective directories.

[tautschnig]

ce25410 of #239 adds license files for floats-cbmc-regression, floats-cdfpl, pthread-wmm (and busybox, but that wasn't essential).

[tautschnig]

Those license fixes have now been moved into #243.

[MartinSpiessl]

What is the status of this issue? Is there still help wanted? Probably we need to update the list with folders that were added in the meanwhile, though those should not be a problem since we always look for a README and a LICENSE in the PRs.

[PhilippWendler]

Yes, help would still be great. The list above should be correct, the most important point would be to contact original submitters of those directories that are not checked above.

I recently did #1098 and also have some info on pthread tasks for which I will create a PR soon.

[MartinSpiessl]

@dopelsunce you added the Apache 2.0 license to eca-programs in 040cc22, where in the README it claims that these were derived from the RERS 2012 tasks. Do you know that the RERS 2012 tasks are under Apache 2.0 license or does this just refer to your changes? You added this license also to the eca-rers2012 folder, which would indicate that you were able to determine the license for them. If so, we could tick eca-rers2012 off the list in this issue

[PhilippWendler]

@MartinSpiessl The license of eca-programs and eca-rers2020 were actually added in 8693853 (#601) and we have confirmation from Bernhard Steffen that Apache 2.0 is correct. So we can indeed tick eca-rers2020.

040cc22 seems to contain lots of content from other branches that should not have been part of it, probably because of a merge commit was incorrectly squashed together with other commits (#584 (comment)). The diff of #584 shows what was actually added.