Cpplint fix

.githooks/pre-commit

@@ -0,0 +1,50 @@
+#!/bin/bash
+# Runs scripts/cpplint.py on the modified files
+# Based on https://github.com/s0enke/git-hooks/
+#
+# @author Peter Schrammel <peter.schrammel@diffblue.com>
+
+gitRoot="$(dirname $0)/../.."
+
+# this is the magic:
+# retrieve all files in staging area that are added, modified or renamed
+# but no deletions etc
+files=$(git diff-index --name-only --cached --diff-filter=ACMR HEAD -- )
+
+if [ "$files" == "" ]; then
+    exit 0
+fi
+
+# create temporary copy of staging area and delete upon exit
+cleanup()
+{
+  rm -rf $tmpStaging
+}
+
+trap cleanup EXIT
+
+tmpStaging=$(mktemp -d)
+
+# Copy contents of staged version of files to temporary staging area
+# because we only want the staged version that will be commited and not
+# the version in the working directory
+stagedFiles=""
+for file in $files
+do
+  id=$(git diff-index --cached HEAD $file | cut -d " " -f4)
+
+  # create staged version of file in temporary staging area with the same
+  # path as the original file
+  mkdir -p "$tmpStaging/$(dirname $file)"
+  git cat-file blob $id > "$tmpStaging/$file"
+  stagedFiles="$stagedFiles $tmpStaging/$file"
+done
+
+output=$(cd $gitRoot; python scripts/cpplint.py $stagedFiles 2>&1)
+retval=$?
+
+if [ $retval -ne 0 ]
+then
+    echo "$output"
+    exit 1
+fi

CODING_STANDARD

@@ -3,10 +3,22 @@ Here a few minimalistic coding rules for the CPROVER source tree.
 Whitespaces:
 - Use 2 spaces indent, no tabs.
 - No lines wider than 80 chars.
+  - When line is wider, do the following:
+    - Subsequent lines should be indented two more than the initial line
+    - Break after = if it is part of an assignment
+    - For chained calls, prefer immediately before .
+    - For other operators (e.g. &&, +) prefer immediately after the operator
+    - For brackets, break after the bracket
+      - In the case of function calls, put each argument on a separate line if
+        they do not fit after one line break
 - If a method is bigger than 50 lines, break it into parts.
 - Put matching { } into the same column.
-- No spaces around operators, except &&, ||, and <<
-- Spaces after , and ; inside 'for'
+- No spaces around operators (=, +, ==, ...)
+  Exceptions: Spaces around &&, || and <<
+- Space after comma (parameter lists, argument lists, ...)
+- Space after colon inside 'for'
+- No whitespaces at end of line
+- No whitespaces in blank lines
 - Put argument lists on next line (and ident 2 spaces) if too long
 - Put parameters on separate lines (and ident 2 spaces) if too long
 - No whitespaces around colon for inheritance, 
@@ -16,8 +28,6 @@ Whitespaces:
 - if(...), else, for(...), do, and while(...) are always in a separate line
 - Break expressions in if, for, while if necessary and align them 
   with the first character following the opening parenthesis
-- No whitespaces at end of line
-- Avoid whitespaces in blank lines
 - Use {} instead of ; for the empty statement
 - Single line blocks without { } are allowed, 
   but put braces around multi-line blocks
@@ -29,9 +39,31 @@ Comments:
 - Do not use /* */ except for file and function comment blocks
 - Each source and header file must start with a comment block 
   stating the Module name and Author [will be changed when we roll out doxygen]
-- Each function in the source file (not the header) is preceded 
-  by a comment block stating Name, Inputs,  Outputs and Purpose [will be changed
-  when we roll out doxygen]
+- Each function in the source file (not the header) is preceded
+  by a function comment header consisting of a comment block stating
+  Name, Inputs,  Outputs and Purpose [will be changed when we roll
+  out doxygen]
+   - It should look like this:
+   ```
+   /*******************************************************************\
+
+   Function: class_namet::function_name
+
+    Inputs:
+     arg_name - Description of its purpose
+     long_arg_name - Descriptions should be indented
+                     to match the first line of the
+                     description
+
+    Outputs: A description of what the function returns
+
+    Purpose: A description of what the function does.
+             Again, indentation with the line above
+
+   \*******************************************************************/
+   ```
+- An empty line should appear between the bottom of the function comment header
+  and the function.
 - Put comments on a separate line
 - Use comments to explain the non-obvious
 - Use #if 0 for commenting out source code
@@ -51,6 +83,8 @@ Naming:
 
 Header files:
 - Avoid unnecessary #includes, especially in header files
