From f18979a429b80d50971bdac880d059d482e7421c Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 4 Sep 2017 18:22:38 +0100 Subject: [PATCH 1/9] Add clang-format config --- .clang-format | 102 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 .clang-format diff --git a/.clang-format b/.clang-format new file mode 100644 index 00000000000..6d8c8f0b034 --- /dev/null +++ b/.clang-format @@ -0,0 +1,102 @@ +--- +AccessModifierOffset: '-2' +AlignAfterOpenBracket: AlwaysBreak +AlignConsecutiveAssignments: 'false' +AlignConsecutiveDeclarations: 'false' +AlignEscapedNewlinesLeft: 'false' +AlignOperands: 'true' +AlignTrailingComments: 'true' +AllowAllParametersOfDeclarationOnNextLine: 'false' +AllowShortBlocksOnASingleLine: 'false' +AllowShortCaseLabelsOnASingleLine: 'false' +AllowShortFunctionsOnASingleLine: None +AllowShortIfStatementsOnASingleLine: 'false' +AllowShortLoopsOnASingleLine: 'false' +AlwaysBreakAfterReturnType: None +AlwaysBreakBeforeMultilineStrings: 'true' +AlwaysBreakTemplateDeclarations: 'true' +BinPackArguments: 'false' +BinPackParameters: 'false' +BreakBeforeBinaryOperators: None +BreakBeforeBraces: Allman +BreakBeforeTernaryOperators: 'true' +BreakConstructorInitializersBeforeComma: 'false' +ColumnLimit: '80' +ConstructorInitializerAllOnOneLineOrOnePerLine: 'true' +ConstructorInitializerIndentWidth: '2' +ContinuationIndentWidth: '2' +Cpp11BracedListStyle: 'true' +DerivePointerAlignment: 'false' +DisableFormat: 'false' +ExperimentalAutoDetectBinPacking: 'false' +ForEachMacros: [ + 'forall_rw_range_set_r_objects', + 'Forall_rw_range_set_r_objects', + 'forall_rw_range_set_w_objects', + 'Forall_rw_range_set_w_objects', + 'forall_rw_set_r_entries', + 'Forall_rw_set_r_entries', + 'forall_rw_set_w_entries', + 'Forall_rw_set_w_entries', + 'forall_goto_functions', + 'Forall_goto_functions', + 'forall_goto_program_instructions', + 'Forall_goto_program_instructions', + 'forall_objects', + 'Forall_objects', + 'forall_valid_objects', + 'Forall_valid_objects', + 'forall_nodes', + 'Forall_nodes', + 'forall_literals', + 'Forall_literals', + 'forall_operands', + 'Forall_operands', + 'forall_expr', + 'Forall_expr', + 'forall_expr_list', + 'Forall_expr_list', + 'forall_symbolptr_list', + 'Forall_symbolptr_list', + 'forall_guard', + 'Forall_guard', + 'forall_irep', + 'Forall_irep', + 'forall_named_irep', + 'Forall_named_irep', + 'forall_value_list', + 'Forall_value_list', + 'forall_symbols', + 'Forall_symbols', + 'forall_symbol_base_map', + 'Forall_symbol_base_map', + 'forall_symbol_module_map', + 'Forall_symbol_module_map', + 'forall_subtypes', + 'Forall_subtypes'] +IndentCaseLabels: 'false' +IndentWidth: '2' +IndentWrappedFunctionNames: 'false' +KeepEmptyLinesAtTheStartOfBlocks: 'false' +Language: Cpp +MaxEmptyLinesToKeep: '1' +NamespaceIndentation: None +PenaltyBreakString: 10000 +PointerAlignment: Right +ReflowComments: 'false' +SortIncludes: 'false' +SpaceAfterCStyleCast: 'false' +SpaceBeforeAssignmentOperators: 'true' +SpaceBeforeParens: Never +SpaceInEmptyParentheses: 'false' +SpacesBeforeTrailingComments: '1' +SpacesInAngles: 'false' +SpacesInCStyleCastParentheses: 'false' +SpacesInContainerLiterals: 'false' +SpacesInParentheses: 'false' +SpacesInSquareBrackets: 'false' +Standard: Cpp11 +TabWidth: '2' +UseTab: Never + +... From 6ce0dba1b35b35b34e3a94f2b7b8a46840cea2d4 Mon Sep 17 00:00:00 2001 From: reuk Date: Sun, 10 Sep 2017 21:42:18 +0100 Subject: [PATCH 2/9] Add travis style check --- .travis.yml | 26 ++++++++++++++++++++++++++ 1 file changed, 26 insertions(+) diff --git a/.travis.yml b/.travis.yml index 6d7c87b854f..6b6d945b645 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,6 +3,32 @@ language: cpp jobs: include: + - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test + env: NAME="clang-format" + addons: + apt: + packages: + - clang-format-3.8 + install: + script: | + # Apparently update-alternatives doesn't work in Travis containers + mkdir -p priority-symlinks + ln -s /usr/bin/clang-format-3.8 priority-symlinks/clang-format + export PATH=${PWD}/priority-symlinks:${PATH} + + # Now we can do the formatting pass + clang-format --version + git-clang-format-3.8 "${TRAVIS_BRANCH}" + git diff --color > formatted.diff + if [[ -s formatted.diff ]] ; then + echo 'Formatting error! Apply the following diff and resubmit:' + cat formatted.diff + exit 1 + fi + echo 'No formatting errors found' + exit 0 + before_cache: + - &linter-stage stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test env: NAME="CPP-LINT" From 554cb54400fd2fe4507a47342e1b0353e1cf6823 Mon Sep 17 00:00:00 2001 From: reuk Date: Sun, 10 Sep 2017 22:10:45 +0100 Subject: [PATCH 3/9] Adjust cpplint to disable whitespace checks by default --- scripts/cpplint.py | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/scripts/cpplint.py b/scripts/cpplint.py index a8b2039c447..0198c57e113 100755 --- a/scripts/cpplint.py +++ b/scripts/cpplint.py @@ -224,8 +224,9 @@ 'readability/inheritance', 'readability/multiline_comment', 'readability/multiline_string', - 'readability/namespace', + 'readability/identifier_spacing', 'readability/identifiers', + 'readability/namespace', 'readability/nolint', 'readability/nul', 'readability/strings', @@ -281,7 +282,12 @@ # flag. By default all errors are on, so only add here categories that should be # off by default (i.e., categories that must be enabled by the --filter= flags). # All entries here should start with a '-' or '+', as in the --filter= flag. -_DEFAULT_FILTERS = ['-build/include_alpha'] +_DEFAULT_FILTERS = [ + '-build/include_alpha', + '-whitespace/', + '-readability/braces', + '-readability/identifier_spacing', + ] # The default list of categories suppressed for C (not C++) files. _DEFAULT_C_SUPPRESSED_CATEGORIES = [ @@ -3624,7 +3630,7 @@ def CheckOperatorSpacing(filename, clean_lines, linenum, error): # check any inherited classes don't have a space between the type and the : if Search(r'(struct|class)\s[\w_]*\s+:', line): - error(filename, linenum, 'readability/identifiers', 4, 'There shouldn\'t be a space between class identifier and :') + error(filename, linenum, 'readability/identifier_spacing', 4, 'There shouldn\'t be a space between class identifier and :') #check type definitions end with t # Look for class declarations and check the final character is a t From 1dcc82cbc59cb526e6846cfc30414ea548ae1733 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 16 Oct 2017 14:26:37 +0100 Subject: [PATCH 4/9] Convert COMPILING to markdown format --- COMPILING => COMPILING.md | 291 +++++++++++++++++--------------------- 1 file changed, 131 insertions(+), 160 deletions(-) rename COMPILING => COMPILING.md (51%) diff --git a/COMPILING b/COMPILING.md similarity index 51% rename from COMPILING rename to COMPILING.md index 2ec4c482bba..ecfe58fdf62 100644 --- a/COMPILING +++ b/COMPILING.md @@ -1,218 +1,198 @@ -What architecture? ------------------- +# What architecture? CPROVER now needs a C++11 compliant compiler and works in the following environments: - Linux - - MacOS X - - Solaris 11 - - FreeBSD 11 +- Cygwin (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or + above.) +- Microsoft's Visual Studio version 12 (2013), version 14 (2015), or version 15 + (older versions won't work) -- Cygwin - (We recommend the i686-pc-mingw32-g++ cross compiler, version 5.4 or above.) - -- Microsoft's Visual Studio version 12 (2013), version 14 (2015), - or version 15 (older versions won't work) - -The rest of this document is split up into three parts: compilation on -Linux, MacOS, Windows. Please read the section appropriate for your -machine. +The rest of this document is split up into three parts: compilation on Linux, +MacOS, Windows. Please read the section appropriate for your machine. - -COMPILATION ON LINUX --------------------- +# COMPILATION ON LINUX We assume that you have a Debian/Ubuntu or Red Hat-like distribution. -0) You need a C/C++ compiler, Flex and Bison, and GNU make. +1. You need a C/C++ compiler, Flex and Bison, and GNU make. The GNU Make needs to be version 3.81 or higher. On Debian-like distributions, do - + ``` apt-get install g++ gcc flex bison make git libwww-perl patch - + ``` On Red Hat/Fedora or derivates, do - + ``` yum install gcc gcc-c++ flex bison perl-libwww-perl patch devtoolset-6 - + ``` Note that you need g++ version 4.9 or newer. - -1) As a user, get the CBMC source via - +2. As a user, get the CBMC source via + ``` git clone https://github.com/diffblue/cbmc cbmc-git - -2) On Debian or Ubuntu, do - + ``` +3. On Debian or Ubuntu, do + ``` cd cbmc-git/src make minisat2-download make - + ``` On Redhat/Fedora etc., do - + ``` cd cbmc-git/src make minisat2-download scl enable devtoolset-6 bash make + ``` +# COMPILATION ON SOLARIS 11 -COMPILATION ON SOLARIS 11 -------------------------- - -1) As root, get the necessary development tools: - +1. As root, get the necessary development tools: + ``` pkg install system/header developer/lexer/flex developer/parser/bison developer/versioning/git pkg install --accept developer/gcc/gcc-c++-5 - -2) As a user, get the CBMC source via - + ``` +2. As a user, get the CBMC source via + ``` git clone https://github.com/diffblue/cbmc cbmc-git - -3) Get MiniSat2 by entering - + ``` +3. Get MiniSat2 by entering + ``` cd cbmc-git wget http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz gtar xfz minisat_2.2.1.orig.tar.gz mv minisat2-2.2.1 minisat-2.2.1 (cd minisat-2.2.1; patch -p1 < ../scripts/minisat-2.2.1-patch) - -4) Type - + ``` +4. Type + ``` cd src; gmake - + ``` That should do it. To run, you will need - + ``` export LD_LIBRARY_PATH=/usr/gcc/4.9/lib + ``` +# COMPILATION ON FREEBSD 11 -COMPILATION ON FREEBSD 11 -------------------------- - -1) As root, get the necessary tools: - +1. As root, get the necessary tools: + ``` pkg install bash gmake git www/p5-libwww patch flex bison - -2) As a user, get the CBMC source via - + ``` +2. As a user, get the CBMC source via + ``` git clone https://github.com/diffblue/cbmc cbmc-git - -3) Do - + ``` +3. Do + ``` cd cbmc-git/src - -4) Do - + ``` +4. Do + ``` gmake minisat2-download gmake + ``` - -COMPILATION ON MACOS X ----------------------- +# COMPILATION ON MACOS X Follow these instructions: -0) You need a C/C++ compiler, Flex and Bison, and GNU make. To this - end, first install the XCode from the App-store and then type - +1. You need a C/C++ compiler, Flex and Bison, and GNU make. To this end, first + install the XCode from the App-store and then type + ``` xcode-select --install - + ``` in a terminal window. - -1) Then get the CBMC source via - +2. Then get the CBMC source via + ``` git clone https://github.com/diffblue/cbmc cbmc-git - -2) Then type - + ``` +3. Then type + ``` cd cbmc-git/src make minisat2-download make + ``` +# COMPILATION ON WINDOWS -COMPILATION ON WINDOWS ----------------------- - -There are two options: compilation using g++ from Cygwin, or using -Visual Studio's compiler. As Cygwin has significant overhead during -process creation, we advise you use Visual Studio. +There are two options: compilation using g++ from Cygwin, or using Visual +Studio's compiler. As Cygwin has significant overhead during process creation, +we advise you use Visual Studio. Follow these instructions: -0) You need a C/C++ compiler, Flex and Bison, GNU tar, gzip2, - GNU make, and patch. The GNU Make needs to be version 3.81 or - higher. If you don't already have the above, we recommend you install - Cygwin. - -1) You need a SAT solver (in source). We recommend MiniSat2. Using a +1. You need a C/C++ compiler, Flex and Bison, GNU tar, gzip2, GNU make, and + patch. The GNU Make needs to be version 3.81 or higher. If you don't + already have the above, we recommend you install Cygwin. +2. You need a SAT solver (in source). We recommend MiniSat2. Using a browser, download from - + ``` http://ftp.debian.org/debian/pool/main/m/minisat2/minisat2_2.2.1.orig.tar.gz - + ``` and then unpack with - + ``` tar xfz minisat-2.2.1.tar.gz mv minisat minisat-2.2.1 cd minisat-2.2.1 patch -p1 < ../scripts/minisat-2.2.1-patch - - The patch removes the dependency on zlib and prevents a problem - with a header file that is often unavailable on Windows. - -2A) To compile with Cygwin, install the mingw compilers, and adjust - the second line of config.inc to say - - BUILD_ENV = MinGW - -2B) To compile with Visual Studio, make sure you have at least Visual - Studio version 12 (2013), and adjust the second line of config.inc to say - - BUILD_ENV = MSVC - - Open the Visual Studio Command prompt, and then bash.exe -login from - Cygwin from in there. - -3) Type cd src; make - that should do it. - + ``` + The patch removes the dependency on zlib and prevents a problem with a + header file that is often unavailable on Windows. + 1. To compile with Cygwin, install the mingw compilers, and adjust + the second line of config.inc to say + ``` + BUILD_ENV = MinGW + ``` + 2. To compile with Visual Studio, make sure you have at least Visual + Studio version 12 (2013), and adjust the second line of config.inc to say + ``` + BUILD_ENV = MSVC + ``` + Open the Visual Studio Command prompt, and then bash.exe -login from + Cygwin from in there. +3. Type cd src; make - that should do it. (Optional) A Visual Studio project file can be generated with the script -"generate_vcxproj" that is in the subdirectory "scripts". The project file -is helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and -can be used for building with MSBuild. Note that you still need to run -flex/bison using "make generated_files" before opening the project. - +"generate_vcxproj" that is in the subdirectory "scripts". The project file is +helpful for GUI-based tasks, e.g., the class viewer, debugging, etc., and can +be used for building with MSBuild. Note that you still need to run flex/bison +using "make generated_files" before opening the project. -WORKING WITH CMAKE (EXPERIMENTAL) ---------------------------------- +# WORKING WITH CMAKE (EXPERIMENTAL) There is an experimental build based on CMake instead of hand-written makefiles. It should work on a wider variety of systems than the standard makefile build, and can integrate better with IDEs and static-analysis tools. -0) Run `cmake --version`. If you get a command-not-found error, or the installed - version is lower than 3.2, go and install a new version. Most Linux - distributions have a package for CMake, and Mac users can get it through - Homebrew. Windows users should download it manually from cmake.org. - -1) Create a directory to store your build: - `mkdir build` +1. Run `cmake --version`. If you get a command-not-found error, or the + installed version is lower than 3.2, go and install a new version. Most + Linux distributions have a package for CMake, and Mac users can get it + through Homebrew. Windows users should download it manually from cmake.org. +2. Create a directory to store your build: + ``` + mkdir build + ``` Run this from the *top level* folder of the project. This is different from the other builds, which require you to `cd src` first. - -2) Generate build files with CMake: - `cmake -H. -Bbuild` +3. Generate build files with CMake: + ``` + cmake -H. -Bbuild + ``` This command tells CMake to use the configuration in the current directory, - and to generate build files into the `build` directory. - This is the point to specify custom build settings, such as compilers and - build back-ends. You can use clang (for example) by adding the argument - `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell - CMake to generate IDE projects by supplying the `-G` flag. - Run `cmake -G` for a comprehensive list of supported back-ends. + and to generate build files into the `build` directory. This is the point + to specify custom build settings, such as compilers and build back-ends. You + can use clang (for example) by adding the argument + `-DCMAKE_CXX_COMPILER=clang++` to the command line. You can also tell CMake + to generate IDE projects by supplying the `-G` flag. Run `cmake -G` for a + comprehensive list of supported back-ends. Generally it is not necessary to manually specify individual compiler or - linker flags, as CMake defines a number of "build modes" including Debug - and Release modes. To build in a particular mode, add the flag + linker flags, as CMake defines a number of "build modes" including Debug and + Release modes. To build in a particular mode, add the flag `-DCMAKE_BUILD_TYPE=Debug` (or `Release`) to the initial invocation. If you *do* need to manually add flags, use `-DCMAKE_CXX_FLAGS=...` and @@ -222,44 +202,35 @@ makefile build, and can integrate better with IDEs and static-analysis tools. Finally, to enable building universal binaries on macOS, you can pass the flag `-DCMAKE_OSX_ARCHITECTURES=i386;x86_64`. If you don't supply this flag, the build will just be for the architecture of your machine. - -3) Run the build: - `cmake --build build` +4. Run the build: + ``` + cmake --build build + ``` This command tells CMake to invoke the correct tool to run the build in the `build` directory. You can also use the build back-end directly by invoking `make`, `ninja`, or opening the generated IDE project as appropriate. - -WORKING WITH ECLIPSE --------------------- +# WORKING WITH ECLIPSE To work with Eclipse, do the following: -1) Select File -> New -> Makefile Project with Existing Code - -2) Type "cprover" as "Project Name" - -3) Select the "src" subdirectory as "Existing Code Location" - -4) Select a toolchain appropriate for your platform - -5) Click "Finish" - -6) Select Project -> Build All - - -CODE COVERAGE -------------- - -Code coverage metrics are provided using gcov and lcov. Ensure that you -have installed lcov from http://ltp.sourceforge.net/coverage/lcov.php -note for ubuntu lcov is available in the standard apt-get repos. +1. Select File -> New -> Makefile Project with Existing Code +2. Type "cprover" as "Project Name" +3. Select the "src" subdirectory as "Existing Code Location" +4. Select a toolchain appropriate for your platform +5. Click "Finish" +6. Select Project -> Build All -To get coverage metrics run the following script from the regression -directory: +# CODE COVERAGE - get_coverage.sh +Code coverage metrics are provided using gcov and lcov. Ensure that you have +installed lcov from http://ltp.sourceforge.net/coverage/lcov.php note for +ubuntu lcov is available in the standard apt-get repos. +To get coverage metrics run the following script from the regression directory: +``` +get_coverage.sh +``` This will: 1) Rebuild CBMC with gcov enabled 2) Run all the regression tests From 8482b353cbcb9d6028cf692f135ee836ac941592 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 16 Oct 2017 14:28:38 +0100 Subject: [PATCH 5/9] Add information about using clang-format --- COMPILING.md | 72 +++++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 71 insertions(+), 1 deletion(-) diff --git a/COMPILING.md b/COMPILING.md index ecfe58fdf62..cb3ee1e1321 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -1,4 +1,4 @@ -# What architecture? +# WHAT ARCHITECTURE? CPROVER now needs a C++11 compliant compiler and works in the following environments: @@ -236,3 +236,73 @@ This will: 2) Run all the regression tests 3) Collate the coverage metrics 4) Provide an HTML report of the current coverage + +# USING CLANG-FORMAT + +CBMC uses clang-format to ensure that the formatting of new patches is readable +and consistent. There are two main ways of running clang-format: remotely, and +locally. + +## RUNNING CLANG-FORMAT REMOTELY + +When patches are submitted to CBMC, they are automatically run through +continuous integration (CI). One of the CI checks will run clang-format over +the diff that your pull request introduces. If clang-format finds formatting +issues at this point, the build will be failed, and a patch will be produced +in the CI output that you can apply to your code so that it conforms to the +style guidelines. + +To apply the patch, copy and paste it into a local file (`patch.txt`) and then +run: +``` +patch -p1 -i patch.txt +``` +Now, you can commit and push the formatting fixes. + +## RUNNING CLANG-FORMAT LOCALLY + +### INSTALLATION + +To avoid waiting until you've made a PR to find formatting issues, you can +install clang-format locally and run it against your code as you are working. + +Different versions of clang-format have slightly different behaviors. CBMC uses +clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and +Homebrew. +To install, run: +``` +sudo apt install clang-format-3.8 # Run this on Ubuntu, Debian etc. +brew install clang-format-3.8 # Run this on a Mac with Homebrew installed +``` + +### FORMATTING A RANGE OF COMMITS + +Clang-format is distributed with a driver script called git-clang-format-3.8. +This script can be used to format git diffs (rather than entire files). + +After committing some code, it is recommended to run: +``` +git-clang-format-3.8 upstream/develop +``` +*Important:* If your branch is based on a branch other than `upstream/develop`, +use the name or checksum of that branch instead. It is strongly recommended to +rebase your work onto the tip of the branch it's based on before running +`git-clang-format` in this way. + +### RETROACTIVELY FORMATTING INDIVIDUAL COMMITS + +If your works spans several commits and you'd like to keep the formatting +correct in each individual commit, you can automatically rewrite the commits +with correct formatting. + +The following command will stop at each commit in the range and run +clang-format on the diff at that point. This rewrites git history, so it's +*unsafe*, and you should back up your branch before running this command: +``` +git filter-branch --tree-filter 'git-clang-format-3.8 upstream/develop' \ + -- upstream/develop..HEAD +``` +*Important*: `upstream/develop` should be changed in *both* places in the +command above if your work is based on a different branch. It is strongly +recommended to rebase your work onto the tip of the branch it's based on before +running `git-clang-format` in this way. From 9d4b827dfc5c9366fb722e90bda54826d9a92c2b Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 16 Oct 2017 14:34:49 +0100 Subject: [PATCH 6/9] Update coding standard --- CODING_STANDARD.md | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/CODING_STANDARD.md b/CODING_STANDARD.md index 3b62c9b45e4..c5d67173e14 100644 --- a/CODING_STANDARD.md +++ b/CODING_STANDARD.md @@ -1,6 +1,10 @@ Here a few minimalistic coding rules for the CPROVER source tree. # Whitespaces + +Formatting is enforced using clang-format. For more information about this, see +`COMPILING.md`. A brief summary of the formatting rules is given below: + - Use 2 spaces indent, no tabs. - No lines wider than 80 chars. - When line is wider, do the following: @@ -16,8 +20,7 @@ Here a few minimalistic coding rules for the CPROVER source tree. even if the outer function call does. - If a method is bigger than 50 lines, break it into parts. - Put matching `{ }` into the same column. -- No spaces around operators (`=`, `+`, `==` ...) Exceptions: Spaces around - `&&`, `||` and `<<` +- Spaces around binary operators (`=`, `+`, `==` ...) - Space after comma (parameter lists, argument lists, ...) - Space after colon inside `for` - For pointers and references, the `*`/`&` should be attached to the variable @@ -27,10 +30,10 @@ Here a few minimalistic coding rules for the CPROVER source tree. - No whitespaces in blank lines - Put argument lists on next line (and indent 2 spaces) if too long - Put parameters on separate lines (and indent 2 spaces) if too long -- No whitespaces around colon for inheritance, put inherited into separate - lines in case of multiple inheritance -- The initializer list follows the constructor without a whitespace around the - colon. Break line after the colon if required and indent members. +- Spaces around colon for inheritance, put inherited into separate lines in + case of multiple inheritance +- The initializer list follows the constructor with a whitespace around the + colon. - `if(...)`, `else`, `for(...)`, `do`, and `while(...)` are always in a separate line - Break expressions in `if`, `for`, `while` if necessary and align them with From 55e6594d04f3753b3089db9a4944d0eee53ee7b4 Mon Sep 17 00:00:00 2001 From: reuk Date: Mon, 16 Oct 2017 14:57:33 +0100 Subject: [PATCH 7/9] Fixup cpplint.py --- scripts/cpplint.py | 7 +------ scripts/run_diff.sh | 4 ++-- 2 files changed, 3 insertions(+), 8 deletions(-) diff --git a/scripts/cpplint.py b/scripts/cpplint.py index 0198c57e113..2e8a5582842 100755 --- a/scripts/cpplint.py +++ b/scripts/cpplint.py @@ -282,12 +282,7 @@ # flag. By default all errors are on, so only add here categories that should be # off by default (i.e., categories that must be enabled by the --filter= flags). # All entries here should start with a '-' or '+', as in the --filter= flag. -_DEFAULT_FILTERS = [ - '-build/include_alpha', - '-whitespace/', - '-readability/braces', - '-readability/identifier_spacing', - ] +_DEFAULT_FILTERS = ['-build/include_alpha'] # The default list of categories suppressed for C (not C++) files. _DEFAULT_C_SUPPRESSED_CATEGORIES = [ diff --git a/scripts/run_diff.sh b/scripts/run_diff.sh index 56eeb2f3aa8..dd0aa5c2f08 100755 --- a/scripts/run_diff.sh +++ b/scripts/run_diff.sh @@ -37,7 +37,7 @@ then echo "Ensure cpplint.py is inside the $script_folder directory then run again" exit 1 else - cmd='${script_folder}/cpplint.py $file 2>&1 >/dev/null' + cmd='${script_folder}/cpplint.py --filter=-whitespace/operators,-readability/identifier_spacing $file 2>&1 >/dev/null' fi elif [[ "$mode" == "DOXYGEN" ]] then @@ -109,7 +109,7 @@ for file in $diff_files; do # Run the linting script and filter: # The errors from the linter go to STDERR so must be redirected to STDOUT - result=$(eval $cmd | "${script_folder}/filter_by_lines.py" "$file" "$added_lines_file" "$absolute_repository_root") + result=$(eval "${cmd}" | "${script_folder}/filter_by_lines.py" "$file" "$added_lines_file" "$absolute_repository_root") # Providing some errors were relevant we print them out if [ "$result" ] From a24ac3d7ee8a37a20cb4754927bd098c78398980 Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 19 Oct 2017 10:02:27 +0100 Subject: [PATCH 8/9] Fixup compiling.md with more clang-format install instructions --- COMPILING.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/COMPILING.md b/COMPILING.md index cb3ee1e1321..b6003e4ee89 100644 --- a/COMPILING.md +++ b/COMPILING.md @@ -269,12 +269,20 @@ install clang-format locally and run it against your code as you are working. Different versions of clang-format have slightly different behaviors. CBMC uses clang-format-3.8 as it is available the repositories for Ubuntu 16.04 and Homebrew. -To install, run: +To install on a Unix-like system, try installing using the system package +manager: ``` -sudo apt install clang-format-3.8 # Run this on Ubuntu, Debian etc. -brew install clang-format-3.8 # Run this on a Mac with Homebrew installed +apt-get install clang-format-3.8 # Run this on Ubuntu, Debian etc. +brew install clang-format@3.8 # Run this on a Mac with Homebrew installed ``` +If your platform doesn't have a package for clang-format, you can download a +pre-built binary, or compile clang-format yourself using the appropriate files +from the [LLVM Downloads page](http://releases.llvm.org/download.html). + +An installer for Windows (along with a Visual Studio plugin) can be found at +the [LLVM Snapshot Builds page](http://llvm.org/builds/). + ### FORMATTING A RANGE OF COMMITS Clang-format is distributed with a driver script called git-clang-format-3.8. From 2110cd1ccbb81050ec0ce2932b3896baf455b42d Mon Sep 17 00:00:00 2001 From: reuk Date: Thu, 19 Oct 2017 10:16:02 +0100 Subject: [PATCH 9/9] Make formatting stage non-blocking on Travis --- .travis.yml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 6b6d945b645..0b70b485c53 100644 --- a/.travis.yml +++ b/.travis.yml @@ -3,7 +3,8 @@ language: cpp jobs: include: - - stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test + - &formatting-stage + stage: Linter + Doxygen + non-debug Ubuntu/gcc-5 test env: NAME="clang-format" addons: apt: @@ -191,6 +192,7 @@ jobs: script: echo "This is coverity build. No need for tests." allow_failures: + - <<: *formatting-stage - <<: *linter-stage install: