Add spdx licenses to seq-mthreaded

[lembergerth]

Replace full copyright header with SPDX licenses in tasks seq-mthreaded/.

[lembergerth]

Previous feedback by @PhilippWendler :

seq_mthreaded tasks are copyrighted and licensed by CMU, but as you already mentioned, it is not clear from which systems these tasks were created from.
I did some internet search but couldn't find any information. Is it good enough to trust the contributors that the license is valid?

I would say this depends on how plausible it is that these programs were created from CMU sources alone. For example, if obviously identifiable references to other programs occur as sources in readmes, file names, program identifiers, or respective papers, then we should investigate more. If nothing of this exists, then I guess we can live with the risk.

I've checked README, files, the contributors webpage and the webpage of his chair for any information on the project.
I couldn't find any details and no publication that sounded like it was involved with the tasks.

It is probably also a good idea to list the SV-Benchmarks community as additional copyright holder, also for making it clear that the files were changed.

Yes, done. I didn't do this at first because I thought that small changes like __VERIFIER_error->reach_error are not enough to claim copyright, but I guess I was wrong?
I also think the second reason is fair to the original author - we should somehow note that some changes were done.

[holznerst]

@PhilippWendler could you please have a look at this PR, since you are already involved?

[PhilippWendler]

7df38be seems to change only ECA programs although the commit message and this PR is about seq-mthreaded. Could you please have a look?

[PhilippWendler]

Yes, done. I didn't do this at first because I thought that small changes like __VERIFIER_error->reach_error are not enough to claim copyright, but I guess I was wrong?

One can claim it for all kinds of changes, but it might just not mean anything if a court decides that there is not enough intellectual contribution. But it does not hurt and in this case there is the advantage of the notification about changes. This is not required by the existing license of these tasks, but nevertheless nice to the original authors, and some licenses actually do require this (cf. #1097), so it is good to do this in general.

[lembergerth]

7df38be seems to change only ECA programs although the commit message and this PR is about seq-mthreaded. Could you please have a look?

It actually changed both ECA and seq-mthreaded, thanks for noticing.
I guess Github didn't get to displaying the seq-mthreaded tasks.

I've force-pushed a commit that fixes this and only modifies the seq-mthreaded tasks.

[PhilippWendler]

Thanks, now this is easy to review.

Interesting that the license header is not at the start of the file (did the reuse tool create this?), but because reuse lint is fine with it, I am, too.

[lembergerth]

Interesting that the license header is not at the start of the file (did the reuse tool create this?)

Yes, the reuse tool did this. It seems to kind of parse the C program and put the license header after external declarations and includes.

This would explain why reuse addheader takes so long on the ECA-tasks.

Thanks for the review!

[PhilippWendler]

Yes, the reuse tool did this. It seems to kind of parse the C program and put the license header after external declarations and includes.

Just FYI: Almost. The reuse tool parses the files in order to find existing license and copyright declarations, and then it deletes existing license headers and merges all copyright information into the new header.