+- Prefer forward declaration to includes, but forward declare at the top
+  of the header file rather than in line
 - Guard headers with #ifndef CPROVER_DIRECTORIES_FILE_H, etc
 
 C++ features:
@@ -85,6 +119,9 @@ C++ features:
 - We allow to use 3rd-party libraries directly. 
   No wrapper matching the coding rules is required. 
   Allowed libraries are: STL. 
+- Use the auto keyword if and only if one of the following
+  - The type is explictly repeated on the RHS (e.g. a constructor call)
+  - Adding the type will increase confusion (e.g. iterators, function pointers)
 
 Architecture-specific code:
 - Avoid if possible.

regression/cpp-linter/Makefile

@@ -0,0 +1,20 @@
+default: tests.log
+
+test:
+	@if ! ../test.pl -c python ../../../scripts/cpplint.py ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c "python ../../../scripts/cpplint.py" ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;

regression/cpp-linter/catch-cast/main.cpp

@@ -0,0 +1,24 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+/*******************************************************************\
+
+Function: fun
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void fun()
+{
+  catch(int)
+}

regression/cpp-linter/catch-cast/test.desc

@@ -0,0 +1,6 @@
+CORE
+main.cpp
+
+^EXIT=0$
+^SIGNAL=0$
+--

regression/cpp-linter/class-decl-space/main.cpp

@@ -0,0 +1,10 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+class temp_classt : public base_classt
+{}

regression/cpp-linter/class-decl-space/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.cpp
+
+^main\.cpp:9:  There shouldn.t be a space between class identifier and :  \[readability/identifiers\] \[4\]$
+^Total errors found: 1$
+^SIGNAL=0$
+--

regression/cpp-linter/do-while1/main.cpp

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+/*******************************************************************\
+
+Function: fun
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void fun()
+{
+  // This should not produce a warning
+  do
+  {
+    int x=0;
+  }
+  while(a);
+
+  // This should
+  while(b);
+
+  // As should this
+  if(true)
+  {
+    do_something();
+  }
+  while(c);
+}

regression/cpp-linter/do-while1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^main\.cpp:31:  Empty loop bodies should use {} or continue  \[whitespace/empty_loop_body\] \[5\]$
+^main\.cpp:38:  Empty loop bodies should use {} or continue  \[whitespace/empty_loop_body\] \[5\]$
+^Total errors found: 2$
+^SIGNAL=0$
+--

regression/cpp-linter/do-while2/main.cpp

@@ -0,0 +1,27 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+/*******************************************************************\
+
+Function: fun
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void fun()
+{
+  do
+  {
+    int x=0;
+  } while(a);
+}

regression/cpp-linter/do-while2/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.cpp
+
+^main\.cpp:26:  while statement of do...while loop should be on a separate line to the closing brace  \[readability/braces\] \[4\]
+^Total errors found: 1$
+^SIGNAL=0$
+--

regression/cpp-linter/function-comment-header1/main.cpp

@@ -0,0 +1,30 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+/*******************************************************************\
+
+Function: fun
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void fun()
+{
+  do_something();
+}
+
+static void foo()
+{
+  // No function header
+  do_something();
+}

regression/cpp-linter/function-comment-header1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.cpp
+
+^main\.cpp:26:  Could not find function header comment for foo  \[readability/function_comment\] \[4\]
+^Total errors found: 1$
+
+^SIGNAL=0$
+--

regression/cpp-linter/function-comment-header2/main.cpp

@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+/*******************************************************************\
+
+Function: fun
+
+\*******************************************************************/
+
+static void fun()
+{
+  do_something();
+}

regression/cpp-linter/function-comment-header2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.cpp
+
+main\.cpp:15:  Function header for fun missing Inputs:  \[readability/function_comment\] \[4\]
+main\.cpp:15:  Function header for fun missing Outputs:  \[readability/function_comment\] \[4\]
+main\.cpp:15:  Function header for fun missing Purpose:  \[readability/function_comment\] \[4\]
+^Total errors found: 3$
+^SIGNAL=0$
+--

regression/cpp-linter/function-comment-header3/main.cpp

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Lint Examples
+
+Author: Thomas Kiley, thomas@diffblue.com
+
+\*******************************************************************/
+
+/*******************************************************************\
+
+Function: fun
+
+ Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+static void fun()
+{
+  do_something();
+}

regression/cpp-linter/function-comment-header3/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.cpp
+
+^main\.cpp:20:  Insert an empty line between function header comment and the function fun  \[readability/function_comment\] \[4\]$
+^Total errors found: 1$
+^SIGNAL=0$
+--