From 889d34864fb2218516fd18250e4f086213f14611 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 29 Mar 2012 19:53:20 +0000 Subject: [PATCH] Fix for bug 316. If the flag @CVC4_TLS_SUPPORTED@ is false, function pointers cannot be directly used with the CVC4_THREADLOCAL macro. This is why there were problems on macs. --- src/theory/bv/theory_bv_rewriter.cpp | 2 +- src/theory/bv/theory_bv_rewriter.h | 4 +++- 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 586f37073..2b48977b6 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -33,7 +33,7 @@ using namespace CVC4::theory::bv; // CVC4_THREADLOCAL(AllRewriteRules*) TheoryBVRewriter::s_allRules = NULL; // CVC4_THREADLOCAL(TimerStat*) TheoryBVRewriter::d_rewriteTimer = NULL; -CVC4_THREADLOCAL(RewriteFunction) TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; +RewriteFunction TheoryBVRewriter::d_rewriteTable[kind::LAST_KIND]; void TheoryBVRewriter::init() { // s_allRules = new AllRewriteRules; // d_rewriteTimer = new TimerStat("theory::bv::rewriteTimer"); diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index e72c1a910..7ce914477 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -35,7 +35,9 @@ typedef RewriteResponse (*RewriteFunction) (TNode); class TheoryBVRewriter { // static CVC4_THREADLOCAL(AllRewriteRules*) s_allRules; // static CVC4_THREADLOCAL(TimerStat*) d_rewriteTimer; - static CVC4_THREADLOCAL(RewriteFunction) d_rewriteTable[kind::LAST_KIND]; + +#warning "TODO: Double check thread safety and make sure the fix compiles on mac." + static RewriteFunction d_rewriteTable[kind::LAST_KIND]; static RewriteResponse IdentityRewrite(TNode node); static RewriteResponse UndefinedRewrite(TNode node); -- 2.30.2