From b06f4135852cce8649fa1da92a9a53a8c7994782 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Jan 2018 23:20:00 +0700 Subject: [PATCH] raise_exception: Annotate that this doesn't return. --- src/ast/ast.h | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 24e2b93b6..ea97af004 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -53,6 +53,12 @@ Revision History: #pragma warning(disable : 4355) #endif +#ifdef __GNUC__ +# define Z3_NORETURN __attribute__((noreturn)) +#else +# define Z3_NORETURN +#endif + class ast; class ast_manager; @@ -1515,7 +1521,7 @@ public: void compress_ids(); // Equivalent to throw ast_exception(msg) - void raise_exception(char const * msg); + void raise_exception(char const * msg) Z3_NORETURN; bool is_format_manager() const { return m_format_manager == 0; }