Skip to content

Commit 8e251a9

Browse files
Add has_properties_to_check
1 parent dcefb13 commit 8e251a9

File tree

2 files changed

+17
-0
lines changed

2 files changed

+17
-0
lines changed

src/goto-checker/properties.cpp

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -233,3 +233,18 @@ resultt determine_result(const propertiest &properties)
233233
}
234234
return static_cast<resultt>(status);
235235
}
236+
237+
/// Returns true if there as a property with NOT_CHECKED or UNKNOWN status.
238+
bool has_properties_to_check(const propertiest &properties)
239+
{
240+
for(const auto &property_pair : properties)
241+
{
242+
if(
243+
property_pair.second.status == property_statust::NOT_CHECKED ||
244+
property_pair.second.status == property_statust::UNKNOWN)
245+
{
246+
return true;
247+
}
248+
}
249+
return false;
250+
}

src/goto-checker/properties.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -93,4 +93,6 @@ property_statust &operator|=(property_statust &, property_statust const &);
9393
property_statust &operator&=(property_statust &, property_statust const &);
9494
resultt determine_result(const propertiest &properties);
9595

96+
bool has_properties_to_check(const propertiest &properties);
97+
9698
#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H

0 commit comments

Comments
 (0)