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>

diff --git a/src/base/exception.h b/src/base/exception.h
index 51829c86c560fcc7d0563d55da7b1368a814697e..704ca928e3d06216a51a6e3320ac55499d531e0b 100644 (file)
--- 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 d7b1cbc61367b0106b5bd42e01a2956ca9b2fb5e..1cdbab7cb86a183770aa634019e00b396e1be795 100644 (file)
--- 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 0e8ace709984fb9c9c03512798f5e679a38c5e39..b7a2721ab6c8f315a17480e59c3220cf9615d6e7 100644 (file)
--- 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;