From 7457fa77cb44f9cfdfb4fc552581e10c41ee69b6 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 2 Jan 2018 08:46:17 -0800
Subject: [PATCH] add noreturn attribute #1435

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.cpp | 41 ++++++++++++++---------------------------
 src/ast/ast.h   |  8 +-------
 2 files changed, 15 insertions(+), 34 deletions(-)

diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index 3824325b3..0f18170df 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -1492,11 +1492,8 @@ void ast_manager::compact_memory() {
     unsigned capacity = m_ast_table.capacity();
     if (capacity > 4*m_ast_table.size()) {
         ast_table new_ast_table;
-        ast_table::iterator it  = m_ast_table.begin();
-        ast_table::iterator end = m_ast_table.end();
-        for (; it != end; ++it) {
-            new_ast_table.insert(*it);
-        }
+        for (ast* curr : m_ast_table)
+            new_ast_table.insert(curr);
         m_ast_table.swap(new_ast_table);
         IF_VERBOSE(10, verbose_stream() << "(ast-table :prev-capacity " << capacity
                    << " :capacity " << m_ast_table.capacity() << " :size " << m_ast_table.size() << ")\n";);
@@ -1510,10 +1507,7 @@ void ast_manager::compress_ids() {
     ptr_vector<ast> asts;
     m_expr_id_gen.cleanup();
     m_decl_id_gen.cleanup(c_first_decl_id);
-    ast_table::iterator it  = m_ast_table.begin();
-    ast_table::iterator end = m_ast_table.end();
-    for (; it != end; ++it) {
-        ast * n = *it;
+    for (ast * n : m_ast_table) {
         if (is_decl(n))
             n->m_id = m_decl_id_gen.mk();
         else
@@ -1521,13 +1515,11 @@ void ast_manager::compress_ids() {
         asts.push_back(n);
     }
     m_ast_table.finalize();
-    ptr_vector<ast>::iterator it2  = asts.begin();
-    ptr_vector<ast>::iterator end2 = asts.end();
-    for (; it2 != end2; ++it2)
-        m_ast_table.insert(*it2);
+    for (ast* a : asts) 
+        m_ast_table.insert(a);
 }
 
-void ast_manager::raise_exception(char const * msg) {
+[[noreturn]] void ast_manager::raise_exception(char const * msg) {
     throw ast_exception(msg);
 }
 
@@ -1570,20 +1562,15 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
 }
 
 void ast_manager::set_next_expr_id(unsigned id) {
-    while (true) {
-        id = m_expr_id_gen.set_next_id(id);
-        ast_table::iterator it  = m_ast_table.begin();
-        ast_table::iterator end = m_ast_table.end();
-        for (; it != end; ++it) {
-            ast * curr = *it;
-            if (curr->get_id() == id)
-                break;
+ try_again:
+    id = m_expr_id_gen.set_next_id(id);
+    for (ast * curr : m_ast_table) {
+        if (curr->get_id() == id) {
+            // id is in use, move to the next one.
+            ++id;
+            goto try_again;
         }
-        if (it == end)
-            return;
-        // id is in use, move to the next one.
-        id++;
-    }
+    }    
 }
 
 unsigned ast_manager::get_node_size(ast const * n) { return ::get_node_size(n); }
diff --git a/src/ast/ast.h b/src/ast/ast.h
index ea97af004..482ec3a99 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -53,12 +53,6 @@ Revision History:
 #pragma warning(disable : 4355)
 #endif
 
-#ifdef __GNUC__
-#  define Z3_NORETURN __attribute__((noreturn))
-#else
-#  define Z3_NORETURN
-#endif
-
 class ast;
 class ast_manager;
 
@@ -1521,7 +1515,7 @@ public:
     void compress_ids();
 
     // Equivalent to throw ast_exception(msg)
-    void raise_exception(char const * msg) Z3_NORETURN;
+    [[noreturn]] void raise_exception(char const * msg);
 
     bool is_format_manager() const { return m_format_manager == 0; }