Skip to content

Commit 2bee7b3

Browse files
Add has_properties_to_check
1 parent fbbcdb2 commit 2bee7b3

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
@@ -232,3 +232,18 @@ resultt determine_result(const propertiest &properties)
232232
}
233233
return static_cast<resultt>(result);
234234
}
235+
236+
/// Returns true if there as a property with NOT_CHECKED or UNKNOWN status.
237+
bool has_properties_to_check(const propertiest &properties)
238+
{
239+
for(const auto &property_pair : properties)
240+
{
241+
if(
242+
property_pair.second.status == property_statust::NOT_CHECKED ||
243+
property_pair.second.status == property_statust::UNKNOWN)
244+
{
245+
return true;
246+
}
247+
}
248+
return false;
249+
}

src/goto-checker/properties.h

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

97+
bool has_properties_to_check(const propertiest &properties);
98+
9799
#endif // CPROVER_GOTO_CHECKER_PROPERTIES_H

0 commit comments

Comments
 (0)