diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-01 21:35:31 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-01 21:35:31 +0000 |
commit | 96d1c3daff7efdd2d853864fb820bc7cf413624e (patch) | |
tree | b995c98a2be18182d6cb52e81de5bf712b475f06 /src/lib | |
parent | d0b49d588033ab8140bdf297c9cdf73b1088fe68 (diff) |
replacement implementation for clock_gettime() on mac os x, build portability (resolving mac os x issues), code cleanup, fix compiler warnings
Diffstat (limited to 'src/lib')
-rw-r--r-- | src/lib/Makefile.am | 19 | ||||
-rw-r--r-- | src/lib/clock_gettime.c | 69 | ||||
-rw-r--r-- | src/lib/clock_gettime.h | 55 | ||||
-rw-r--r-- | src/lib/replacements.h | 36 |
4 files changed, 179 insertions, 0 deletions
diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am new file mode 100644 index 000000000..ba0ebdd20 --- /dev/null +++ b/src/lib/Makefile.am @@ -0,0 +1,19 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. +AM_CFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libreplacements.la + +libreplacements_la_SOURCES = empty.c +libreplacements_la_LIBADD = \ + $(LTLIBOBJS) + +EXTRA_DIST = \ + replacements.h \ + clock_gettime.c \ + clock_gettime.h + +# empty.c hack -- need *some* source file so that library make rules are built +empty.c:; touch empty.c diff --git a/src/lib/clock_gettime.c b/src/lib/clock_gettime.c new file mode 100644 index 000000000..682269458 --- /dev/null +++ b/src/lib/clock_gettime.c @@ -0,0 +1,69 @@ +/********************* */ +/*! \file clock_gettime.c + ** \verbatim + ** Original author: + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for clock_gettime() for systems without it (like + ** Mac OS X) + ** + ** Replacement for clock_gettime() for systems without it (like Mac + ** OS X). + **/ + +#include <stdio.h> +#include <errno.h> +#include <time.h> + +#include "lib/clock_gettime.h" + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +#ifndef __APPLE__ +# warning This code assumes you're on Mac OS X, and you don't seem to be. You'll likely have problems. +#endif /* __APPLE__ */ + +#include <mach/mach_time.h> + +static double s_clockconv = 0.0; + +long clock_gettime(clockid_t which_clock, struct timespec *tp) { + if( s_clockconv == 0.0 ) { + mach_timebase_info_data_t tb; + kern_return_t err = mach_timebase_info(&tb); + if(err == 0) { + s_clockconv = ((double) tb.numer) / tb.denom; + } else { + return -EINVAL; + } + } + + switch(which_clock) { + case CLOCK_REALTIME: + case CLOCK_REALTIME_HR: + case CLOCK_MONOTONIC: + case CLOCK_MONOTONIC_HR: { + uint64_t t = mach_absolute_time() * s_clockconv; + tp->tv_sec = t / 1000000000ul; + tp->tv_nsec = t % 1000000000ul; + } + break; + default: + return -EINVAL; + } + + return 0; +} + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ diff --git a/src/lib/clock_gettime.h b/src/lib/clock_gettime.h new file mode 100644 index 000000000..aac80dadf --- /dev/null +++ b/src/lib/clock_gettime.h @@ -0,0 +1,55 @@ +/********************* */ +/*! \file clock_gettime.h + ** \verbatim + ** Original author: + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Replacement for clock_gettime() for systems without it (like Mac OS X) + ** + ** Replacement for clock_gettime() for systems without it (like Mac OS X). + **/ + +#ifndef __CVC4__LIB__CLOCK_GETTIME_H +#define __CVC4__LIB__CLOCK_GETTIME_H + +#include "lib/replacements.h" + +#ifdef HAVE_CLOCK_GETTIME + +/* it should be available from <time.h> */ +#include <time.h> + +#else /* HAVE_CLOCK_GETTIME */ + +/* otherwise, we have to define it */ + +/* get timespec from <time.h> */ +#include <time.h> + +#ifdef __cplusplus +extern "C" { +#endif /* __cplusplus */ + +typedef enum { + CLOCK_REALTIME, + CLOCK_MONOTONIC, + CLOCK_REALTIME_HR, + CLOCK_MONOTONIC_HR +} clockid_t; + +long clock_gettime(clockid_t which_clock, struct timespec *tp); + +#ifdef __cplusplus +}/* extern "C" */ +#endif /* __cplusplus */ + +#endif /* HAVE_CLOCK_GETTIME */ +#endif /*__CVC4__LIB__CLOCK_GETTIME_H */ + diff --git a/src/lib/replacements.h b/src/lib/replacements.h new file mode 100644 index 000000000..d38331b66 --- /dev/null +++ b/src/lib/replacements.h @@ -0,0 +1,36 @@ +/********************* */ +/*! \file replacements.h + ** \verbatim + ** Original author: + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Common header for replacement function sources + ** + ** Common header for replacement function sources. + **/ + +#ifndef __CVC4__LIB__REPLACEMENTS_H +#define __CVC4__LIB__REPLACEMENTS_H + +#if defined(__BUILDING_CVC4LIB) || defined(__BUILDING_CVC4LIB_UNIT_TEST) +# include "cvc4_private.h" +#else +# if defined(__BUILDING_CVC4PARSERLIB) || defined(__BUILDING_CVC4PARSERLIB_UNIT_TEST) +# include "cvc4parser_private.h" +# else +# if defined(__BUILDING_CVC4DRIVER) +# include "cvc4autoconfig.h" +# else +# error Must be building libcvc4 or libcvc4parser to use replacement functions. This is because replacement function headers should never be publicly-depended upon, as they should not be installed on user machines with 'make install'. +# endif +# endif +#endif + +#endif /* __CVC4__LIB__REPLACEMENTS_H */ |