From: makaimann <makaim@stanford.edu>
Date: Fri, 12 May 2017 19:47:16 +0000 (-0700)
Subject: Conditional coverage build
X-Git-Tag: cvc5-1.0.0~5794^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=220d8a9cf8706bdf28162ff452f58f1262ba691d;p=cvc5.git

Conditional coverage build
---

diff --git a/configure.ac b/configure.ac
index 7da86d8a8..e94733576 100644
--- a/configure.ac
+++ b/configure.ac
@@ -720,6 +720,9 @@ AC_ARG_ENABLE([coverage],
 
 if test -z "${enable_coverage+set}"; then
   enable_coverage=no
+  # make COVERAGE_ON the empty string for makefile conditional function
+  # $(if $(COVERAGE_ON), action1, action2)
+  COVERAGE_ON=
 fi
 
 AC_MSG_RESULT([$enable_coverage])
@@ -730,6 +733,7 @@ if test "$enable_coverage" = yes; then
   # If the user didn't specify these, we force them here.  If the
   # user specified them in opposite phase, give warnings that they
   # shouldn't do that, or bomb out.
+  COVERAGE_ON=yes
   if test "$user_specified_enable_or_disable_shared" != yes; then
     enable_shared=no
     AC_MSG_WARN([turning off shared library building due to --enable-coverage])
@@ -1263,6 +1267,7 @@ AC_SUBST(BUILDING_STATIC)
 AC_SUBST(STATIC_BINARY)
 AM_CONDITIONAL([STATIC_BINARY], [test "$enable_static_binary" = yes])
 AM_CONDITIONAL([COVERAGE_ENABLED], [test "$enable_coverage" = yes])
+AC_SUBST([COVERAGE_ON])
 
 AM_CONDITIONAL([CVC4_DEBUG], [test "$with_build" = debug])
 AM_CONDITIONAL([CVC4_TRACING], [test "$enable_tracing" = yes])
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index d5f8de462..1334a8804 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -1,19 +1,15 @@
-# Forcing some make variables to be actual absolute paths to fix Coverage
+# if coverage is enabled:
+# COVERAGE_ON = yes from configure.ac
+# Using an inline conditional function to choose between absolute and
+# relative paths for options files
 # lcov does not support relative paths and src/options and src/expr
 # in particular were breaking it
-# Note: variable declarations may be moved in generated Makefile
-# see src/expr/Makefile.am
-
-VPATH = $(realpath @srcdir@)
-srcdir = $(realpath @srcdir@)
-abs_srcdir = $(realpath @abs_srcdir@)
-abs_top_srcdir = $(realpath @abs_top_srcdir@)
-top_srcdir = $(realpath @top_srcdir@)
-
+# Building with coverage will cause portability issues in some cases
 
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I$(realpath @builddir@/..) -I$(realpath @srcdir@/../include) -I$(realpath @srcdir@/..)
+	$(if $(COVERAGE_ON), -I@abs_builddir@/.. -I@abs_srcdir@/../include -I@abs_srcdir@/.., \
+	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..)
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = libexpr.la
@@ -134,13 +130,13 @@ CLEANFILES = \
 $(top_builddir)/src/expr/.subdirs: $(top_srcdir)/src/Makefile.theories  @top_srcdir@/src/mksubdirs
 	$(AM_V_at)test -d $(top_builddir)/src/expr || mkdir $(top_builddir)/src/expr
 	$(AM_V_at)chmod +x @top_srcdir@/src/mksubdirs
-	$(AM_V_at)( @top_srcdir@/src/mksubdirs "$(top_srcdir)" ) > $(top_builddir)/src/expr/.subdirs.tmp
+	$(AM_V_at)( @top_srcdir@/src/mksubdirs $(if $(COVERAGE_ON), "$(abs_top_srcdir)", "$(top_srcdir)")) > $(top_builddir)/src/expr/.subdirs.tmp
 	@if ! diff -q $(top_builddir)/src/expr/.subdirs $(top_builddir)/src/expr/.subdirs.tmp &>/dev/null; then \
 		echo "  GEN   " $@; \
 		$(am__mv) $(top_builddir)/src/expr/.subdirs.tmp $(top_builddir)/src/expr/.subdirs; \
 	fi
 
-kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkkind
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkkind \
@@ -148,7 +144,7 @@ kind.h: kind_template.h mkkind @top_builddir@/src/expr/.subdirs @top_srcdir@/src
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkmetakind
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkmetakind \
@@ -156,7 +152,7 @@ metakind.h: metakind_template.h mkmetakind @top_builddir@/src/expr/.subdirs @top
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkkind
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkkind \
@@ -164,7 +160,7 @@ type_properties.h: type_properties_template.h mkkind @top_builddir@/src/expr/.su
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-expr.h: expr_template.h mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.h: expr_template.h mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -172,7 +168,7 @@ expr.h: expr_template.h mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -180,7 +176,7 @@ expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -188,7 +184,7 @@ expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/expr/.subdirs
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -196,7 +192,7 @@ expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/expr/.subd
 		`cat @top_builddir@/src/expr/.subdirs` \
 	> $@) || (rm -f $@ && exit 1)
 
