Skip to content

Commit

Permalink
Make all contracts unevaluated if no handler is active
Browse files Browse the repository at this point in the history 
That's a dynamic check, and easy to expand to a static one

Also rename `Axiom` to `Unevaluated` to avoid antibodies
  • Loading branch information
@hsutter
hsutter committed Dec 17, 2023
1 parent 696c5d4 commit 2893e64
Show file tree
Hide file tree
Showing 36 changed files with 324 additions and 317 deletions.
12 changes: 5 additions & 7 deletions include/cpp2util.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -391,11 +391,14 @@ class contract_group {
public:
using handler = void (*)(CPP2_MESSAGE_PARAM msg CPP2_SOURCE_LOCATION_PARAM);

constexpr contract_group (handler h) : reporter{h} { }
constexpr auto set_handler(handler h);
constexpr contract_group (handler h = {}) : reporter{h} { }
constexpr auto set_handler(handler h = {}) { reporter = h; }
constexpr auto get_handler() const -> handler { return reporter; }
constexpr auto has_handler() const -> bool { return reporter != handler{}; }
constexpr auto expects (bool b, CPP2_MESSAGE_PARAM msg = "" CPP2_SOURCE_LOCATION_PARAM_WITH_DEFAULT)
-> void { if (!b) reporter(msg CPP2_SOURCE_LOCATION_ARG); }
constexpr auto violation (CPP2_MESSAGE_PARAM msg = "" CPP2_SOURCE_LOCATION_PARAM_WITH_DEFAULT)
-> void { reporter(msg CPP2_SOURCE_LOCATION_ARG); }
private:
handler reporter;
};
Expand Down Expand Up @@ -441,11 +444,6 @@ auto inline Testing = contract_group(
}
);

constexpr auto contract_group::set_handler(handler h) {
Default.expects(h);
reporter = h;
}


// Null pointer deref checking
//
Expand Down
10 changes: 9 additions & 1 deletion regression-tests/pure2-contracts.cpp2
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,13 @@
test_condition_evaluation: (tag) -> bool = { std::cout << tag << "\n"; return true; }

