From 548aeba6b9db02ddfe26ac6ddb4c079ae1284768 Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 4 Aug 2017 14:48:48 +0100 Subject: [PATCH 1/2] Stop using C headers --- src/util/ieee_float.cpp | 4 +--- src/util/pipe_stream.cpp | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) 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 From 33811ce31d488789899ba6b4ad7b4fb5ecaf8730 Mon Sep 17 00:00:00 2001 From: reuk Date: Fri, 4 Aug 2017 14:53:24 +0100 Subject: [PATCH 2/2] Update coding standard --- CODING_STANDARD.md | 3 +++ 1 file changed, 3 insertions(+) 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