diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index 4d57b09da31..06c6bf53666 100644 --- a/CODING_STANDARD.md +++ b/CODING_STANDARD.md @@ -107,6 +107,9 @@ Here a few minimalistic coding rules for the CPROVER source tree. include in the source file. For example, given `foo.h` and `foo.cpp`, the line `#include "foo.h"` should precede all other include statements in `foo.cpp`. +- Use the C++ versions of C headers (e.g. `cmath` instead of `math.h`). + Some of the C headers use macros instead of functions which can have + unexpected consequences. # Makefiles - Each source file should appear on a separate line diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp index 154ba29c558..ba9fb9ac857 100644 --- a/src/util/ieee_float.cpp +++ b/src/util/ieee_float.cpp @@ -8,9 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "ieee_float.h" -// is yet to come -#include - +#include #include #include #include diff --git a/src/util/pipe_stream.cpp b/src/util/pipe_stream.cpp index 4306bce8e00..1ed29eb415c 100644 --- a/src/util/pipe_stream.cpp +++ b/src/util/pipe_stream.cpp @@ -23,9 +23,9 @@ Module: A stdin/stdout pipe as STL stream #else #include #include -#include #include #include +#include #endif #define READ_BUFFER_SIZE 1024