-type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/expr/.subdirs @top_srcdir@/src/theory/*/kinds
+type_checker.cpp: type_checker_template.cpp mkexpr @top_builddir@/src/expr/.subdirs $(if $(COVERAGE_ON), @abs_top_srcdir@, @top_srcdir@)/src/theory/*/kinds
 	$(AM_V_at)chmod +x @srcdir@/mkexpr
 	$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
 	$(AM_V_GEN)(@srcdir@/mkexpr \
diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index 2d4fcc436..bca6ca16e 100644
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -12,17 +12,14 @@
 #   This stage also waits for X_options.h as otherwise it cannot compile.
 #
 
-# Forcing some make variables to be actual absolute paths to fix Coverage
+# if coverage is enabled:
+# COVERAGE_ON = yes from configure.ac
+# Using an inline conditional function to choose between absolute and
+# relative paths for options files
 # lcov does not support relative paths and src/options and src/expr
 # in particular were breaking it
-# Note: variable declarations may be moved in generated Makefile
-# see src/options/Makefile.am
+# Building with coverage will cause portability issues in some cases
 
-VPATH = $(realpath @srcdir@)
-srcdir = $(realpath @srcdir@)
-abs_srcdir = $(realpath @abs_srcdir@)
-abs_top_srcdir = $(realpath @abs_top_srcdir@)
-top_srcdir = $(realpath @top_srcdir@)
 
 OPTIONS_SRC_FILES = \
 	arith_options \
@@ -212,7 +209,8 @@ DOCUMENTATION_TEMPLATE_SEDS = \
 
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-	-I$(realpath @builddir@/..) -I$(realpath @srcdir@/../include) -I$(realpath @srcdir@/..)
+	$(if $(COVERAGE_ON), -I@abs_builddir@/.. -I@abs_srcdir@/../include -I@abs_srcdir@/.., \
+	-I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..)
 AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 noinst_LTLIBRARIES = liboptions.la
@@ -320,7 +318,7 @@ arith_options arrays_options base_options booleans_options builtin_options bv_op
 # Make is happier being listed explictly. Not sure why.
 arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sep_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp:
 	echo "$@" "$(@:.tmp=)"
-	$(AM_V_GEN)(cp "$(realpath @srcdir@/$(@:.tmp=))" "$@" || true)
+	$(AM_V_GEN)(cp $(if $(COVERAGE_ON), "@abs_srcdir@/$(@:.tmp=)", "@srcdir@/$(@:.tmp=)") "$@" || true)
 #TIM:
 #The (... || true) here is to make distcheck not fail.
 
@@ -333,38 +331,38 @@ arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp built
 # We use the updating of %_options.options to signal that the options file updated.
 # However, we use the original file in src to generate the file.
 %_options.sed: %_options.options mkoptions
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) module-sed "$(realpath @srcdir@/$(@:.sed=))" ) > "$@"
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions module-sed $(if $(COVERAGE_ON), "@abs_srcdir@/$(@:.sed=)", "@srcdir@/$(@:.sed=)")) > "$@"
 
 
 $(CPP_TEMPLATE_SEDS): %.sed : % mkoptions
 #	echo "template seds"
 #	echo "$@"
 #	echo $(TEMPLATE_SEDS)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) template-sed "$<" ) > "$@"
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@"
 
 $(DOCUMENTATION_TEMPLATE_SEDS): %.sed : % mkoptions
 #	echo "template seds"
 #	echo "$@"
 #	echo $(TEMPLATE_SEDS)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) template-sed "$<" ) > "$@"
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@"
 
 %_options.h : %_options.sed mkoptions base_options_template.h base_options_template.h.sed
 #	echo heads
 #	echo "$@"
 #	echo $(OPTIONS_HEADS)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
