From dc3cee7cf3d49ad592139042a8e15e3905e55ee9 Mon Sep 17 00:00:00 2001
From: Ken Matsui <26405363+matken11235@users.noreply.github.com>
Date: Thu, 12 Sep 2019 08:48:18 +0900
Subject: [PATCH] Fix not to output all warnings (#2778)

Fix syntax error when --language-bindings is java

Replace __attribute__((__unused__)) with CVC4_UNUSED macro

Signed-off-by: matken11235 <26405363+matken11235@users.noreply.github.com>
---
 src/base/exception.h         | 6 +++---
 src/context/cdlist_forward.h | 2 +-
 src/expr/datatype.h          | 2 +-
 3 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/base/exception.h b/src/base/exception.h
index 51829c86c..704ca928e 100644
--- a/src/base/exception.h
+++ b/src/base/exception.h
@@ -125,15 +125,15 @@ inline std::ostream& operator<<(std::ostream& os, const Exception& e)
 
 template <class T> inline void CheckArgument(bool cond, const T& arg,
                                              const char* tail) CVC4_PUBLIC;
-template <class T> inline void CheckArgument(bool cond, const T& arg,
-                                             const char* tail) {
+template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED,
+                                             const char* tail CVC4_UNUSED) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
 }
 template <class T> inline void CheckArgument(bool cond, const T& arg)
   CVC4_PUBLIC;
-template <class T> inline void CheckArgument(bool cond, const T& arg) {
+template <class T> inline void CheckArgument(bool cond, const T& arg CVC4_UNUSED) {
   if(__builtin_expect( ( !cond ), false )) { \
     throw ::CVC4::IllegalArgumentException("", "", ""); \
   } \
diff --git a/src/context/cdlist_forward.h b/src/context/cdlist_forward.h
index d7b1cbc61..1cdbab7cb 100644
--- a/src/context/cdlist_forward.h
+++ b/src/context/cdlist_forward.h
@@ -42,7 +42,7 @@ namespace context {
 template <class T>
 class DefaultCleanUp {
 public:
-  inline void operator()(T* t) const{}
+  inline void operator()(T* t CVC4_UNUSED) const{}
 };
 
 template <class T, class CleanUp = DefaultCleanUp<T>, class Allocator = std::allocator<T> >
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 0e8ace709..b7a2721ab 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -1084,7 +1084,7 @@ class CVC4_PUBLIC DatatypeIndexConstant {
  public:
   DatatypeIndexConstant(unsigned index);
 
-  const unsigned getIndex() const { return d_index; }
+  unsigned getIndex() const { return d_index; }
   bool operator==(const DatatypeIndexConstant& uc) const
   {
     return d_index == uc.d_index;
-- 
2.30.2