Skip to content

Commit d9c678b

Browse files
tautschnigtautschnig
authored
Merge pull request #5801 from tautschnig/goto-checker-properties
goto-checker properties: do not ignore ERROR
2 parents cc30590 + 0d32a6b commit d9c678b

File tree

4 files changed

+181
-1
lines changed

4 files changed

+181
-1
lines changed

‎src/goto-checker/properties.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -226,7 +226,6 @@ property_statust &operator&=(property_statust &a, property_statust const &b)
226226
switch(a)
227227
{
228228
case property_statust::ERROR:
229-
a = b;
230229
return a;
231230
case property_statust::FAIL:
232231
a = (b == property_statust::ERROR ? b : a);

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,7 @@ SRC += analyses/ai/ai.cpp \
3434
compound_block_locations.cpp \
3535
get_goto_model_from_c_test.cpp \
3636
goto-cc/armcc_cmdline.cpp \
37+
goto-checker/properties/property_status.cpp \
3738
goto-checker/report_util/is_property_less_than.cpp \
3839
goto-instrument/cover_instrument.cpp \
3940
goto-instrument/cover/cover_only.cpp \

‎unit/goto-checker/properties/module_dependencies.txt

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,2 @@
1+
goto-checker
2+
testing-utils

‎unit/goto-checker/properties/property_status.cpp

Lines changed: 178 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,178 @@
1+
// Copyright 2021 Michael Tautschnig
2+
3+
/// \file Tests operations on property_statust
4+
5+
#include <goto-checker/properties.h>
6+
7+
#include <testing-utils/use_catch.h>
8+
9+
TEST_CASE(
10+
"Preference order of properties",
11+
"[core][goto-checker][property_statust]")
12+
{
13+
const property_statust error{property_statust::ERROR};
14+
const property_statust fail{property_statust::FAIL};
15+
const property_statust unknown{property_statust::UNKNOWN};
16+
const property_statust not_checked{property_statust::NOT_CHECKED};
17+
const property_statust not_reachable{property_statust::NOT_REACHABLE};
18+
const property_statust pass{property_statust::PASS};
19+
20+
SECTION("Update a single property status")
21+
{
22+
property_statust status = property_statust::ERROR;
23+
status |= unknown;
24+
REQUIRE(status == property_statust::ERROR);
25+
status |= error;
26+
REQUIRE(status == property_statust::ERROR);
27+
28+
status = property_statust::FAIL;
29+
status |= unknown;
30+
REQUIRE(status == property_statust::FAIL);
31+
status |= fail;
32+
REQUIRE(status == property_statust::FAIL);
33+
34+
status = property_statust::UNKNOWN;
35+
status |= pass;
36+
REQUIRE(status == property_statust::PASS);
37+
status = property_statust::UNKNOWN;
38+
status |= not_reachable;
39+
REQUIRE(status == property_statust::NOT_REACHABLE);
40+
status = property_statust::UNKNOWN;
41+
status |= unknown;
42+
REQUIRE(status == property_statust::UNKNOWN);
43+
status = property_statust::UNKNOWN;
44+
status |= fail;
45+
REQUIRE(status == property_statust::FAIL);
46+
status = property_statust::UNKNOWN;
47+
status |= error;
48+
REQUIRE(status == property_statust::ERROR);
49+
50+
status = property_statust::NOT_CHECKED;
51+
status |= pass;
52+
REQUIRE(status == property_statust::PASS);
53+
status = property_statust::NOT_CHECKED;
54+
status |= not_reachable;
55+
REQUIRE(status == property_statust::NOT_REACHABLE);
56+
status = property_statust::NOT_CHECKED;
57+
status |= not_checked;
58+
REQUIRE(status == property_statust::NOT_CHECKED);
59+
status = property_statust::NOT_CHECKED;
60+
status |= unknown;
61+
REQUIRE(status == property_statust::UNKNOWN);
62+
status = property_statust::NOT_CHECKED;
63+
status |= fail;
64+
REQUIRE(status == property_statust::FAIL);
65+
status = property_statust::NOT_CHECKED;
66+
status |= error;
67+
REQUIRE(status == property_statust::ERROR);
68+
69+
status = property_statust::NOT_REACHABLE;
70+
status |= not_reachable;
71+
REQUIRE(status == property_statust::NOT_REACHABLE);
72+
status |= unknown;
73+
REQUIRE(status == property_statust::NOT_REACHABLE);
74+
75+
status = property_statust::PASS;
76+
status |= pass;
77+
REQUIRE(status == property_statust::PASS);
78+
status |= unknown;
79+
REQUIRE(status == property_statust::PASS);
80+
}
81+
82+
SECTION("Determine overall status")
83+
{
84+
property_statust status = property_statust::ERROR;
85+
status &= pass;
86+
REQUIRE(status == property_statust::ERROR);
87+
status &= not_reachable;
88+
REQUIRE(status == property_statust::ERROR);
89+
status &= not_checked;
90+
REQUIRE(status == property_statust::ERROR);
91+
status &= unknown;
92+
REQUIRE(status == property_statust::ERROR);
93+
status &= fail;
94+
REQUIRE(status == property_statust::ERROR);
95+
status &= error;
96+
REQUIRE(status == property_statust::ERROR);
97+
98+
status = property_statust::FAIL;
99+
status &= pass;
100+
REQUIRE(status == property_statust::FAIL);
101+
status &= not_reachable;
102+
REQUIRE(status == property_statust::FAIL);
103+
status &= not_checked;
104+
REQUIRE(status == property_statust::FAIL);
105+
status &= unknown;
106+
REQUIRE(status == property_statust::FAIL);
107+
status &= fail;
108+
REQUIRE(status == property_statust::FAIL);
109+
status &= error;
110+
REQUIRE(status == property_statust::ERROR);
111+
112+
status = property_statust::UNKNOWN;
113+
status &= pass;
114+
REQUIRE(status == property_statust::UNKNOWN);
115+
status &= not_reachable;
116+
REQUIRE(status == property_statust::UNKNOWN);
117+
status &= not_checked;
118+
REQUIRE(status == property_statust::UNKNOWN);
119+
status &= unknown;
120+
REQUIRE(status == property_statust::UNKNOWN);
121+
status &= fail;
122+
REQUIRE(status == property_statust::FAIL);
123+
status = property_statust::UNKNOWN;
124+
status &= error;
125+
REQUIRE(status == property_statust::ERROR);
126+
127+
status = property_statust::NOT_CHECKED;
128+
status &= pass;
129+
REQUIRE(status == property_statust::NOT_CHECKED);
130+
status &= not_reachable;
131+
REQUIRE(status == property_statust::NOT_CHECKED);
132+
status &= not_checked;
133+
REQUIRE(status == property_statust::NOT_CHECKED);
134+
status &= unknown;
135+
REQUIRE(status == property_statust::UNKNOWN);
136+
status = property_statust::NOT_CHECKED;
137+
status &= fail;
138+
REQUIRE(status == property_statust::FAIL);
139+
status = property_statust::NOT_CHECKED;
140+
status &= error;
141+
REQUIRE(status == property_statust::ERROR);
142+
143+
status = property_statust::NOT_REACHABLE;
144+
status &= pass;
145+
REQUIRE(status == property_statust::NOT_REACHABLE);
146+
status &= not_reachable;
147+
REQUIRE(status == property_statust::NOT_REACHABLE);
148+
status &= not_checked;
149+
REQUIRE(status == property_statust::NOT_CHECKED);
150+
status = property_statust::NOT_REACHABLE;
151+
status &= unknown;
152+
REQUIRE(status == property_statust::UNKNOWN);
153+
status = property_statust::NOT_REACHABLE;
154+
status &= fail;
155+
REQUIRE(status == property_statust::FAIL);
156+
status = property_statust::NOT_REACHABLE;
157+
status &= error;
158+
REQUIRE(status == property_statust::ERROR);
159+
160+
status = property_statust::PASS;
161+
status &= pass;
162+
REQUIRE(status == property_statust::PASS);
163+
status &= not_reachable;
164+
REQUIRE(status == property_statust::NOT_REACHABLE);
165+
status = property_statust::PASS;
166+
status &= not_checked;
167+
REQUIRE(status == property_statust::NOT_CHECKED);
168+
status = property_statust::PASS;
169+
status &= unknown;
170+
REQUIRE(status == property_statust::UNKNOWN);
171+
status = property_statust::PASS;
172+
status &= fail;
173+
REQUIRE(status == property_statust::FAIL);
174+
status = property_statust::PASS;
175+
status &= error;
176+
REQUIRE(status == property_statust::ERROR);
177+
}
178+
}

0 commit comments

Comments
 (0)