Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit 457c7e6

Browse files
lembergerthlembergerth
committed
Get copyright info for combination tasks from original tasks
Instead of adding copyright info explicitly
1 parent 47c831b commit 457c7e6

File tree

212 files changed

+2378
-1896
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

212 files changed

+2378
-1896
lines changed

‎c/combinations/Makefile‎

Lines changed: 0 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -14,10 +14,5 @@ CLANG_WARNINGS := \
1414

1515
include $(LEVEL)/Makefile.config
1616

17-
license-pals:
18-
reuse addheader --template header.jinja2 --copyright "The SV-Benchmarks Community" --year 2014-2020 --license Apache-2.0 pals_lcr.*c
19-
reuse addheader --template header.jinja2 --copyright "Carnegie Mellon University" --year 2013 --license "LicenseRef-BSD-3-Clause-Attribution-CMU" pals_lcr.*c
20-
reuse addheader --template header.jinja2 --copyright "The RERS Challenge <https://www.rers-challenge.org>" --year 2012 pals_lcr.*c
21-
2217
tasks:
2318
./generate-tasks.py --benchmark-dir ../../ --output-dir ./

‎c/combinations/generate-tasks.py‎

Lines changed: 68 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@
1313
from pathlib import Path
1414
import yaml
1515
import sys
16+
import re
1617

1718

1819
class TaskError(Exception):
@@ -53,6 +54,21 @@ def _get_verdict(yml_task_def):
5354
raise TaskError()
5455

5556

57+
def _remove_all_copyright_comments(content):
58+
filtered_content = list()
59+
delimiter = "\n"
60+
for line in content.split(delimiter):
61+
if _is_singleline_comment(line) and (
62+
"This file is part of" in line
63+
or "sv-benchmarks" in line
64+
or "SPDX" in line
65+
or line.strip() == "//"
66+
):
67+
continue
68+
filtered_content.append(line)
69+
return delimiter.join(filtered_content)
70+
71+
5672
def _create_combo(
5773
file1: Path, file2: Path, replacement1=None, replacement2=None
5874
) -> str:
@@ -85,7 +101,7 @@ def _create_combo(
85101
extern void exit(int);
86102
"""
87103

88-
return (
104+
content = (
89105
additional_defs
90106
+ content1
91107
+ content2
@@ -98,6 +114,9 @@ def _create_combo(
98114
}"""
99115
)
100116

117+
# remove comments to avoid duplicate SPDX and copyright info
118+
return _remove_all_copyright_comments(content)
119+
101120

