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

Commit a46e16f

Browse files
dbeyerdbeyer
authored
Merge pull request #1102 from lembergerth/property-merges-for-eca-rers2018
Add unreach-call prop to eca-rers2018
2 parents 481d682 + cf8d997 commit a46e16f

23 files changed

+1103
-917
lines changed

‎c/check.py‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@
3434
re.I)
3535
CONFIG_KEYS = set(["Architecture", "Description"])
3636
PROPERTIES = set(["def-behavior", "no-overflow", "no-data-race", "termination", "unreach-call", "valid-deref", "valid-free", "valid-memcleanup", "valid-memsafety", "valid-memtrack",
37-
"coverage-error-call", "coverage-branches", "coverage-conditions", "coverage-statements"])
37+
"coverage-error-call", "coverage-branches", "coverage-conditions", "coverage-statements", "unreach-call-a", "unreach-call-b"])
3838
# multiple properties for eca-rers2018-files
3939
for i in range(100):
4040
PROPERTIES.add("unreach-call-%d" % i)

‎c/eca-rers2018/Problem10.c‎

Lines changed: 114 additions & 101 deletions
Original file line numberDiff line numberDiff line change
@@ -1,104 +1,117 @@
11
extern int __VERIFIER_nondet_int();
2-
void reach_error_0(){}
3-
void reach_error_1(){}
4-
void reach_error_2(){}
5-
void reach_error_3(){}
6-
void reach_error_4(){}
7-
void reach_error_5(){}
8-
void reach_error_6(){}
9-
void reach_error_7(){}
10-
void reach_error_8(){}
11-
void reach_error_9(){}
12-
void reach_error_10(){}
13-
void reach_error_11(){}
14-
void reach_error_12(){}
15-
void reach_error_13(){}
16-
void reach_error_14(){}
17-
void reach_error_15(){}
18-
void reach_error_16(){}
19-
void reach_error_17(){}
20-
void reach_error_18(){}
21-
void reach_error_19(){}
22-
void reach_error_20(){}
23-
void reach_error_21(){}
24-
void reach_error_22(){}
25-
void reach_error_23(){}
26-
void reach_error_24(){}
27-
void reach_error_25(){}
28-
void reach_error_26(){}
29-
void reach_error_27(){}
30-
void reach_error_28(){}
31-
void reach_error_29(){}
32-
void reach_error_30(){}
33-
void reach_error_31(){}
34-
void reach_error_32(){}
35-
void reach_error_33(){}
36-
void reach_error_34(){}
37-
void reach_error_35(){}
38-
void reach_error_36(){}
39-
void reach_error_37(){}
40-
void reach_error_38(){}
41-
void reach_error_39(){}
42-
void reach_error_40(){}
43-
void reach_error_41(){}
44-
void reach_error_42(){}
45-
void reach_error_43(){}
46-
void reach_error_44(){}
47-
void reach_error_45(){}
48-
void reach_error_46(){}
49-
void reach_error_47(){}
50-
void reach_error_48(){}
51-
void reach_error_49(){}
52-
void reach_error_50(){}
53-
void reach_error_51(){}
54-
void reach_error_52(){}
55-
void reach_error_53(){}
56-
void reach_error_54(){}
57-
void reach_error_55(){}
58-
void reach_error_56(){}
59-
void reach_error_57(){}
60-
void reach_error_58(){}
61-
void reach_error_59(){}
62-
void reach_error_60(){}
63-
void reach_error_61(){}
64-
void reach_error_62(){}
65-
void reach_error_63(){}
66-
void reach_error_64(){}
67-
void reach_error_65(){}
68-
void reach_error_66(){}
69-
void reach_error_67(){}
70-
void reach_error_68(){}
71-
void reach_error_69(){}
72-
void reach_error_70(){}
73-
void reach_error_71(){}
74-
void reach_error_72(){}
75-
void reach_error_73(){}
76-
void reach_error_74(){}
77-
void reach_error_75(){}
78-
void reach_error_76(){}
79-
void reach_error_77(){}
80-
void reach_error_78(){}
81-
void reach_error_79(){}
82-
void reach_error_80(){}
83-
void reach_error_81(){}
84-
void reach_error_82(){}
85-
void reach_error_83(){}
86-
void reach_error_84(){}
87-
void reach_error_85(){}
88-
void reach_error_86(){}
89-
void reach_error_87(){}
90-
void reach_error_88(){}
91-
void reach_error_89(){}
92-
void reach_error_90(){}
93-
void reach_error_91(){}
94-
void reach_error_92(){}
95-
void reach_error_93(){}
96-
void reach_error_94(){}
97-
void reach_error_95(){}
98-
void reach_error_96(){}
99-
void reach_error_97(){}
100-
void reach_error_98(){}
101-
void reach_error_99(){}
2+
3+
extern void __assert_fail (const char *__assertion, const char *__file,
4+
unsigned int __line, const char *__function)
5+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
6+
extern void __assert_perror_fail (int __errnum, const char *__file,
7+
unsigned int __line, const char *__function)
8+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
9+
extern void __assert (const char *__assertion, const char *__file, int __line)
10+
__attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
11+
12+
void reach_error() { ((void) sizeof ((0) ? 1 : 0), __extension__ ({ if (0) ; else __assert_fail ("0", "Problem10.c", 3, __extension__ __PRETTY_FUNCTION__); })); }
13+
void reach_error_b(){ reach_error(); }
14+
void reach_error_a(){ reach_error(); }
15+
void reach_error_0(){ reach_error_a(); }
16+
void reach_error_1(){ reach_error_a(); }
17+
void reach_error_2(){ reach_error_a(); }
18+
void reach_error_3(){ reach_error_a(); }
19+
void reach_error_4(){ reach_error_b(); }
20+
void reach_error_5(){ reach_error_a(); }
21+
void reach_error_6(){ reach_error_b(); }
22+
void reach_error_7(){ reach_error_a(); }
23+
void reach_error_8(){ reach_error_a(); }
24+
void reach_error_9(){ reach_error_a(); }
25+
void reach_error_10(){ reach_error_a(); }
26+
void reach_error_11(){ reach_error_a(); }
27+
void reach_error_12(){ reach_error_a(); }
28+
void reach_error_13(){ reach_error_a(); }
29+
void reach_error_14(){ reach_error_a(); }
30+
void reach_error_15(){ reach_error_a(); }
31+
void reach_error_16(){ reach_error_a(); }
32+
void reach_error_17(){ reach_error_a(); }
33+
void reach_error_18(){ reach_error_b(); }
34+
void reach_error_19(){ reach_error_a(); }
35+
void reach_error_20(){ reach_error_a(); }
36+
void reach_error_21(){ reach_error_a(); }
37+
void reach_error_22(){ reach_error_a(); }
38+
void reach_error_23(){ reach_error_b(); }
39+
void reach_error_24(){ reach_error_a(); }
40+
void reach_error_25(){ reach_error_a(); }
41+
void reach_error_26(){ reach_error_a(); }
42+
void reach_error_27(){ reach_error_b(); }
43+
void reach_error_28(){ reach_error_a(); }
44+
void reach_error_29(){ reach_error_a(); }
45+
void reach_error_30(){ reach_error_a(); }
46+
void reach_error_31(){ reach_error_b(); }
47+
void reach_error_32(){ reach_error_a(); }
48+
void reach_error_33(){ reach_error_a(); }
49+
void reach_error_34(){ reach_error_a(); }
50+
void reach_error_35(){ reach_error_a(); }
51+
void reach_error_36(){ reach_error_a(); }
52+
void reach_error_37(){ reach_error_a(); }
53+
void reach_error_38(){ reach_error_b(); }
54+
void reach_error_39(){ reach_error_a(); }
55+
void reach_error_40(){ reach_error_a(); }
56+
void reach_error_41(){ reach_error_a(); }
57+
void reach_error_42(){ reach_error_a(); }
58+
void reach_error_43(){ reach_error_a(); }
59+
void reach_error_44(){ reach_error_a(); }
60+
void reach_error_45(){ reach_error_a(); }
61+
void reach_error_46(){ reach_error_a(); }
62+
void reach_error_47(){ reach_error_a(); }
63+
void reach_error_48(){ reach_error_a(); }
64+
void reach_error_49(){ reach_error_a(); }
65+
void reach_error_50(){ reach_error_a(); }
66+
void reach_error_51(){ reach_error_a(); }
67+
void reach_error_52(){ reach_error_a(); }
68+
void reach_error_53(){ reach_error_a(); }
69+
void reach_error_54(){ reach_error_a(); }
70+
void reach_error_55(){ reach_error_a(); }
71+
void reach_error_56(){ reach_error_a(); }
72+
void reach_error_57(){ reach_error_a(); }
73+
void reach_error_58(){ reach_error_b(); }
74+
void reach_error_59(){ reach_error_a(); }
75+
void reach_error_60(){ reach_error_a(); }
76+
void reach_error_61(){ reach_error_a(); }
77+
void reach_error_62(){ reach_error_a(); }
78+
void reach_error_63(){ reach_error_a(); }
79+
void reach_error_64(){ reach_error_b(); }
80+
void reach_error_65(){ reach_error_b(); }
81+
void reach_error_66(){ reach_error_a(); }
82+
void reach_error_67(){ reach_error_a(); }
83+
void reach_error_68(){ reach_error_a(); }
84+
void reach_error_69(){ reach_error_b(); }
85+
void reach_error_70(){ reach_error_a(); }
86+
void reach_error_71(){ reach_error_a(); }
87+
void reach_error_72(){ reach_error_a(); }
88+
void reach_error_73(){ reach_error_b(); }
89+
void reach_error_74(){ reach_error_a(); }
90+
void reach_error_75(){ reach_error_a(); }
91+
void reach_error_76(){ reach_error_a(); }
92+
void reach_error_77(){ reach_error_a(); }
93+
void reach_error_78(){ reach_error_a(); }
94+
void reach_error_79(){ reach_error_a(); }
95+
void reach_error_80(){ reach_error_a(); }
96+
void reach_error_81(){ reach_error_a(); }
97+
void reach_error_82(){ reach_error_a(); }
98+
void reach_error_83(){ reach_error_a(); }
99+
void reach_error_84(){ reach_error_a(); }
100+
void reach_error_85(){ reach_error_a(); }
101+
void reach_error_86(){ reach_error_a(); }
102+
void reach_error_87(){ reach_error_a(); }
103+
void reach_error_88(){ reach_error_b(); }
104+
void reach_error_89(){ reach_error_a(); }
105+
void reach_error_90(){ reach_error_a(); }
106+
void reach_error_91(){ reach_error_a(); }
107+
void reach_error_92(){ reach_error_b(); }
108+
void reach_error_93(){ reach_error_a(); }
109+
void reach_error_94(){ reach_error_a(); }
110+
void reach_error_95(){ reach_error_a(); }
111+
void reach_error_96(){ reach_error_a(); }
112+
void reach_error_97(){ reach_error_a(); }
113+
void reach_error_98(){ reach_error_a(); }
114+
void reach_error_99(){ reach_error_a(); }
102115

103116

104117
// inputs
@@ -1348,4 +1361,4 @@ int main()
13481361
return -2;
13491362
calculate_output(input);
13501363
}
1351-
}
1364+
}

‎c/eca-rers2018/Problem10.yml‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,12 @@
11
format_version: '2.0'
22
input_files: Problem10.c
33
properties:
4+
- property_file: ../properties/unreach-call.prp
5+
expected_verdict: false
6+
- property_file: properties/unreach-call-a.prp
7+
expected_verdict: true
8+
- property_file: properties/unreach-call-b.prp
9+
expected_verdict: false
410
- property_file: properties/unreach-call-0.prp
511
expected_verdict: true
612
- property_file: properties/unreach-call-1.prp

0 commit comments

Comments
 (0)