From 968607261b1ca820bc525b7830f93c177e828b85 Mon Sep 17 00:00:00 2001
From: Andreas Tiemeyer <andreas.tiemeyer@gmx.com>
Date: Fri, 13 Oct 2017 10:19:23 +0100
Subject: [PATCH] Replace asserts with INVARIANT et al. to enable compilation
 with NDEBUG for src and unit tests with gcc and clang.

---
 src/goto-programs/remove_returns.cpp |  4 ++--
 src/util/sharing_node.h              |  2 +-
 unit/sharing_node.cpp                | 21 ++++++++++++++++-----
 3 files changed, 19 insertions(+), 8 deletions(-)

diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 1a22bd72359..864d89ebd76 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -290,8 +290,8 @@ bool remove_returnst::restore_returns(
 
       if(i_it->is_goto())
       {
-        goto_programt::const_targett target=i_it->get_target();
-        assert(target->is_end_function());
+        DATA_INVARIANT(i_it->get_target()->is_end_function(),
+          "goto after return value assignment is to end of function");
       }
       else
       {
diff --git a/src/util/sharing_node.h b/src/util/sharing_node.h
index 19b41712649..9281ba8b94f 100644
--- a/src/util/sharing_node.h
+++ b/src/util/sharing_node.h
@@ -178,7 +178,7 @@ class sharing_nodet
     subt &s=get_sub();
     size_t r=s.erase(n);
 
-    _sn_assert(r==1);
+    CHECK_RETURN(r==1);
   }
 
   // container nodes
diff --git a/unit/sharing_node.cpp b/unit/sharing_node.cpp
index 2d256b8dd45..64bd590b8fe 100644
--- a/unit/sharing_node.cpp
+++ b/unit/sharing_node.cpp
@@ -1,3 +1,14 @@
+/*******************************************************************\
+
+Module: Unit tests for sharing node
+
+Author: Daniel Poetzl, daniel.poetzl@cs.ox.ac.uk
+
+\*******************************************************************/
+
+/// \file
+/// Unit tests for class sharing_nodet
+
 #include <iostream>
 #include <cassert>
 
@@ -30,7 +41,7 @@ void sharing_node_test()
     assert(sn2.get_sub().size()==3);
 
     p2=sn2.find_child(0);
-    assert(p2!=nullptr);
+    CHECK_RETURN(p2!=nullptr);
 
     p2=sn1.find_child(0);
     assert(p2!=nullptr);
@@ -62,7 +73,7 @@ void sharing_node_test()
     p2=p1;
 
     assert(p1->find_leaf("a")==nullptr);
-    assert(p2->find_leaf("a")==nullptr);
+    CHECK_RETURN(p2->find_leaf("a")==nullptr);
 
     p1->place_leaf("a", "b");
     assert(p2->get_container().size()==1);
@@ -114,15 +125,15 @@ void sharing_node_test()
     assert(sn2.is_internal());
 
     sn1.remove_child(0);
-    assert(sn1c.get_sub().size()==1);
+    INVARIANT(sn1c.get_sub().size()==1, "node has one child");
 
-    assert(sn2c.get_sub().size()==2);
+    INVARIANT(sn2c.get_sub().size()==2, "node has two children");
   }
 }
 
 int main()
 {
-  sharing_node_test();  
+  sharing_node_test();
 
   return 0;
 }