(symbolic engines) annotate P*_PrintToMainLog, error message, export_string methods for format string checks

GCC / CLang offer checking for consistency between format strings and the variable argument parameters that
are passed to printf-like functions. For these compilers, we add the necessary function attribute (use with -Wformat).

For MinGW, we have to be a bit more specific, as both a STDIO implementation by Microsoft as well
as a POSIX compatible implementation are supported. Generally, for C++, the POSIX library is used. We check the
MinGW compiler definition that selects the STDIO implementation and use the corresponding format specification
(gnu_printf vs ms_printf).


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12178 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/include/PrismHybridGlob.h

@@ -45,11 +45,11 @@ extern double last_unif;
 // macros, function prototypes
 
 #define logtwo(X) log((double)X)/log(2.0)
-void PH_PrintToMainLog(JNIEnv *env, const char *str, ...);
-void PH_PrintWarningToMainLog(JNIEnv *env, const char *str, ...);
-void PH_PrintToTechLog(JNIEnv *env, const char *str, ...);
+void PH_PrintToMainLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
+void PH_PrintWarningToMainLog(JNIEnv *env, const char *str, ...)  IS_LIKE_PRINTF(2,3);
+void PH_PrintToTechLog(JNIEnv *env, const char *str, ...)  IS_LIKE_PRINTF(2,3);
 void PH_PrintMemoryToMainLog(JNIEnv *env, const char *before, double mem, const char *after);
-void PH_SetErrorMessage(const char *str, ...);
+void PH_SetErrorMessage(const char *str, ...)  IS_LIKE_PRINTF(1,2);
 char *PH_GetErrorMessage();
 bool PH_GetFlagExportIterations();
 

prism/include/PrismMTBDDGlob.h

@@ -44,13 +44,15 @@ extern JNIEnv *export_env;
 
 // function prototypes
 
-void PM_PrintToMainLog(JNIEnv *env, const char *str, ...);
-void PM_PrintWarningToMainLog(JNIEnv *env, const char *str, ...);
-void PM_PrintToTechLog(JNIEnv *env, const char *str, ...);
-void PM_SetErrorMessage(const char *str, ...);
+void PM_PrintToMainLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
+void PM_PrintWarningToMainLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
+void PM_PrintToTechLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
+void PM_SetErrorMessage(const char *str, ...) IS_LIKE_PRINTF(1,2);
 char *PM_GetErrorMessage();
 int store_export_info(int type, jstring fn, JNIEnv *env);
-void export_string(const char *str, ...);
+
+
+void export_string(const char *str, ...) IS_LIKE_PRINTF(1,2);
 bool PM_GetFlagExportIterations();
 
 //------------------------------------------------------------------------------

prism/include/PrismNativeGlob.h

@@ -28,6 +28,7 @@
 #define PRISMNATIVEGLOB_H
 
 //------------------------------------------------------------------------------
+#include <cstdio>
 #include <jni.h>
 
 // Flags for building Windows DLLs
@@ -37,6 +38,35 @@
 	#define EXPORT
 #endif
 
+//------------------------------------------------------------------------------
+
+// macro for attributing printf-like functions to notify the compiler
+// that we'd like to have format string / argument sanity checking
+
+#ifdef __GNUC__
+  // __attribute__ should be supported by compilers that claim to behave like GNU GCC
+
+  // we have to determine the printf format string, as MINGW supports two printf backends
+#if defined(__USE_MINGW_ANSI_STDIO) && __USE_MINGW_ANSI_STDIO
+  // this should be the default for C++
+#define PRISM_PRINTF_FORMAT gnu_printf
+#elif defined(__USE_MINGW_ANSI_STDIO) && !(__USE_MINGW_ANSI_STDIO)
+#define PRISM_PRINTF_FORMAT ms_printf
+#else
+  // normal GCC: use printf as format
+#define PRISM_PRINTF_FORMAT printf
+#endif
+
+// define IS_LIKE_PRINTF, which can be placed after a printf-like function
+// first parameter is index of format string, second parameter is first vararg
+#define IS_LIKE_PRINTF(format_index, first_arg) __attribute__((__format__(PRISM_PRINTF_FORMAT, format_index,first_arg)))
+
+#else // !defined __GNUC__
+// empty IS_LIKE_PRINTF
+#define IS_LIKE_PRINTF(format_index, first_arg)
+#endif
+
+
 //------------------------------------------------------------------------------
 
 // Constants - these need to match the definitions in prism/Prism.java

prism/include/PrismSparseGlob.h

@@ -45,14 +45,14 @@ extern JNIEnv *export_env;
 // macros, function prototypes
 
 #define logtwo(X) log((double)X)/log(2.0)
-void PS_PrintToMainLog(JNIEnv *env, const char *str, ...);
-void PS_PrintWarningToMainLog(JNIEnv *env, const char *str, ...);
-void PS_PrintToTechLog(JNIEnv *env, const char *str, ...);
+void PS_PrintToMainLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
+void PS_PrintWarningToMainLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
+void PS_PrintToTechLog(JNIEnv *env, const char *str, ...) IS_LIKE_PRINTF(2,3);
 void PS_PrintMemoryToMainLog(JNIEnv *env, const char *before, double mem, const char *after);
-void PS_SetErrorMessage(const char *str, ...);
+void PS_SetErrorMessage(const char *str, ...) IS_LIKE_PRINTF(1,2);
 char *PS_GetErrorMessage();
 int store_export_info(int type, jstring fn, JNIEnv *env);
-void export_string(const char *str, ...);
+void export_string(const char *str, ...) IS_LIKE_PRINTF(1,2);
 bool PS_GetFlagExportIterations();
 
 //------------------------------------------------------------------------------