From d8cea7c8d58fbca915bfd38822da5ceb2d60ab0c Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 26 May 2020 13:49:13 +0100 Subject: [PATCH] fix a few warnings & simplify debug.h header --- src/math/polynomial/polynomial.cpp | 3 +-- src/smt/seq_regex.cpp | 1 - src/smt/smt_induction.cpp | 3 +-- src/smt/theory_str.cpp | 18 ++++++------- src/util/debug.cpp | 12 ++++----- src/util/debug.h | 43 +++++------------------------- 6 files changed, 24 insertions(+), 56 deletions(-) diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 5d94e77a1..0cb75ff4e 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -549,8 +549,7 @@ namespace polynomial { increase_capacity(sz * 2); SASSERT(sz < m_capacity); m_ptr->m_size = sz; - if (sz == 0) return; - memcpy(m_ptr->m_powers, pws, sizeof(power) * sz); + std::uninitialized_copy(pws, pws + sz, m_ptr->m_powers); } void reset() { diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 51ca4ccf8..ba50d890b 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -209,7 +209,6 @@ namespace smt { expr* s = nullptr, *idx = nullptr, *r = nullptr; expr* e = ctx.bool_var2expr(lit.var()); VERIFY(sk().is_accept(e, s, idx, r)); - expr* t = nullptr; if (i > th.m_max_unfolding_depth && th.m_max_unfolding_lit != null_literal && ctx.get_assignment(th.m_max_unfolding_lit) == l_true && diff --git a/src/smt/smt_induction.cpp b/src/smt/smt_induction.cpp index 28304c665..c7562b608 100644 --- a/src/smt/smt_induction.cpp +++ b/src/smt/smt_induction.cpp @@ -400,7 +400,6 @@ literal induction_lemmas::mk_literal(expr* e) { bool induction_lemmas::operator()(literal lit) { - unsigned num = m_num_lemmas; enode* r = ctx.bool_var2enode(lit.var()); #if 1 @@ -410,6 +409,7 @@ bool induction_lemmas::operator()(literal lit) { } return !combinations.empty(); #else + unsigned num = m_num_lemmas; expr_ref_vector sks(m); expr_safe_replace rep(m); // have to be non-overlapping: @@ -494,7 +494,6 @@ void induction_lemmas::apply_induction(literal lit, induction_positions_t const SASSERT(is_app(t)); args.reset(); unsigned sz = todo.size(); - unsigned i = 0; expr* s = nullptr; for (unsigned i = 0; i < to_app(t)->get_num_args(); ++i) { expr* arg = to_app(t)->get_arg(i); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index ff0bfab6a..1cbbf083f 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -7045,10 +7045,10 @@ namespace smt { void theory_str::check_consistency_prefix(expr * e, bool is_true) { context & ctx = get_context(); ast_manager & m = get_manager(); - expr * needle; - expr * haystack; + expr * needle = nullptr; + expr * haystack = nullptr; - u.str.is_prefix(e, needle, haystack); + VERIFY(u.str.is_prefix(e, needle, haystack)); TRACE("str", tout << "check consistency of prefix predicate: " << mk_pp(needle, m) << " prefixof " << mk_pp(haystack, m) << std::endl;); zstring needleStringConstant; @@ -7072,10 +7072,10 @@ namespace smt { void theory_str::check_consistency_suffix(expr * e, bool is_true) { context & ctx = get_context(); ast_manager & m = get_manager(); - expr * needle; - expr * haystack; + expr * needle = nullptr; + expr * haystack = nullptr; - u.str.is_suffix(e, needle, haystack); + VERIFY(u.str.is_suffix(e, needle, haystack)); TRACE("str", tout << "check consistency of suffix predicate: " << mk_pp(needle, m) << " suffixof " << mk_pp(haystack, m) << std::endl;); zstring needleStringConstant; @@ -7099,10 +7099,10 @@ namespace smt { void theory_str::check_consistency_contains(expr * e, bool is_true) { context & ctx = get_context(); ast_manager & m = get_manager(); - expr * needle; - expr * haystack; + expr * needle = nullptr; + expr * haystack = nullptr; - u.str.is_contains(e, haystack, needle); // first string contains second one + VERIFY(u.str.is_contains(e, haystack, needle)); // first string contains second one TRACE("str", tout << "check consistency of contains predicate: " << mk_pp(haystack, m) << " contains " << mk_pp(needle, m) << std::endl;); zstring needleStringConstant; diff --git a/src/util/debug.cpp b/src/util/debug.cpp index 2d5bfab16..dd9922344 100644 --- a/src/util/debug.cpp +++ b/src/util/debug.cpp @@ -36,13 +36,13 @@ bool assertions_enabled() { } void notify_assertion_violation(const char * fileName, int line, const char * condition) { - std::cerr << "ASSERTION VIOLATION\n"; - std::cerr << "File: " << fileName << "\n"; - std::cerr << "Line: " << line << "\n"; - std::cerr << condition << "\n"; + std::cerr << "ASSERTION VIOLATION\n" + "File: " << fileName << "\n" + "Line: " << line << '\n' + << condition << '\n'; #ifndef Z3DEBUG - std::cerr << Z3_FULL_VERSION << "\n"; - std::cerr << "Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new\n"; + std::cerr << Z3_FULL_VERSION "\n" + "Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new\n"; #endif } diff --git a/src/util/debug.h b/src/util/debug.h index 3dea81418..170049bdb 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -16,25 +16,13 @@ Author: Revision History: --*/ -#ifndef DEBUG_H_ -#define DEBUG_H_ +#pragma once #include void enable_assertions(bool f); bool assertions_enabled(); -#if 0 -#define _CRTDBG_MAP_ALLOC -#include -#include -#include -#endif - -#ifndef __has_builtin -# define __has_builtin(x) 0 -#endif - #include "util/error_codes.h" #include "util/warning.h" @@ -75,44 +63,27 @@ bool is_debug_enabled(const char * tag); #define CASSERT(TAG, COND) DEBUG_CODE(if (assertions_enabled() && is_debug_enabled(TAG) && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); INVOKE_DEBUGGER(); }) #define XASSERT(COND, EXTRA_CODE) DEBUG_CODE(if (assertions_enabled() && !(COND)) { notify_assertion_violation(__FILE__, __LINE__, #COND); { EXTRA_CODE } INVOKE_DEBUGGER(); }) -/** - We use __builtin_unreachable where possible to suppress control flow compilation warnings, but it should - not be called because its behavior is undefined, so we do need to exit before "calling" it. -*/ -#if (defined(__GNUC__) && ((__GNUC__ * 100 + __GNUC_MINOR__) >= 405)) || __has_builtin(__builtin_unreachable) -# define EXIT_WITH(ERR_CODE) { exit(ERR_CODE); __builtin_unreachable(); } ((void) 0) -#else -# define EXIT_WITH(ERR_CODE) { exit(ERR_CODE); } ((void) 0) -#endif - #ifdef Z3DEBUG # define UNREACHABLE() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); INVOKE_DEBUGGER();) #else -# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); EXIT_WITH(ERR_UNREACHABLE); } ((void) 0) +# define UNREACHABLE() { notify_assertion_violation(__FILE__, __LINE__, "UNREACHABLE CODE WAS REACHED."); exit(ERR_UNREACHABLE); } ((void) 0) #endif #ifdef Z3DEBUG # define NOT_IMPLEMENTED_YET() DEBUG_CODE(notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); INVOKE_DEBUGGER();) #else -# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); EXIT_WITH(ERR_NOT_IMPLEMENTED_YET); } ((void) 0) +# define NOT_IMPLEMENTED_YET() { notify_assertion_violation(__FILE__, __LINE__, "NOT IMPLEMENTED YET!"); exit(ERR_NOT_IMPLEMENTED_YET); } ((void) 0) #endif -#define VERIFY(_x_) if (!(_x_)) { \ - std::cerr << "Failed to verify: " << #_x_ << "\n"; \ - UNREACHABLE(); \ +#define VERIFY(_x_) if (!(_x_)) { \ + notify_assertion_violation(__FILE__, __LINE__, "Failed to verify: " #_x_ "\n"); \ + exit(ERR_UNREACHABLE); \ } -#define ENSURE(_x_) \ - if (!(_x_)) { \ - std::cerr << "Failed to verify: " << #_x_ << "\n"; \ - exit(-1); \ - } +#define ENSURE(_x_) VERIFY(_x_) void finalize_debug(); /* ADD_FINALIZER('finalize_debug();') */ - -#endif /* DEBUG_H_ */ -