Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add the Catch unit testing framework #874

Merged
merged 4 commits into from
May 15, 2017
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
68 changes: 21 additions & 47 deletions unit/Makefile
Original file line number Diff line number Diff line change
@@ -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 \
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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?

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

sharing_map.cpp \
sharing_node.cpp \
smt2_parser.cpp \
string_utils.cpp \
unicode.cpp \
wp.cpp \
.PHONY: all cprover.dir test

SRC = catch_entry_point.cpp \
catch_example.cpp \
# Empty last line

INCLUDES= -I ../src/
INCLUDES= -I ../src/ -I.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.


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) \
Expand All @@ -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 = catch_entry_point$(EXEEXT) \
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

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)
catch_entry_point$(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)

Loading