Add the Catch unit testing framework

.travis.yml

@@ -152,6 +152,9 @@ script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
     COMMAND="env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test" &&
     eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C unit CXX=\"$COMPILER\" CXXFLAGS=\"$FLAGS $EXTRA_CXXFLAGS\" -j2" &&
+    eval ${PRE_COMMAND} ${COMMAND}
+  - COMMAND="make -C unit test" && eval ${PRE_COMMAND} ${COMMAND}
 
 before_cache:
   - ccache -s

CODING_STANDARD

@@ -26,23 +26,23 @@ Whitespaces:
 - 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, 
+- 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.
 - if(...), else, for(...), do, and while(...) are always in a separate line
-- Break expressions in if, for, while if necessary and align them 
+- Break expressions in if, for, while if necessary and align them
   with the first character following the opening parenthesis
 - Use {} instead of ; for the empty statement
-- Single line blocks without { } are allowed, 
+- Single line blocks without { } are allowed,
   but put braces around multi-line blocks
-- Use blank lines to visually separate logically cohesive code blocks 
+- Use blank lines to visually separate logically cohesive code blocks
   within a function
 - Have a newline at the end of a file
 
 Comments:
 - Do not use /* */ except for file and function comment blocks
-- Each source and header file must start with a comment block 
+- 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 function comment header consisting of a comment block stating
@@ -75,9 +75,9 @@ Comments:
 - Use #ifdef DEBUG to guard debug code
 
 Naming:
-- Identifiers may use the characters [a-z0-9_] and should start with a 
+- Identifiers may use the characters [a-z0-9_] and should start with a
   lower-case letter (parameters in constructors may start with _).
-- Use american spelling for identifiers. 
+- Use american spelling for identifiers.
 - Separate basic words by _
 - Avoid abbreviations (e.g. prefer symbol_table to of st).
 - User defined type identifiers have to be terminated by 't'. Moreover,
@@ -136,7 +136,7 @@ C++ features:
 - Avoid iterators, use ranged for instead
 - Avoid allocation with new/delete, use unique_ptr
 - Avoid pointers, use references
-- Avoid char *, use std::string 
+- Avoid char *, use std::string
 - For numbers, use int, unsigned, long, unsigned long, double
 - Use mp_integer, not BigInt
 - Use the functions in util for conversions between numbers and strings
@@ -146,13 +146,13 @@ C++ features:
 - Use instances of std::size_t for comparison with return values of .size() of
   STL containers and algorithms, and use them as indices to arrays or vectors.
 - Do not use default values in public functions
-- Use assertions to detect programming errors, e.g. whenever you make 
+- Use assertions to detect programming errors, e.g. whenever you make
   assumptions on how your code is used
-- Use exceptions only when the execution of the program has to abort 
+- Use exceptions only when the execution of the program has to abort
   because of erroneous user input
-- We allow to use 3rd-party libraries directly. 
-  No wrapper matching the coding rules is required. 
-  Allowed libraries are: STL. 
+- We allow to use 3rd-party libraries directly.
+  No wrapper matching the coding rules is required.
+  Allowed libraries are: STL.
 - When throwing, omit the brackets, i.e. `throw "error"`.
 - Error messages should start with a lower case letter.
 - Use the auto keyword if and only if one of the following
@@ -165,12 +165,30 @@ Architecture-specific code:
 - Don't include architecture-specific header files without #ifdef ...
 
 Output:
-- Do not output to cout or cerr directly (except in temporary debug code, 
+- Do not output to cout or cerr directly (except in temporary debug code,
   and then guard #include <iostream> by #ifdef DEBUG)
 - Derive from messaget if the class produces output and use the streams provided
   (status(), error(), debug(), etc)
 - Use '\n' instead of std::endl
 
+Unit tests:
+ - Unit tests are written using Catch: https://github.com/philsquared/Catch/
+ - For large classes:
+    - Create a separate file that contains the tests for each method of each
+      class
+    - The file should be named according to
+      `unit/class/path/class_name/function_name.cpp`
+ - For small classes:
+    - Create a separate file that contains the tests for all methods of each
+      class
+    - The file should be named according to unit/class/path/class_name.cpp
+ - Catch supports tagging, tests should be tagged with all the following tags:
+    - [core] should be used for all tests unless the test takes more than 1
+      second to run, then it should be tagged with [long]
+    - [folder_name] of the file being tested
+    - [class_name] of the class being tested
+    - [function_name] of the function being tested
+
 You are allowed to break rules if you have a good reason to do so.
 
 Pre-commit hook to run cpplint locally

appveyor.yml

@@ -108,3 +108,7 @@ test_script:
     rmdir /s /q goto-instrument\slice08
 
     make test
+
+    cd ..
+    make -C unit all
+    make -C unit test

unit/.gitignore

@@ -0,0 +1,5 @@
+# Unit test binaries
+miniBDD
+sharing_node
+string_utils
+unit_tests

unit/Makefile

@@ -1,24 +1,17 @@
-SRC = cpp_parser.cpp \
-      cpp_scanner.cpp \
-      elf_reader.cpp \
-      float_utils.cpp \
-      ieee_float.cpp \
-      json.cpp \
-      miniBDD.cpp \
-      osx_fat_reader.cpp \
-      sharing_map.cpp \
-      sharing_node.cpp \
-      smt2_parser.cpp \
-      string_utils.cpp \
-      unicode.cpp \
-      wp.cpp \
+.PHONY: all cprover.dir test
+
+SRC = unit_tests.cpp \
+      catch_example.cpp \
       # Empty last line
 
-INCLUDES= -I ../src/
+INCLUDES= -I ../src/ -I.
 
 include ../src/config.inc
 include ../src/common
 
+cprover.dir:
+	$(MAKE) $(MAKEARGS) -C ../src
+
 LIBS = ../src/ansi-c/ansi-c$(LIBEXT) \
        ../src/cpp/cpp$(LIBEXT) \
        ../src/json/json$(LIBEXT) \
@@ -31,52 +24,33 @@ LIBS = ../src/ansi-c/ansi-c$(LIBEXT) \
        ../src/assembler/assembler$(LIBEXT) \
        ../src/analyses/analyses$(LIBEXT) \
        ../src/solvers/solvers$(LIBEXT) \
+       # Empty last line
 
-CLEANFILES = $(SRC:.cpp=$(EXEEXT))
+TESTS = unit_tests$(EXEEXT) \
+        miniBDD$(EXEEXT) \
+        string_utils$(EXEEXT) \
+        sharing_node$(EXEEXT) \
+        # Empty last line
 
-all: $(SRC:.cpp=$(EXEEXT))
+CLEANFILES = $(TESTS)
 
-###############################################################################
+all: cprover.dir
+	$(MAKE) $(MAKEARGS) $(TESTS)
 
-cpp_parser$(EXEEXT): cpp_parser$(OBJEXT)
-	$(LINKBIN)
+test: all
+	$(foreach test,$(TESTS), (echo Running: $(test); ./$(test)) &&) true
 
-cpp_scanner$(EXEEXT): cpp_scanner$(OBJEXT)
-	$(LINKBIN)
 
-elf_reader$(EXEEXT): elf_reader$(OBJEXT)
-	$(LINKBIN)
-
-float_utils$(EXEEXT): float_utils$(OBJEXT)
-	$(LINKBIN)
-
-ieee_float$(EXEEXT): ieee_float$(OBJEXT)
-	$(LINKBIN)
+###############################################################################
 
-json$(EXEEXT): json$(OBJEXT)
+unit_tests$(EXEEXT): $(OBJ)
 	$(LINKBIN)
 
 miniBDD$(EXEEXT): miniBDD$(OBJEXT)
 	$(LINKBIN)
 
-osx_fat_reader$(EXEEXT): osx_fat_reader$(OBJEXT)
-	$(LINKBIN)
-
-smt2_parser$(EXEEXT): smt2_parser$(OBJEXT)
-	$(LINKBIN)
-
-wp$(EXEEXT): wp$(OBJEXT)
-	$(LINKBIN)
-
 string_utils$(EXEEXT): string_utils$(OBJEXT)
 	$(LINKBIN)
 
-sharing_map$(EXEEXT): sharing_map$(OBJEXT)
-	$(LINKBIN)
-
 sharing_node$(EXEEXT): sharing_node$(OBJEXT)
 	$(LINKBIN)
-
-unicode$(EXEEXT): unicode$(OBJEXT)
-	$(LINKBIN)
-