mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

fix a few warnings & simplify debug.h header

Browse source
This commit is contained in:
Nuno Lopes 2020-05-26 13:49:13 +01:00
parent a97bc65af4
commit d8cea7c8d5
6 changed files with 24 additions and 56 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/math/polynomial/polynomial.cpp
View file

@ -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() {

1
src/smt/seq_regex.cpp
View file

@ -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 &&

3
src/smt/smt_induction.cpp
View file

@ -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);

18
src/smt/theory_str.cpp
View file

@ -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;

12
src/util/debug.cpp
View file

@ -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
}

43
src/util/debug.h
View file

@ -16,25 +16,13 @@ Author:
Revision History:
--*/
#ifndef DEBUG_H_
#define DEBUG_H_
#pragma once
#include <stdlib.h>
void enable_assertions(bool f);
bool assertions_enabled();
#if 0
#define _CRTDBG_MAP_ALLOC
#include<stdlib.h>
#include<new>
#include<crtdbg.h>
#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_ */