diff --git a/src/include/pv.h b/src/include/pv.h
index abd0812..1931398 100644
--- a/src/include/pv.h
+++ b/src/include/pv.h
@@ -280,7 +280,7 @@ extern void pv_state_free(/*@only@*/ pvstate_t);
 # endif
 # define debug(x,...) debugging_output(__func__, __FILE__, __LINE__, x, __VA_ARGS__)
 #else
-# define debug(x,...) do { } while (0)
+# define debug(x,...) /*@-noeffect@*/ do { } while (0) /*@+noeffect@*/
 #endif
 
 /*
diff --git a/src/main/debug.c b/src/main/debug.c
index 9b48356..50f7e5c 100644
--- a/src/main/debug.c
+++ b/src/main/debug.c
@@ -101,7 +101,7 @@ void debugging_output(const char *function, const char *file, int line, const ch
 /*
  * Stub debugging destination function.
  */
-void debugging_output_destination( __attribute__((unused))
+void debugging_output_destination( /*@unused@ */  __attribute__((unused))
 				  const char *filename)
 {
 }
@@ -109,10 +109,10 @@ void debugging_output_destination( __attribute__((unused))
 /*
  * Stub debugging output function.
  */
-void debugging_output( __attribute__((unused))
-		      const char *function, __attribute__((unused))
-		      const char *file, __attribute__((unused))
-		      int line, __attribute__((unused))
+void debugging_output( /*@unused@ */  __attribute__((unused))
+		      const char *function, /*@unused@ */  __attribute__((unused))
+		      const char *file, /*@unused@ */  __attribute__((unused))
+		      int line, /*@unused@ */  __attribute__((unused))
 		      const char *format, ...)
 {
 }