Skip to content

Commit 4b55962

Browse files
Add has_properties_to_check
1 parent 3c2778e commit 4b55962

File tree

2 files changed

+22
-0
lines changed

2 files changed

+22
-0
lines changed

src/goto-checker/properties.cpp

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -145,6 +145,22 @@ count_properties(const propertiest &properties, property_statust status)
145145
return count;
146146
}
147147

148+
bool is_property_to_check(property_statust status)
149+
{
150+
return status == property_statust::NOT_CHECKED ||
151+
status == property_statust::UNKNOWN;
152+
}
153+
154+
bool has_properties_to_check(const propertiest &properties)
155+
{
156+
for(const auto &property_pair : properties)
157+
{
158+
if(is_property_to_check(property_pair.second.status))
159+
return true;
160+
}
161+
return false;
162+
}
163+
148164
/// Update with the preference order
149165
/// 1. old non-UNKNOWN/non-NOT_CHECKED status
150166
/// 2. new non-UNKNOWN/non-NOT_CHECKED status

src/goto-checker/properties.h

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -89,6 +89,12 @@ int result_to_exit_code(resultt result);
8989
/// Return the number of properties with given \p status
9090
std::size_t count_properties(const propertiest &, property_statust);
9191

92+
/// Return true if the status is NOT_CHECKED or UNKNOWN
93+
bool is_property_to_check(property_statust);
94+
95+
/// Return true if there as a property with NOT_CHECKED or UNKNOWN status
96+
bool has_properties_to_check(const propertiest &properties);
97+
9298
property_statust &operator|=(property_statust &, property_statust const &);
9399
property_statust &operator&=(property_statust &, property_statust const &);
94100
resultt determine_result(const propertiest &properties);

0 commit comments

Comments
 (0)