main: () = {
assert( 1 != 2, "ack, arithmetic is buggy" );
assert<Type>( typeid(int) != typeid(double), "ack, C types are broken" );
assert<Axiom>( any-grammatical.kind(of, nonsense * here) is "all ignored" );
assert<Unevaluated>( any-grammatical.kind(of, nonsense * here) is "all ignored" );

assert( test_condition_evaluation(1), "default" ); // evaluated: prints "1"
assert<Type>( test_condition_evaluation(2), "type" ); // evaluated: prints "2"
cpp2::Type.set_handler();
assert<Type>( test_condition_evaluation(3), "type" ); // not evaluated
assert<Unevaluated>( test_condition_evaluation(4) ); // not evaluated
}
52 changes: 26 additions & 26 deletions regression-tests/test-results/clang-12/mixed-bugfix-for-ufcs-non-local.cpp.output
View file
Original file line number Diff line number Diff line change
@@ -1,118 +1,118 @@
mixed-bugfix-for-ufcs-non-local.cpp2:13:12: error: a lambda expression cannot appear in this context
template<t<CPP2_UFCS_NONLOCAL(f)(o)> _> bool inline constexpr v0 = false;// Fails on GCC ([GCC109781][]) and Clang 12 (a lambda expression cannot appear in this context)
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:15:3: error: a lambda expression cannot appear in this context
t<CPP2_UFCS_NONLOCAL(f)(o)> inline constexpr v1 = t<true>();// Fails on Clang 12 (lambda in unevaluated context).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:21:12: error: a lambda expression cannot appear in this context
template<t<CPP2_UFCS_NONLOCAL(f)(o)> _> auto g() -> void;
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:23:36: error: a lambda expression cannot appear in this context
auto g([[maybe_unused]] cpp2::in<t<CPP2_UFCS_NONLOCAL(f)(o)>> unnamed_param_1) -> void;
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:27:29: error: a lambda expression cannot appear in this context
[[nodiscard]] auto h() -> t<CPP2_UFCS_NONLOCAL(f)(o)>;
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:31:12: error: a lambda expression cannot appear in this context
template<t<CPP2_UFCS_NONLOCAL(f)(o)> _> using a = bool;// Fails on GCC ([GCC109781][]) and Clang 12 (a lambda expression cannot appear in this context)
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:33:12: error: a lambda expression cannot appear in this context
template<t<CPP2_UFCS_NONLOCAL(f)(o)> _> auto inline constexpr b = false;// Fails on GCC ([GCC109781][]).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:35:13: error: a lambda expression cannot appear in this context
using c = t<CPP2_UFCS_NONLOCAL(f)(o)>;// Fails on Clang 12 (lambda in unevaluated context) and Clang 12 (a lambda expression cannot appear in this context)
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:37:29: error: a lambda expression cannot appear in this context
auto inline constexpr d = t<CPP2_UFCS_NONLOCAL(f)(o)>();// Fails on Clang 12 (lambda in unevaluated context).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:21:12: error: a lambda expression cannot appear in this context
template<t<CPP2_UFCS_NONLOCAL(f)(o)> _> auto g() -> void{}// Fails on GCC ([GCC109781][]) and Clang 12 (a lambda expression cannot appear in this context)
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:23:36: error: a lambda expression cannot appear in this context
auto g([[maybe_unused]] cpp2::in<t<CPP2_UFCS_NONLOCAL(f)(o)>> unnamed_param_1) -> void{}// Fails on Clang 12 (lambda in unevaluated context).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:27:29: error: a lambda expression cannot appear in this context
[[nodiscard]] auto h() -> t<CPP2_UFCS_NONLOCAL(f)(o)> { return o; }// Fails on Clang 12 (lambda in unevaluated context).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
mixed-bugfix-for-ufcs-non-local.cpp2:41:79: error: lambda expression in an unevaluated operand
inline CPP2_CONSTEXPR bool u::c = [](cpp2::in<std::type_identity_t<decltype(CPP2_UFCS_NONLOCAL(f)(o))>> x) mutable -> auto { return x; }(true);// Fails on Clang 12 (lambda in unevaluated context).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
13 errors generated.
4 changes: 2 additions & 2 deletions regression-tests/test-results/clang-12/pure2-bugfix-for-ufcs-noexcept.cpp.output
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
pure2-bugfix-for-ufcs-noexcept.cpp2:5:26: error: lambda expression in an unevaluated operand
static_assert(noexcept(CPP2_UFCS(swap)(t(), t())));// Fails on Clang 12 (lambda in unevaluated context) and GCC 10 (static assertion failed)
^
../../../include/cpp2util.h:859:59: note: expanded from macro 'CPP2_UFCS'
../../../include/cpp2util.h:857:59: note: expanded from macro 'CPP2_UFCS'
#define CPP2_UFCS(...) CPP2_UFCS_(&,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
1 error generated.
8 changes: 4 additions & 4 deletions regression-tests/test-results/clang-12/pure2-bugfix-for-ufcs-sfinae.cpp.output
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,19 @@
pure2-bugfix-for-ufcs-sfinae.cpp2:1:78: error: lambda expression in an unevaluated operand
template<typename T> [[nodiscard]] auto f() -> std::type_identity_t<decltype(CPP2_UFCS_NONLOCAL(a)(T()))>;
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
pure2-bugfix-for-ufcs-sfinae.cpp2:1:78: error: lambda expression in an unevaluated operand
template<typename T> [[nodiscard]] auto f() -> std::type_identity_t<decltype(CPP2_UFCS_NONLOCAL(a)(T()))>{}// Fails on Clang 12 (lambda in unevaluated context).
^
../../../include/cpp2util.h:862:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
../../../include/cpp2util.h:860:59: note: expanded from macro 'CPP2_UFCS_NONLOCAL'
#define CPP2_UFCS_NONLOCAL(...) CPP2_UFCS_(,(),,__VA_ARGS__)
^
../../../include/cpp2util.h:843:53: note: expanded from macro 'CPP2_UFCS_'
../../../include/cpp2util.h:841:53: note: expanded from macro 'CPP2_UFCS_'
#define CPP2_UFCS_(LAMBDADEFCAPT,QUALID,TEMPKW,...) \
^
2 errors generated.
7 changes: 0 additions & 7 deletions ...sion-tests/test-results/clang-12/pure2-bugfix-for-unbraced-function-expression.cpp.output
View file
Original file line number Diff line number Diff line change
@@ -1,7 +0,0 @@
pure2-bugfix-for-unbraced-function-expression.cpp2:2:34: warning: unused parameter 'f' [-Wunused-parameter]
auto t::operator[](auto const& f) const& -> void{}
^
pure2-bugfix-for-unbraced-function-expression.cpp2:9:65: warning: expression result unused [-Wunused-value]
cpp2::Default.expects(!((cpp2::is<int>([]() mutable -> void { 0; }))), "");
^
2 warnings generated.
2 changes: 2 additions & 0 deletions regression-tests/test-results/clang-12/pure2-contracts.cpp.execution
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
1
2
6 changes: 0 additions & 6 deletions ...ession-tests/test-results/gcc-10/pure2-bugfix-for-unbraced-function-expression.cpp.output
View file
Original file line number Diff line number Diff line change
@@ -1,6 +0,0 @@
pure2-bugfix-for-unbraced-function-expression.cpp2: In instantiation of ‘void t::operator[](const auto:90&) const & [with auto:89 = main()::<lambda()>]’:
pure2-bugfix-for-unbraced-function-expression.cpp2:6:4: required from here
pure2-bugfix-for-unbraced-function-expression.cpp2:2:34: warning: unused parameter ‘f’ [-Wunused-parameter]
pure2-bugfix-for-unbraced-function-expression.cpp2: In instantiation of ‘void t::operator[](const auto:90&) const & [with auto:89 = main()::<lambda()>]’:
pure2-bugfix-for-unbraced-function-expression.cpp2:7:4: required from here
pure2-bugfix-for-unbraced-function-expression.cpp2:2:34: warning: unused parameter ‘f’ [-Wunused-parameter]
2 changes: 2 additions & 0 deletions regression-tests/test-results/gcc-10/pure2-contracts.cpp.execution
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
1
2
Loading

0 comments on commit 2893e64

Please sign in to comment.