Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/base/configuration.cpp	Lines:	110	130	84.6 %
Date:	2021-09-30	Branches:	119	292	40.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Aina Niemetz, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Implementation of Configuration class, which provides compile-time
 * configuration information about the cvc5 library.
 */
#include "base/configuration.h"

#include <stdlib.h>
#include <string.h>

#include <algorithm>
#include <sstream>
#include <string>

#include "base/Debug_tags.h"
#include "base/Trace_tags.h"
#include "base/configuration_private.h"
#include "base/cvc5config.h"

using namespace std;

namespace cvc5 {

string Configuration::getName() { return CVC5_PACKAGE_NAME; }

bool Configuration::isDebugBuild() {
  return IS_DEBUG_BUILD;
}

bool Configuration::isTracingBuild() {
  return IS_TRACING_BUILD;
}

bool Configuration::isDumpingBuild() {
  return IS_DUMPING_BUILD && !IS_MUZZLED_BUILD;
}

bool Configuration::isMuzzledBuild() {
  return IS_MUZZLED_BUILD;
}

bool Configuration::isAssertionBuild() {
  return IS_ASSERTIONS_BUILD;
}

bool Configuration::isCoverageBuild() {
  return IS_COVERAGE_BUILD;
}

bool Configuration::isProfilingBuild() {
  return IS_PROFILING_BUILD;
}

bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }

bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }

bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }

bool Configuration::isCompetitionBuild() {
  return IS_COMPETITION_BUILD;
}

bool Configuration::isStaticBuild()
{
#if defined(CVC5_STATIC_BUILD)
  return true;
#else
  return false;
#endif
}

string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }

string Configuration::getVersionString() { return CVC5_RELEASE_STRING; }

unsigned Configuration::getVersionMajor() { return CVC5_MAJOR; }

unsigned Configuration::getVersionMinor() { return CVC5_MINOR; }

unsigned Configuration::getVersionRelease() { return CVC5_RELEASE; }

std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; }

std::string Configuration::copyright() {
  std::stringstream ss;
  ss << "Copyright (c) 2009-2021 by the authors and their institutional\n"
     << "affiliations listed at https://cvc5.github.io/people.html\n\n";

  if (Configuration::licenseIsGpl()) {
    ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n"
       << "the GNU General Public License (GPL) version 3.  Versions of cvc5\n"
       << "are available that are covered by the (modified) BSD license. If\n"
       << "you want to license cvc5 under this license, please configure cvc5\n"
       << "with the \"--no-gpl\" option before building from sources.\n\n";
  } else {
    ss << "cvc5 is open-source and is covered by the BSD license (modified)."
       << "\n\n";
  }

  ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n"
     << "USE AT YOUR OWN RISK.\n\n";

  ss << "cvc5 incorporates code from ANTLR3 (http://www.antlr.org).\n"
     << "See licenses/antlr3-LICENSE for copyright and licensing information."
     << "\n\n";

  ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
     << "third party libraries.\n\n";

  ss << "  CaDiCaL - Simplified Satisfiability Solver\n"
     << "  See https://github.com/arminbiere/cadical for copyright "
     << "information.\n\n";

  if (Configuration::isBuiltWithAbc()
      || Configuration::isBuiltWithCryptominisat()
      || Configuration::isBuiltWithKissat()
      || Configuration::isBuiltWithEditline())
  {
    if (Configuration::isBuiltWithAbc()) {
      ss << "  ABC - A System for Sequential Synthesis and Verification\n"
         << "  See http://bitbucket.org/alanmi/abc for copyright and\n"
         << "  licensing information.\n\n";
    }
    if (Configuration::isBuiltWithCryptominisat())
    {
      ss << "  CryptoMiniSat - An Advanced SAT Solver\n"
         << "  See https://github.com/msoos/cryptominisat for copyright "
         << "information.\n\n";
    }
    if (Configuration::isBuiltWithKissat())
    {
      ss << "  Kissat - Simplified Satisfiability Solver\n"
         << "  See https://fmv.jku.at/kissat for copyright "
         << "information.\n\n";
    }
    if (Configuration::isBuiltWithEditline())
    {
      ss << "  Editline Library\n"
         << "  See https://thrysoee.dk/editline\n"
         << "  for copyright information.\n\n";
    }
  }

  ss << "  SymFPU - The Symbolic Floating Point Unit\n"
     << "  See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
     << "information.\n\n";

  if (Configuration::isBuiltWithGmp() || Configuration::isBuiltWithPoly())
  {
    ss << "This version of cvc5 is linked against the following third party\n"
       << "libraries covered by the LGPLv3 license.\n"
       << "See licenses/lgpl-3.0.txt for more information.\n\n";
    if (Configuration::isBuiltWithGmp()) {
      ss << "  GMP - Gnu Multi Precision Arithmetic Library\n"
         << "  See http://gmplib.org for copyright information.\n\n";
    }
    if (Configuration::isBuiltWithPoly())
    {
      ss << "  LibPoly polynomial library\n"
         << "  See https://github.com/SRI-CSL/libpoly for copyright and\n"
         << "  licensing information.\n\n";
    }
    if (Configuration::isStaticBuild())
    {
      ss << "cvc5 is statically linked against these libraries. To recompile\n"
            "this version of cvc5 with different versions of these libraries\n"
            "follow the instructions on "
            "https://github.com/cvc5/cvc5/blob/master/INSTALL.md\n\n";
    }
  }

  if (Configuration::isBuiltWithCln()
      || Configuration::isBuiltWithGlpk ()) {
    ss << "This version of cvc5 is linked against the following third party\n"
       << "libraries covered by the GPLv3 license.\n"
       << "See licenses/gpl-3.0.txt for more information.\n\n";
    if (Configuration::isBuiltWithCln()) {
      ss << "  CLN - Class Library for Numbers\n"
         << "  See http://www.ginac.de/CLN for copyright information.\n\n";
    }
    if (Configuration::isBuiltWithGlpk()) {
      ss << "  glpk-cut-log - a modified version of GPLK, "
         << "the GNU Linear Programming Kit\n"
         << "  See http://github.com/timothy-king/glpk-cut-log for copyright"
         << " information\n\n";
    }
  }

  ss << "See the file COPYING (distributed with the source code, and with\n"
     << "all binaries) for the full cvc5 copyright, licensing, and (lack of)\n"
     << "warranty information.\n";
  return ss.str();
}

