Add the Catch unit testing framework #874

thk123 · 2017-04-26T12:58:27Z

Adds catch.hpp - a test harness for writing and running unit tests. Updated the make file so that running make test runs all the tests. I removed all the tests that either didn't compile, failing on running or
didn't terminate without some input.

Added an example catch test to demonstrate it working.

Updated one of the unit tests to use catch as a demonstration (I can do the others in the next sprint if it is deemed important).

NathanJPhillips

Big request is to split the changes to sharing_map.cpp into three commits, one to indent, one to move and one to actually make the changes. That way I can review the last one properly. Understand if that feels like too much work though.

NathanJPhillips · 2017-04-26T13:10:30Z

CODING_STANDARD

+Unit tests:
+ - Unit tests are written using Catch: https://github.com/philsquared/Catch/
+ - For large classes:
+    - Each file should contain tests for one function in one class


Suggested clarity rewording:
Create a separate file that contains the tests for each method of each class

I've just edited my suggestion again, which shows that it's hard to find clear wording for this!

NathanJPhillips · 2017-04-26T13:13:10Z

CODING_STANDARD

+    - Each file should contain tests for one function in one class
+    - The file should be put inside unit/class/path/class_name/function_name.cpp
+ - For small classes:
+    - Each file should contain the tests for the class


Create a separate file that contains the tests for all methods of each class

NathanJPhillips · 2017-04-26T13:13:34Z

CODING_STANDARD

+    - Each file should contain the tests for the class
+    - The file should be put inside unit/class/path/class_name.cpp
+ - Catch supports tagging, tests should be tagged with:
+    - [CORE] or [LONG] if the test takes a long time to run


Perhaps explain the difference between these tags.

NathanJPhillips · 2017-04-26T13:14:10Z

unit/Makefile

      # Empty last line

-INCLUDES= -I ../src/
+INCLUDES= -I ../src/ -I.


Do we really need this? It seems like a bad thing.

I thought this is needed so that include paths can be relative to the root of the unit directory, is that not true?

For example, each of the Makefiles for each CBMC module does INCLUDE= -I .. to get the src directory included.

But then that should be the INCLUDES as is; the -I. seems wrong.

I think you need to think about what the current working directory will be when the actual compile command is run and make the include paths relative to this. But if it's working already then maybe I'm wrong. If I'm not then this setting might need to be in the makefile in each sub-folder.

OK, I understand what is going on. This makefile is directly building source files in sub-folders that include files in this folder using #include <catch.hpp>. In that case this is the right syntax. As you were.

NathanJPhillips · 2017-04-26T13:15:03Z

unit/Makefile

+catch: catch_entry_point$(EXEEXT)
+
+# Run the catch tests
+test-catch: catch


This rule should not be named for the unit test framework. unit-test or unit might be better names.

Technically all the tests in here are unit tests, the only difference is these are catch unit tests. We could just remove the rule since I've removed tests that don't actually pass.

NathanJPhillips · 2017-04-26T13:17:38Z

unit/catch_example.cpp

+/// This is an example unit test to demonstrate the build system and the
+/// catch unit test framework. The source code is taken from the documentation
+/// of catch.
+///


This comment block is not in a standard format. If you want to include the example you probably need to DiffBlue-ise it.

NathanJPhillips · 2017-04-26T13:21:33Z

unit/sharing_map.cpp


-  // place elements
+TEST_CASE("sharing map", "[core][util][sharing_map]")


Unfortunately this file is impossible to diff because of the change in indenting. Can you split the changes into one that does the change and then one that indents it out correctly (or one that indents it out wrongly and then one that does the change)?

I have just learnt the magic of ?w=1 and the diff looks fine on this file.

NathanJPhillips · 2017-04-26T13:22:27Z

unit/Makefile

@@ -1,5 +1,5 @@
 CATCH_TESTS = catch_example.cpp \
-              sharing_map.cpp \
+              util/sharing_map.cpp \


This change is in the wrong commit (will mess up git blame).

tautschnig · 2017-04-26T16:35:19Z

unit/Makefile

      miniBDD.cpp \
-      osx_fat_reader.cpp \


Dangling files aren't great. (Yes, effectively the entire directory had been dangling.) Any chance to get those fixed instead?

Unfortunately I don't have time to fix these at the moment, I have opened an issue to resolve this: #879. Would you prefer the files to be deleted (I'll attach them to the issue) so they aren't dangling?

Thanks for logging #879; I think it's good enough this way, no need to delete files.

thk123 · 2017-04-28T11:40:48Z

