mirror of
https://github.com/microsoft/GSL.git
synced 2024-11-03 17:56:43 -05:00
Improve GSL postconditions and add invariants
This commit is contained in:
parent
c9e423d7cf
commit
5a84fe69d8
@ -88,6 +88,58 @@ struct fail_fast : public std::logic_error
|
||||
#endif
|
||||
|
||||
#define Expects(cond) GSL_CONTRACT_CHECK("Precondition", cond)
|
||||
#define Ensures(cond) GSL_CONTRACT_CHECK("Postcondition", cond)
|
||||
|
||||
#if defined(GSL_UNENFORCED_ON_CONTRACT_VIOLATION)
|
||||
|
||||
#define Ensures(cond) static_cast<void>(0)
|
||||
#define AlwaysEnsures(cond) static_cast<void>(0)
|
||||
|
||||
#else // GSL_UNENFORCED_ON_CONTRACT_VIOLATION
|
||||
|
||||
// Ensures uses an object that checks the condition on destruction
|
||||
// Setting `always` to true means we want the ensurer to trigger even when
|
||||
// exiting via exception (this will call std::terminate).
|
||||
template<class A, bool always> class gsl_ensurer {
|
||||
gsl_ensurer (const gsl_ensurer&) = delete;
|
||||
gsl_ensurer& operator=(const gsl_ensurer&) = delete;
|
||||
A& asserter;
|
||||
public:
|
||||
gsl_ensurer(A& asserter) : asserter(asserter) {}
|
||||
~gsl_ensurer() noexcept(false)
|
||||
{ if (!std::uncaught_exceptions() || always) asserter(); }
|
||||
};
|
||||
|
||||
// Use line numbers to create unique names for each ensurer.
|
||||
#define GSL_UNIQUE(a) GSL_JOIN(a, __LINE__)
|
||||
#define GSL_JOIN(a, b) GSL_PASTE(a, b)
|
||||
#define GSL_PASTE(a, b) a##b
|
||||
|
||||
// Ensure along all non-exception exit paths.
|
||||
#define Ensures(cond) \
|
||||
auto GSL_UNIQUE(GSL_ENSURER_) = [&]() { \
|
||||
GSL_CONTRACT_CHECK("Postcondition", cond); \
|
||||
}; \
|
||||
gsl_ensurer<decltype(GSL_UNIQUE(GSL_ENSURER_)), false> \
|
||||
GSL_UNIQUE(GSL_ENSURE_)(GSL_UNIQUE(GSL_ENSURER_));
|
||||
|
||||
// Ensure even when exiting via exception.
|
||||
#define AlwaysEnsures(cond) \
|
||||
auto GSL_UNIQUE(GSL_ENSURER_) = [&]() { \
|
||||
GSL_CONTRACT_CHECK("Postcondition", cond); \
|
||||
}; \
|
||||
gsl_ensurer<decltype(GSL_UNIQUE(GSL_ENSURER_)), true> \
|
||||
GSL_UNIQUE(GSL_ENSURE_)(GSL_UNIQUE(GSL_ENSURER_));
|
||||
|
||||
#endif // GSL_UNENFORCED_ON_CONTRACT_VIOLATION
|
||||
|
||||
// Assert that a function maintains an invariant during normal control flow
|
||||
#define Maintains(cond) \
|
||||
Expects(cond); \
|
||||
Ensures(cond) \
|
||||
|
||||
// Assert that the invariant is maintained even when exiting via exception
|
||||
#define AlwaysMaintains(cond) \
|
||||
Expects(cond); \
|
||||
AlwaysEnsures(cond) \
|
||||
|
||||
#endif // GSL_CONTRACTS_H
|
||||
|
@ -34,8 +34,26 @@ TEST_CASE("expects")
|
||||
|
||||
int g(int i)
|
||||
{
|
||||
i++;
|
||||
Ensures(i > 0 && i < 10);
|
||||
i++;
|
||||
return i;
|
||||
}
|
||||
|
||||
int g2(int i)
|
||||
{
|
||||
Ensures(i > 0 && i < 10);
|
||||
Ensures(i == 4);
|
||||
|
||||
i++;
|
||||
return i;
|
||||
}
|
||||
|
||||
int g3(int i)
|
||||
{
|
||||
AlwaysEnsures(i > 0 && i < 10);
|
||||
AlwaysEnsures(i == 4);
|
||||
|
||||
i++;
|
||||
return i;
|
||||
}
|
||||
|
||||
@ -43,4 +61,59 @@ TEST_CASE("ensures")
|
||||
{
|
||||
CHECK(g(2) == 3);
|
||||
CHECK_THROWS_AS(g(9), fail_fast);
|
||||
|
||||
CHECK(g2(3) == 4);
|
||||
CHECK_THROWS_AS(g2(4), fail_fast);
|
||||
CHECK_THROWS_AS(g2(9), fail_fast);
|
||||
|
||||
CHECK(g3(3) == 4);
|
||||
CHECK_THROWS_AS(g3(4), fail_fast);
|
||||
// g3(9); // should terminate
|
||||
}
|
||||
|
||||
int h(int i, int j)
|
||||
{
|
||||
Maintains(i > 0 && i < 10);
|
||||
i += j;
|
||||
return i;
|
||||
}
|
||||
|
||||
int h2(int i, int j)
|
||||
{
|
||||
Maintains(i < 3);
|
||||
Maintains(J > 7);
|
||||
i++;
|
||||
j--;
|
||||
return i + j;
|
||||
}
|
||||
|
||||
int h3(int i, int j)
|
||||
{
|
||||
AlwaysMaintains(i < 3);
|
||||
AlwaysMaintains(j > 7);
|
||||
i++;
|
||||
j--;
|
||||
return i + j;
|
||||
}
|
||||
|
||||
TEST_CASE("maintains")
|
||||
{
|
||||
CHECK(h(2, 4) == 6);
|
||||
CHECK_THROWS_AS(h(9,1), fail_fast);
|
||||
CHECK_THROWS_AS(h(1,-1), fail_fast);
|
||||
CHECK_THROWS_AS(h(0,2), fail_fast);
|
||||
|
||||
CHECK(h2(1,9) == 10);
|
||||
CHECK_THROWS_AS(h2(1,7), fail_fast);
|
||||
CHECK_THROWS_AS(h2(1,8), fail_fast);
|
||||
CHECK_THROWS_AS(h2(3,9), fail_fast);
|
||||
CHECK_THROWS_AS(h2(2,9), fail_fast);
|
||||
CHECK_THROWS_AS(h2(2,8), fail_fast);
|
||||
|
||||
CHECK(h3(1,9) == 10);
|
||||
CHECK_THROWS_AS(h3(1,7), fail_fast);
|
||||
CHECK_THROWS_AS(h3(1,8), fail_fast);
|
||||
CHECK_THROWS_AS(h3(3,9), fail_fast);
|
||||
CHECK_THROWS_AS(h3(2,9), fail_fast);
|
||||
// h3(2,8); // should terminate
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user