From: Andres Noetzli Date: Mon, 17 May 2021 16:52:55 +0000 (-0700) Subject: Include cinttypes instead of inttypes.h (#6548) X-Git-Tag: cvc5-1.0.0~1756 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eed22b44b92d14be51f82e4871c926dee79eaf3a;p=cvc5.git Include cinttypes instead of inttypes.h (#6548) This commit changes the includes used by MiniSat. This commit changes the includes from stdint.h/inttypes.h/limits.h to cstdint/cinttypes/climits. This ensures that the macros in cinttypes/inttypes.h, e.g., `PRIi64`, are actually defined. The C99 standard suggested that those macros are only defined for C++ code when `__STDC_FORMAT_MACROS` is defined. This was never adopted by a C++ standard (https://en.cppreference.com/w/cpp/types/integer). However, certain versions of mingw-w64 seem to require it with inttypes.h but not cinttypes. This fixes the nightly Windows build (tested in the Docker container used by the nightlies). --- diff --git a/src/prop/bvminisat/mtl/IntTypes.h b/src/prop/bvminisat/mtl/IntTypes.h index 19ca38bea..7856dc07c 100644 --- a/src/prop/bvminisat/mtl/IntTypes.h +++ b/src/prop/bvminisat/mtl/IntTypes.h @@ -30,12 +30,20 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #else -# include -# include +// In contrast to the original MiniSat source code, we are including the +// cstdint/cinttypes/climits headers instead of stdint.h/inttypes.h/limits.h +// here. This ensures that the macros in cinttypes/inttypes.h, e.g., PRIi64, +// are actually defined. The C99 standard suggested that those macros are only +// defined for C++ code when __STDC_FORMAT_MACROS is defined. This was never +// adopted by a C++ standard (https://en.cppreference.com/w/cpp/types/integer). +// However, certain versions of mingw-w64 seem to require it with inttypes.h +// but not cinttypes. +# include +# include #endif -#include +#include //================================================================================================= diff --git a/src/prop/minisat/mtl/IntTypes.h b/src/prop/minisat/mtl/IntTypes.h index c48816284..f1fc84163 100644 --- a/src/prop/minisat/mtl/IntTypes.h +++ b/src/prop/minisat/mtl/IntTypes.h @@ -30,12 +30,20 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #else -# include -# include +// In contrast to the original MiniSat source code, we are including the +// cstdint/cinttypes/climits headers instead of stdint.h/inttypes.h/limits.h +// here. This ensures that the macros in cinttypes/inttypes.h such as PRIi64 +// are actually defined. The C99 standard suggested that those macros are only +// defined for C++ code when __STDC_FORMAT_MACROS is defined. This was never +// adopted by a C++ standard (https://en.cppreference.com/w/cpp/types/integer). +// However, certain versions of mingw-w64 seem to require it with inttypes.h +// but not cinttypes. +# include +# include #endif -#include +#include //=================================================================================================