I have applied Nathan's suggestions and fixed the linting errors. Hopefully I've got the travis file right this time. I still suspect the Makefile could be improved as the way the CBMC libraries are linked in feels a bit clunky, but I don't know how to improve it. I will squash after review so easier to see what changes have been made.

NathanJPhillips · 2017-04-28T16:25:35Z

Do remember to ignore your executable output in a local .gitignore.

thk123 · 2017-04-28T16:49:37Z

.gitignore

Done

Rename exe

Done

Assuming I have finally got the travis and appveyor things correct - I will rebase this on Tuesday.

thk123 · 2017-05-04T08:50:32Z

@forejtv This is failing on Mac because of your unit test - could you investigate? https://travis-ci.org/diffblue/cbmc/jobs/228295412#L2395

Still investigating why the Windows build is failing, it is something to do with the sharing map so I might just pull that into a separate PR so can get this merged.

thk123 · 2017-05-04T12:03:39Z

I have dropped the commits relating to the sharing_map unit tests into a separate PR: #887

Assuming @forejtv can address the Mac issue this should now pass CI.

thk123 · 2017-05-05T14:50:58Z

The windows one is now also failing on the unicode test

thk123 · 2017-05-08T09:33:33Z

As discussed with @forejtv I have removed the unicode tests (that failed on Mac, noted on #879) and this now builds so I think should be mergable.

NathanJPhillips

Couple of minor suggestions but otherwise good to merge.

NathanJPhillips · 2017-05-08T09:38:42Z

CODING_STANDARD

+ - For large classes:
+    - Create a separate file that contains the tests for each method of each
+      class
+    - The file should be put inside unit/class/path/class_name/function_name.cpp


The file should be named according to unit/class/path/class_name/function_name.cpp

NathanJPhillips · 2017-05-08T09:42:46Z

CODING_STANDARD

+    - Create a separate file that contains the tests for all methods of each
+      class
+    - The file should be put inside unit/class/path/class_name.cpp
+ - Catch supports tagging, tests should be tagged with:


with all the following tags:

NathanJPhillips · 2017-05-08T09:44:07Z

unit/.gitignore

+float_utils
+json
+miniBDD
+osx_fat_reader


Are all of these still created?

thk123 · 2017-05-08T10:29:40Z

@NathanJPhillips Thanks, fixed.

thk123 · 2017-05-09T09:38:19Z

I think the Makefile might still not be correct as if I clean CBMC then do a clean build of the unit, it appears to try and build the unit tests in parallel to the CBMC directory. I think the all rule should be:

all: cprover.dir
	$(TESTS)

Does this make sense to someone who know's make files?(!) ~~It appears to be work for a clean rebuild.~~

As an aside, would you expect make -C unit clean to clean the src directory as well?

tautschnig · 2017-05-09T09:47:34Z

A rule all: cprover.dir $(TESTS) will make all depend on both cprover.dir and $(TESTS), but will not yield any dependency or order between them. You'll likely need an additional rule $(TESTS): cprover.dir.

thk123 · 2017-05-09T11:52:30Z

@tautschnig This didn't work exactly (by adding that dependency, the $(LINKBIN) was trying to compile cprover.dir which makes no sense. In the end we did:

all: cprover.dir
	$(MAKE) $(MAKEARGS) $(TESTS)

Adds catch.hpp - a test harness for writing and running unit tests. Updated the make file so that running `make test` runs all the tests. I removed all the tests that either didn't compile, failing on running or didn't terminate without some input. Added an example catch test to demonstrate it working.

Added running unit tests to the Travis and AppVeyor yml files

Moved the sharing map test into the appropriate folder

peterschrammel · 2017-05-12T16:48:52Z

unit/catch_example.cpp

+
+ Module: Example Catch Tests
+
+ Author: DiffBlue Limited. All rights reserved.


I suggest to put your name as author until we have a common copyright header.

peterschrammel · 2017-05-12T16:55:24Z

unit/Makefile


-CLEANFILES = $(SRC:.cpp=$(EXEEXT))
+TESTS = catch_entry_point$(EXEEXT) \


Is there a better way to specify which tests (not) to run?

All the Catch tests get compiled into one executable, so the only way to remove them will be to modify the source of the test or remove them from the SRC list above I believe.

peterschrammel · 2017-05-12T22:54:20Z

unit/Makefile

@@ -1,6 +1,6 @@
 .PHONY: all cprover.dir test

-SRC = catch_entry_point.cpp \
+SRC = unit_tests.cpp \


Is it possible to specify the tests to build and execute in a way that does not require to add them in three different places?

My understanding is that the test is catch_example, which is only specified once, in SRC. That's where extra tests will be added. The other executables here will be migrated to the Catch framework over time and be removed from this makefile.

Is the plan to put all tests into a single cpp file?

Multiple cpp files, since executable is my understanding.

peterschrammel · 2017-05-15T09:50:06Z

Ok, #887 should then replace the dummy catch_example. Or better integrate #887 into this PR to have at least one real use case. The dummy example is then obsolete and need not be committed into the code base.

peterschrammel · 2017-05-15T15:02:50Z

Since the cleanup of #887 will take a considerable amount of time, I suggest to get this merged as is, and do the porting of the existing tests in follow-up PRs.

NathanJPhillips suggested changes Apr 26, 2017

View reviewed changes

tautschnig reviewed Apr 26, 2017

View reviewed changes

thk123 force-pushed the feature/unit-test-framework branch from 420babb to e9a6824 Compare April 28, 2017 11:38

thk123 force-pushed the feature/unit-test-framework branch from e2de329 to 1a4a9ac Compare April 28, 2017 11:44

thk123 force-pushed the feature/unit-test-framework branch from 48d6e70 to 22a0505 Compare May 3, 2017 11:15

tautschnig mentioned this pull request May 3, 2017

replace assert() #182

Closed

thk123 force-pushed the feature/unit-test-framework branch from 22a0505 to 2d5bac3 Compare May 4, 2017 11:59

thk123 mentioned this pull request May 4, 2017

Sharing Map Unit Tests #887

Closed

thk123 force-pushed the feature/unit-test-framework branch from 2d5bac3 to 66bccf0 Compare May 5, 2017 13:33

thk123 force-pushed the feature/unit-test-framework branch 2 times, most recently from fb3ccdf to ca6e2b3 Compare May 8, 2017 09:17

NathanJPhillips approved these changes May 8, 2017

View reviewed changes

thk123 force-pushed the feature/unit-test-framework branch from ca6e2b3 to a4af717 Compare May 8, 2017 10:29

thk123 force-pushed the feature/unit-test-framework branch from a4af717 to 3b79d6c Compare May 9, 2017 11:48

thk123 mentioned this pull request May 9, 2017

[depends: #472] Variable Sensitivity Domain #708

Closed

thk123 added 4 commits May 10, 2017 09:12

Add unit tests to the CI files

de73265

Added running unit tests to the Travis and AppVeyor yml files

Updated coding standard to explain unit testing

b22210d

Moved the sharing map test into the appropriate folder

Renamed exe and added exes to gitignore

760e1fc

thk123 force-pushed the feature/unit-test-framework branch from 3b79d6c to 760e1fc Compare May 10, 2017 08:12

thk123 mentioned this pull request May 12, 2017

goto-instrument --remove-function-body #730

Merged

peterschrammel reviewed May 12, 2017

View reviewed changes

NathanJPhillips mentioned this pull request May 15, 2017

Move existing unit tests to Catch #921

Closed

peterschrammel approved these changes May 15, 2017

View reviewed changes

peterschrammel assigned kroening May 15, 2017

kroening merged commit 7e1ba16 into diffblue:master May 15, 2017

thk123 deleted the feature/unit-test-framework branch May 16, 2017 12:22


		// place elements
		TEST_CASE("sharing map", "[core][util][sharing_map]")


		Module: Example Catch Tests

		Author: DiffBlue Limited. All rights reserved.


		CLEANFILES = $(SRC:.cpp=$(EXEEXT))
		TESTS = catch_entry_point$(EXEEXT) \

Add the Catch unit testing framework #874

Add the Catch unit testing framework #874

Conversation

thk123 commented Apr 26, 2017

NathanJPhillips left a comment

Choose a reason for hiding this comment

NathanJPhillips Apr 26, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

NathanJPhillips Apr 26, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented Apr 28, 2017 • edited Loading

NathanJPhillips commented Apr 28, 2017

thk123 commented Apr 28, 2017

thk123 commented May 4, 2017

thk123 commented May 4, 2017

thk123 commented May 5, 2017

thk123 commented May 8, 2017

NathanJPhillips left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

thk123 commented May 8, 2017

thk123 commented May 9, 2017 • edited Loading

tautschnig commented May 9, 2017

thk123 commented May 9, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

peterschrammel commented May 15, 2017

peterschrammel commented May 15, 2017

NathanJPhillips Apr 26, 2017 •

edited

Loading

NathanJPhillips Apr 26, 2017 •

edited

Loading

thk123 commented Apr 28, 2017 •

edited

Loading

thk123 commented May 9, 2017 •

edited

Loading