std::string Configuration::about() {
  std::stringstream ss;
  ss << "This is cvc5 version " << CVC5_RELEASE_STRING;
  if (Configuration::isGitBuild()) {
    ss << " [" << Configuration::getGitId() << "]";
  }
  ss << "\ncompiled with " << Configuration::getCompiler()
     << "\non " << Configuration::getCompiledDateTime() << "\n\n";
  ss << Configuration::copyright ();
  return ss.str();
}

bool Configuration::licenseIsGpl() {
  return IS_GPL_BUILD;
}

bool Configuration::isBuiltWithGmp() {
  return IS_GMP_BUILD;
}

bool Configuration::isBuiltWithCln() {
  return IS_CLN_BUILD;
}

bool Configuration::isBuiltWithGlpk() {
  return IS_GLPK_BUILD;
}

bool Configuration::isBuiltWithAbc() {
  return IS_ABC_BUILD;
}

bool Configuration::isBuiltWithCryptominisat() {
  return IS_CRYPTOMINISAT_BUILD;
}

bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }

bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }

bool Configuration::isBuiltWithPoly()
{
  return IS_POLY_BUILD;
}

const std::vector<std::string>& Configuration::getDebugTags()
{
  return Debug_tags;
}

bool Configuration::isDebugTag(const std::string& tag)
{
  return std::find(Debug_tags.begin(), Debug_tags.end(), tag)
         != Debug_tags.end();
}

const std::vector<std::string>& Configuration::getTraceTags()
{
  return Trace_tags;
}

bool Configuration::isTraceTag(const std::string& tag)
{
  return std::find(Trace_tags.begin(), Trace_tags.end(), tag)
         != Trace_tags.end();
}

bool Configuration::isGitBuild() {
  return IS_GIT_BUILD;
}

const char* Configuration::getGitBranchName() {
  return GIT_BRANCH_NAME;
}

const char* Configuration::getGitCommit() {
  return GIT_COMMIT;
}

bool Configuration::hasGitModifications() {
  return GIT_HAS_MODIFICATIONS;
}