-		$(realpath @srcdir@/base_options_template.h) \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+		$(if $(COVERAGE_ON), @abs_srcdir@, @srcdir@)/base_options_template.h \
 		base_options_template.h.sed \
 		"$<" \
 	) > "$@"
 
 summary.sed : mkoptions $(OPTIONS_OPTIONS_FILES)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) summary-sed \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions summary-sed \
 		$(OPTIONS_OPTIONS_FILES) \
 	) > summary.sed
 
@@ -372,18 +370,18 @@ summary.sed : mkoptions $(OPTIONS_OPTIONS_FILES)
 
 #   mkoptions apply-sed-to-template sed-file template-file
 options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions $(OPTIONS_HEADS)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
-		$(realpath @srcdir@/options_holder_template.h) \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+		$(if $(COVERAGE_ON), @abs_srcdir@, @srcdir@)/options_holder_template.h \
 		@builddir@/options_holder_template.h.sed \
 		summary.sed \
 	) > "$@"
 
 # Make sure not to match with "options.cpp" too.
 %_options.cpp: %_options.sed %_options.h mkoptions options_holder.h base_options_template.cpp base_options_template.cpp.sed
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
-		$(realpath @srcdir@/base_options_template.cpp) \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+		$(if $(COVERAGE_ON), @abs_srcdir@, @srcdir@)/base_options_template.cpp \
 		base_options_template.cpp.sed \
 		"$<" \
 	) > "$@"
@@ -393,9 +391,9 @@ options_holder.h : options_holder_template.h options_holder_template.h.sed summa
 
 #   mkoptions apply-sed-to-template sed-file template-file
 options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) options_holder.h
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
-		$(realpath @srcdir@/options_template.cpp) \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+		$(if $(COVERAGE_ON), @abs_srcdir@, @srcdir@)/options_template.cpp \
 		@builddir@/options_template.cpp.sed \
 		summary.sed \
 	) > "$@"
@@ -403,17 +401,17 @@ options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.se
 
 #   mkoptions apply-sed-to-template sed-file template-file
 options_get_option.cpp : options_get_option_template.cpp options_get_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
-		$(realpath @srcdir@/options_get_option_template.cpp) \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+		$(if $(COVERAGE_ON), @abs_srcdir@, @srcdir@)/options_get_option_template.cpp \
 		@builddir@/options_get_option_template.cpp.sed \
 		summary.sed \
 	) > "$@"
 
 options_set_option.cpp : options_set_option_template.cpp options_set_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS)
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
-		$(realpath @srcdir@/options_set_option_template.cpp) \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+		$(if $(COVERAGE_ON), @abs_srcdir@, @srcdir@)/options_set_option_template.cpp \
 		@builddir@/options_set_option_template.cpp.sed \
 		summary.sed \
 	) > "$@"
@@ -423,8 +421,8 @@ options_set_option.cpp : options_set_option_template.cpp options_set_option_temp
 $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed
 #	echo "$<"
 #	echo "$@"
-	$(AM_V_at)chmod +x $(realpath @srcdir@/mkoptions)
-	$(AM_V_GEN)($(realpath @srcdir@/mkoptions) apply-sed-files-to-template \
+	$(AM_V_at)chmod +x @srcdir@/mkoptions
+	$(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
 		"$<" \
 		"$<".sed \
 		@builddir@/summary.sed \