102121
def _get_yml_content(verdict1, verdict2, input_file: str, data_model="ILP32"):
103122
verdict = verdict1 == verdict2 == True
@@ -115,6 +134,53 @@ def _get_yml_content(verdict1, verdict2, input_file: str, data_model="ILP32"):
115134
"""
116135

117136

137+
def _spdx_info_to_text(spdx_info):
138+
def to_comment(key, value):
139+
return f"// {key}: {value}"
140+
141+
content = ""
142+
for idx, item in enumerate(sorted(spdx_info.items())):
143+
key, values = item
144+
if idx > 0:
145+
content += "//\n" # add one empty line to separate different keys
146+
text_for_single_key = "\n".join((to_comment(key, v) for v in sorted(values)))
147+
content += text_for_single_key + "\n"
148+
return content
149+
150+
151+
def _is_singleline_comment(line):
152+
return line.strip().startswith("//")
153+
154+
155+
def _get_spdx_header(*files):
156+
"""Parse all given files for SPDX-metadata and return a header that contains all of that combined information."""
157+
158+
def _try_extract_spdx(line):
159+
if not (_is_singleline_comment(line) and "SPDX" in line):
160+
return None, None
161+
try:
162+
matches = re.search(r"(SPDX-[a-zA-Z\-]+):\s*(.+)", line)
163+
return matches.group(1), matches.group(2)
164+
except (IndexError, AttributeError):
165+
# search didn't work
166+
return None, None
167+
168+
all_spdx_info = dict()
169+
for f in files:
170+
with open(f) as inp:
171+
for line in inp.readlines():
172+
key, value = _try_extract_spdx(line)
173+
if key:
174+
if key not in all_spdx_info:
175+
all_spdx_info[key] = set()
176+
all_spdx_info[key].add(value)
177+
178+
return f"""// This file is part of the SV-Benchmarks collection of verification tasks:
179+
// https://github.com/sosy-lab/sv-benchmarks
180+
//
181+
{_spdx_info_to_text(all_spdx_info)}"""
182+
183+
118184
def create_combos(
119185
pattern1, pattern2, replacement1=None, replacement2=None, output_dir=None
120186
):
@@ -132,6 +198,7 @@ def create_combos(
132198
basename = file1.name[:-2] + "+" + file2.name
133199
c_file = output_dir / Path(basename)
134200
c_content = _create_combo(file1, file2, replacement1, replacement2)
201+
c_content = _get_spdx_header(file1, file2) + "\n" + c_content
135202
yml_content = _get_yml_content(verdict1, verdict2, c_file.name)
136203
yml_file = output_dir / Path(basename[:-2] + ".yml")
137204

‎c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label01.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.BOUNDED-6.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -294,6 +295,7 @@ void assert(_Bool arg )
294295
}
295296
}
296297
}
298+
297299
int calculate_output(int);
298300
int calculate_output2(int);
299301
int calculate_output3(int);

‎c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label02.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.BOUNDED-6.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -294,6 +295,7 @@ void assert(_Bool arg )
294295
}
295296
}
296297
}
298+
297299
int calculate_output(int);
298300
int calculate_output2(int);
299301
int calculate_output3(int);

‎c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label04.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.BOUNDED-6.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -294,6 +295,7 @@ void assert(_Bool arg )
294295
}
295296
}
296297
}
298+
297299
int calculate_output(int);
298300
int calculate_output2(int);
299301
int calculate_output3(int);

‎c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label05.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.BOUNDED-6.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -294,6 +295,7 @@ void assert(_Bool arg )
294295
}
295296
}
296297
}
298+
297299
int calculate_output(int);
298300
int calculate_output2(int);
299301
int calculate_output3(int);

‎c/combinations/pals_lcr.3.1.ufo.BOUNDED-6.pals+Problem12_label09.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.BOUNDED-6.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -294,6 +295,7 @@ void assert(_Bool arg )
294295
}
295296
}
296297
}
298+
297299
int calculate_output(int);
298300
int calculate_output2(int);
299301
int calculate_output3(int);

‎c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label01.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.UNBOUNDED.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -299,6 +300,7 @@ void assert(_Bool arg )
299300
}
300301
}
301302
}
303+
302304
int calculate_output(int);
303305
int calculate_output2(int);
304306
int calculate_output3(int);

‎c/combinations/pals_lcr.3.1.ufo.UNBOUNDED.pals+Problem12_label02.c‎

Lines changed: 11 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,13 @@
1+
// This file is part of the SV-Benchmarks collection of verification tasks:
2+
// https://github.com/sosy-lab/sv-benchmarks
3+
//
4+
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
5+
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
6+
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
7+
//
8+
// SPDX-License-Identifier: Apache-2.0
9+
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
10+
111
extern unsigned int __VERIFIER_nondet_uint();
212
extern char __VERIFIER_nondet_char();
313
extern int __VERIFIER_nondet_int();
@@ -9,15 +19,6 @@ extern void abort(void);
919
extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
1020
void reach_error() { __assert_fail("0", "pals_lcr.3.1.ufo.UNBOUNDED.pals.c", 3, "reach_error"); }
1121

12-
// This file is part of the SV-Benchmarks collection of verification tasks:
13-
// https://github.com/sosy-lab/sv-benchmarks
14-
//
15-
// SPDX-FileCopyrightText: 2012 The RERS Challenge <https://www.rers-challenge.org>
16-
// SPDX-FileCopyrightText: 2013 Carnegie Mellon University
17-
// SPDX-FileCopyrightText: 2014-2020 The SV-Benchmarks Community
18-
//
19-
// SPDX-License-Identifier: Apache-2.0
20-
// SPDX-License-Identifier: LicenseRef-BSD-3-Clause-Attribution-CMU
2122

2223
/* Generated by CIL v. 1.6.0 */
2324
/* print_CIL_Input is true */
@@ -299,6 +300,7 @@ void assert(_Bool arg )
299300
}
300301
}
301302
}
303+
302304
int calculate_output(int);
303305
int calculate_output2(int);
304306
int calculate_output3(int);

0 commit comments

Comments
 (0)