std::string Configuration::getGitId() {
  if(! isGitBuild()) {
    return "";
  }

  const char* branchName = getGitBranchName();
  if(*branchName == '\0') {
    branchName = "-";
  }

  stringstream ss;
  ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
     << (::cvc5::Configuration::hasGitModifications() ? " (with modifications)"
                                                      : "");
  return ss.str();
}

std::string Configuration::getCompiler() {
  stringstream ss;
#ifdef __GNUC__
  ss << "GCC";
#else /* __GNUC__ */
  ss << "unknown compiler";
#endif /* __GNUC__ */
#ifdef __VERSION__
  ss << " version " << __VERSION__;
#else /* __VERSION__ */
  ss << ", unknown version";
#endif /* __VERSION__ */
  return ss.str();
}

std::string Configuration::getCompiledDateTime() {
  return __DATE__ " " __TIME__;
}

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Morgan Deters, Aina Niemetz, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* Implementation of Configuration class, which provides compile-time
14		* configuration information about the cvc5 library.
15		*/
16		#include "base/configuration.h"
17
18		#include <stdlib.h>
19		#include <string.h>
20
21		#include <algorithm>
22		#include <sstream>
23		#include <string>
24
25		#include "base/Debug_tags.h"
26		#include "base/Trace_tags.h"
27		#include "base/configuration_private.h"
28		#include "base/cvc5config.h"
29
30		using namespace std;
31
32		namespace cvc5 {
33
34	3	string Configuration::getName() { return CVC5_PACKAGE_NAME; }
35
36	26338	bool Configuration::isDebugBuild() {
37	26338	return IS_DEBUG_BUILD;
38		}
39
40	2630	bool Configuration::isTracingBuild() {
41	2630	return IS_TRACING_BUILD;
42		}
43
44	2630	bool Configuration::isDumpingBuild() {
45	2630	return IS_DUMPING_BUILD && !IS_MUZZLED_BUILD;
46		}
47
48	6705	bool Configuration::isMuzzledBuild() {
49	6705	return IS_MUZZLED_BUILD;
50		}
51
52	2390017	bool Configuration::isAssertionBuild() {
53	2390017	return IS_ASSERTIONS_BUILD;
54		}
55
56	2630	bool Configuration::isCoverageBuild() {
57	2630	return IS_COVERAGE_BUILD;
58		}
59
60	2630	bool Configuration::isProfilingBuild() {
61	2630	return IS_PROFILING_BUILD;
62		}
63
64	2628	bool Configuration::isAsanBuild() { return IS_ASAN_BUILD; }
65
66	2628	bool Configuration::isUbsanBuild() { return IS_UBSAN_BUILD; }
67
68	2628	bool Configuration::isTsanBuild() { return IS_TSAN_BUILD; }
69
70	2628	bool Configuration::isCompetitionBuild() {
71	2628	return IS_COMPETITION_BUILD;
72		}
73
74	2631	bool Configuration::isStaticBuild()
75		{
76		#if defined(CVC5_STATIC_BUILD)
77	2631	return true;
78		#else
79		return false;
80		#endif
81		}
82
83	2	string Configuration::getPackageName() { return CVC5_PACKAGE_NAME; }
84
85	2631	string Configuration::getVersionString() { return CVC5_RELEASE_STRING; }
86
87	2630	unsigned Configuration::getVersionMajor() { return CVC5_MAJOR; }
88
89	2630	unsigned Configuration::getVersionMinor() { return CVC5_MINOR; }
90
91	2630	unsigned Configuration::getVersionRelease() { return CVC5_RELEASE; }
92
93		std::string Configuration::getVersionExtra() { return CVC5_EXTRAVERSION; }
94
95	2631	std::string Configuration::copyright() {
96	5262	std::stringstream ss;
97		ss << "Copyright (c) 2009-2021 by the authors and their institutional\n"
98	2631	<< "affiliations listed at https://cvc5.github.io/people.html\n\n";
99
100	2631	if (Configuration::licenseIsGpl()) {
101		ss << "This build of cvc5 uses GPLed libraries, and is thus covered by\n"
102		<< "the GNU General Public License (GPL) version 3. Versions of cvc5\n"
103		<< "are available that are covered by the (modified) BSD license. If\n"
104		<< "you want to license cvc5 under this license, please configure cvc5\n"
105	2631	<< "with the \"--no-gpl\" option before building from sources.\n\n";
106		} else {
107		ss << "cvc5 is open-source and is covered by the BSD license (modified)."
108		<< "\n\n";
109		}
110
111		ss << "THIS SOFTWARE IS PROVIDED AS-IS, WITHOUT ANY WARRANTIES.\n"
112	2631	<< "USE AT YOUR OWN RISK.\n\n";
113
114		ss << "cvc5 incorporates code from ANTLR3 (http://www.antlr.org).\n"
115		<< "See licenses/antlr3-LICENSE for copyright and licensing information."
116	2631	<< "\n\n";
117
118		ss << "This version of cvc5 is linked against the following non-(L)GPL'ed\n"
119	2631	<< "third party libraries.\n\n";
120
121		ss << " CaDiCaL - Simplified Satisfiability Solver\n"
122		<< " See https://github.com/arminbiere/cadical for copyright "
123	2631	<< "information.\n\n";
124
125	5262	if (Configuration::isBuiltWithAbc()
126	2631	\|\| Configuration::isBuiltWithCryptominisat()
127		\|\| Configuration::isBuiltWithKissat()
128	2631	\|\| Configuration::isBuiltWithEditline())
129		{
130	2631	if (Configuration::isBuiltWithAbc()) {
131		ss << " ABC - A System for Sequential Synthesis and Verification\n"
132		<< " See http://bitbucket.org/alanmi/abc for copyright and\n"
133		<< " licensing information.\n\n";
134		}
135	2631	if (Configuration::isBuiltWithCryptominisat())
136		{
137		ss << " CryptoMiniSat - An Advanced SAT Solver\n"
138		<< " See https://github.com/msoos/cryptominisat for copyright "
139	2631	<< "information.\n\n";
140		}
141	2631	if (Configuration::isBuiltWithKissat())
142		{
143		ss << " Kissat - Simplified Satisfiability Solver\n"
144		<< " See https://fmv.jku.at/kissat for copyright "
145		<< "information.\n\n";
146		}
147	2631	if (Configuration::isBuiltWithEditline())
148		{
149		ss << " Editline Library\n"
150		<< " See https://thrysoee.dk/editline\n"
151		<< " for copyright information.\n\n";
152		}
153		}
154
155		ss << " SymFPU - The Symbolic Floating Point Unit\n"
156		<< " See https://github.com/martin-cs/symfpu/tree/cvc5 for copyright "
157	2631	<< "information.\n\n";
158
159	2631	if (Configuration::isBuiltWithGmp() \|\| Configuration::isBuiltWithPoly())
160		{
161		ss << "This version of cvc5 is linked against the following third party\n"
162		<< "libraries covered by the LGPLv3 license.\n"
163	2631	<< "See licenses/lgpl-3.0.txt for more information.\n\n";
164	2631	if (Configuration::isBuiltWithGmp()) {
165		ss << " GMP - Gnu Multi Precision Arithmetic Library\n"
166		<< " See http://gmplib.org for copyright information.\n\n";
167		}
168	2631	if (Configuration::isBuiltWithPoly())
169		{
170		ss << " LibPoly polynomial library\n"
171		<< " See https://github.com/SRI-CSL/libpoly for copyright and\n"
172	2631	<< " licensing information.\n\n";
173		}
174	2631	if (Configuration::isStaticBuild())
175		{
176	2631	ss << "cvc5 is statically linked against these libraries. To recompile\n"
177		"this version of cvc5 with different versions of these libraries\n"
178		"follow the instructions on "
179		"https://github.com/cvc5/cvc5/blob/master/INSTALL.md\n\n";
180		}
181		}
182
183	5262	if (Configuration::isBuiltWithCln()
184	2631	\|\| Configuration::isBuiltWithGlpk ()) {
185		ss << "This version of cvc5 is linked against the following third party\n"
186		<< "libraries covered by the GPLv3 license.\n"
187	2631	<< "See licenses/gpl-3.0.txt for more information.\n\n";
188	2631	if (Configuration::isBuiltWithCln()) {
189		ss << " CLN - Class Library for Numbers\n"
190	2631	<< " See http://www.ginac.de/CLN for copyright information.\n\n";
191		}
192	2631	if (Configuration::isBuiltWithGlpk()) {
193		ss << " glpk-cut-log - a modified version of GPLK, "
194		<< "the GNU Linear Programming Kit\n"
195		<< " See http://github.com/timothy-king/glpk-cut-log for copyright"
196		<< " information\n\n";
197		}
198		}
199
200		ss << "See the file COPYING (distributed with the source code, and with\n"
201		<< "all binaries) for the full cvc5 copyright, licensing, and (lack of)\n"
202	2631	<< "warranty information.\n";
203	5262	return ss.str();
204		}
205
206	2631	std::string Configuration::about() {
207	5262	std::stringstream ss;
208	2631	ss << "This is cvc5 version " << CVC5_RELEASE_STRING;
209	2631	if (Configuration::isGitBuild()) {
210	2631	ss << " [" << Configuration::getGitId() << "]";
211		}
212	5262	ss << "\ncompiled with " << Configuration::getCompiler()
213	5262	<< "\non " << Configuration::getCompiledDateTime() << "\n\n";
214	2631	ss << Configuration::copyright ();
215	5262	return ss.str();
216		}
217
218	2631	bool Configuration::licenseIsGpl() {
219	2631	return IS_GPL_BUILD;
220		}
221
222	7890	bool Configuration::isBuiltWithGmp() {
223	7890	return IS_GMP_BUILD;
224		}
225
226	7890	bool Configuration::isBuiltWithCln() {
227	7890	return IS_CLN_BUILD;
228		}
229
230	5259	bool Configuration::isBuiltWithGlpk() {
231	5259	return IS_GLPK_BUILD;
232		}
233
234	7890	bool Configuration::isBuiltWithAbc() {
235	7890	return IS_ABC_BUILD;
236		}
237
238	7894	bool Configuration::isBuiltWithCryptominisat() {
239	7894	return IS_CRYPTOMINISAT_BUILD;
240		}
241
242	5259	bool Configuration::isBuiltWithKissat() { return IS_KISSAT_BUILD; }
243
244	5259	bool Configuration::isBuiltWithEditline() { return IS_EDITLINE_BUILD; }
245
246	7890	bool Configuration::isBuiltWithPoly()
247		{
248	7890	return IS_POLY_BUILD;
249		}
250
251		const std::vector<std::string>& Configuration::getDebugTags()
252		{
253		return Debug_tags;
254		}
255
256		bool Configuration::isDebugTag(const std::string& tag)
257		{
258		return std::find(Debug_tags.begin(), Debug_tags.end(), tag)
259		!= Debug_tags.end();
260		}
261
262		const std::vector<std::string>& Configuration::getTraceTags()
263		{
264		return Trace_tags;
265		}
266
267		bool Configuration::isTraceTag(const std::string& tag)
268		{
269		return std::find(Trace_tags.begin(), Trace_tags.end(), tag)
270		!= Trace_tags.end();
271		}
272
273	7890	bool Configuration::isGitBuild() {
274	7890	return IS_GIT_BUILD;
275		}
276
277	5259	const char* Configuration::getGitBranchName() {
278	5259	return GIT_BRANCH_NAME;
279		}
280
281	5259	const char* Configuration::getGitCommit() {
282	5259	return GIT_COMMIT;
283		}
284
285	5259	bool Configuration::hasGitModifications() {
286	5259	return GIT_HAS_MODIFICATIONS;
287		}
288
289	2631	std::string Configuration::getGitId() {
290	2631	if(! isGitBuild()) {
291		return "";
292		}
293
294	2631	const char* branchName = getGitBranchName();
295	2631	if(*branchName == '\0') {
296		branchName = "-";
297		}
298
299	5262	stringstream ss;
300	5262	ss << "git " << branchName << " " << string(getGitCommit()).substr(0, 8)
301	5262	<< (::cvc5::Configuration::hasGitModifications() ? " (with modifications)"
302	7893	: "");
303	2631	return ss.str();
304		}
305
306	2631	std::string Configuration::getCompiler() {
307	5262	stringstream ss;
308		#ifdef __GNUC__
309	2631	ss << "GCC";
310		#else /* __GNUC__ */
311		ss << "unknown compiler";
312		#endif /* __GNUC__ */
313		#ifdef __VERSION__
314	2631	ss << " version " << __VERSION__;
315		#else /* __VERSION__ */
316		ss << ", unknown version";
317		#endif /* __VERSION__ */
318	5262	return ss.str();
319		}
320
321	2631	std::string Configuration::getCompiledDateTime() {
322	2631	return __DATE__ " " __TIME__;
323		}
324
325	22761	} // namespace cvc5