mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

avoid unintialized value build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-24 15:02:31 -07:00
parent a557913307
commit af51d98a32
3 changed files with 33 additions and 26 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/math/lp/nla_intervals.cpp
View file

@ -120,10 +120,10 @@ void intervals::add_linear_to_vector(const nex* e, vector<std::pair<rational, lp
// e = a * can_t + b // e = a * can_t + b
lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational& a, rational& b) { lp::lar_term intervals::expression_to_normalized_term(const nex_sum* e, rational& a, rational& b) {
TRACE("nla_horner_details", tout << *e << "\n";); TRACE("nla_horner_details", tout << *e << "\n";);
lpvar smallest_j; lpvar smallest_j = 0;
vector<std::pair<rational, lpvar>> v; vector<std::pair<rational, lpvar>> v;
b = rational(0); b = rational(0);
unsigned a_index; unsigned a_index = UINT_MAX;
for (const nex* c : *e) { for (const nex* c : *e) {
if (c->is_scalar()) { if (c->is_scalar()) {
b += c->to_scalar().value(); b += c->to_scalar().value();

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

@ -581,6 +581,9 @@ namespace algebraic_numbers {
bool b_lt_a = lt(b, a); bool b_lt_a = lt(b, a);
bool c_lt_b = lt(c, b); bool c_lt_b = lt(c, b);
bool c_lt_a = lt(c, a); bool c_lt_a = lt(c, a);
(void)b_lt_a;
(void)c_lt_b;
(void)c_lt_a;
// (a <= b & b <= c) => a <= c // (a <= b & b <= c) => a <= c
// b < a or c < b or !(c < a) // b < a or c < b or !(c < a)
CTRACE("algebraic_bug", CTRACE("algebraic_bug",

52
src/smt/theory_str_mc.cpp
View file

@ -55,22 +55,19 @@ namespace smt {
rational val1; rational val1;
expr_ref len(m), len_val(m); expr_ref len(m), len_val(m);
expr* e1, *e2; expr* e1 = nullptr, *e2 = nullptr;
expr_ref_vector todo(m); expr_ref_vector todo(m);
todo.push_back(e); todo.push_back(e);
val.reset(); val.reset();
while (!todo.empty()) { while (!todo.empty()) {
expr* c = todo.back(); expr* c = todo.back();
todo.pop_back(); todo.pop_back();
if (u.str.is_concat(to_app(c))) { zstring tmp;
e1 = to_app(c)->get_arg(0); if (u.str.is_concat(c, e1, e2)) {
e2 = to_app(c)->get_arg(1);
todo.push_back(e1); todo.push_back(e1);
todo.push_back(e2); todo.push_back(e2);
} }
else if (u.str.is_string(to_app(c))) { else if (u.str.is_string(c, tmp)) {
zstring tmp;
u.str.is_string(to_app(c), tmp);
unsigned int sl = tmp.length(); unsigned int sl = tmp.length();
val += rational(sl); val += rational(sl);
} }
@ -96,9 +93,9 @@ namespace smt {
ast_manager & sub_m = subsolver.m(); ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context(); context & sub_ctx = subsolver.get_context();
expr * full; expr * full = nullptr;
expr * suff; expr * suff = nullptr;
u.str.is_suffix(f, suff, full); VERIFY(u.str.is_suffix(f, suff, full));
expr_ref haystack(full, m); expr_ref haystack(full, m);
expr_ref needle(suff, m); expr_ref needle(suff, m);
@ -159,9 +156,9 @@ namespace smt {
ast_manager & sub_m = subsolver.m(); ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context(); context & sub_ctx = subsolver.get_context();
expr * full; expr * full = nullptr;
expr * suff; expr * suff = nullptr;
u.str.is_suffix(f, suff, full); VERIFY(u.str.is_suffix(f, suff, full));
expr_ref haystack(full, m); expr_ref haystack(full, m);
expr_ref needle(suff, m); expr_ref needle(suff, m);
@ -214,9 +211,9 @@ namespace smt {
ast_manager & sub_m = subsolver.m(); ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context(); context & sub_ctx = subsolver.get_context();
expr * full; expr * full = nullptr;
expr * pref; expr * pref = nullptr;
u.str.is_prefix(f, pref, full); VERIFY(u.str.is_prefix(f, pref, full));
expr_ref haystack(full, m); expr_ref haystack(full, m);
expr_ref needle(pref, m); expr_ref needle(pref, m);
@ -331,9 +328,9 @@ namespace smt {
ast_manager & sub_m = subsolver.m(); ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context(); context & sub_ctx = subsolver.get_context();
expr * full; expr * full = nullptr;
expr * small; expr * small = nullptr;
u.str.is_contains(f, full, small); VERIFY(u.str.is_contains(f, full, small));
expr_ref haystack(full, m); expr_ref haystack(full, m);
expr_ref needle(small, m); expr_ref needle(small, m);
@ -471,9 +468,8 @@ namespace smt {
ast_manager & sub_m = subsolver.m(); ast_manager & sub_m = subsolver.m();
context & sub_ctx = subsolver.get_context(); context & sub_ctx = subsolver.get_context();
expr * str; expr * str = nullptr, *re = nullptr;
expr * re; VERIFY(u.str.is_in_re(f, str, re));
u.str.is_in_re(f, str, re);
// TODO reuse some of the automaton framework from theory_str_regex // TODO reuse some of the automaton framework from theory_str_regex
eautomaton * aut = m_mk_aut(re); eautomaton * aut = m_mk_aut(re);
@ -1630,6 +1626,7 @@ namespace smt {
if (indicatorHasEqcValue) { if (indicatorHasEqcValue) {
zstring len_pIndiStr; zstring len_pIndiStr;
u.str.is_string(len_indicator_value, len_pIndiStr); u.str.is_string(len_indicator_value, len_pIndiStr);
// NSB: is len_indicator_value always a string? Then use VERIFY, or otherwise test return value
if (len_pIndiStr != "more") { if (len_pIndiStr != "more") {
effectiveLenInd = len_indicator_pre; effectiveLenInd = len_indicator_pre;
effectiveLenIndiStr = len_pIndiStr; effectiveLenIndiStr = len_pIndiStr;
@ -1658,6 +1655,7 @@ namespace smt {
} else { } else {
if (effectiveHasEqcValue) { if (effectiveHasEqcValue) {
u.str.is_string(effective_eqc_value, effectiveLenIndiStr); u.str.is_string(effective_eqc_value, effectiveLenIndiStr);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
} else { } else {
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
} }
@ -1955,6 +1953,7 @@ namespace smt {
// safety check // safety check
zstring effectiveLenIndiStr; zstring effectiveLenIndiStr;
u.str.is_string(len_indicator_value, effectiveLenIndiStr); u.str.is_string(len_indicator_value, effectiveLenIndiStr);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") { if (effectiveLenIndiStr == "more" || effectiveLenIndiStr == "less") {
TRACE("str", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;); TRACE("str", tout << "ERROR: illegal state -- requesting 'more value tests' but a length tester is not yet concrete!" << std::endl;);
UNREACHABLE(); UNREACHABLE();
@ -1982,6 +1981,7 @@ namespace smt {
if (indicatorHasEqcValue) { if (indicatorHasEqcValue) {
zstring len_pIndiStr; zstring len_pIndiStr;
u.str.is_string(len_indicator_value, len_pIndiStr); u.str.is_string(len_indicator_value, len_pIndiStr);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
if (len_pIndiStr != "more") { if (len_pIndiStr != "more") {
effectiveLenInd = len_indicator_pre; effectiveLenInd = len_indicator_pre;
effectiveLenIndiStr = len_pIndiStr; effectiveLenIndiStr = len_pIndiStr;
@ -2086,6 +2086,7 @@ namespace smt {
} }
} else { } else {
u.str.is_string(lastTesterValue, lastTesterConstant); u.str.is_string(lastTesterValue, lastTesterConstant);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
} }
TRACE("str", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << "\n";); TRACE("str", tout << "last length tester is assigned \"" << lastTesterConstant << "\"" << "\n";);
if (lastTesterConstant == "more" || lastTesterConstant == "less") { if (lastTesterConstant == "more" || lastTesterConstant == "less") {
@ -2249,6 +2250,7 @@ namespace smt {
expr * coreVal = to_app(str2RegFunc)->get_arg(0); expr * coreVal = to_app(str2RegFunc)->get_arg(0);
zstring coreStr; zstring coreStr;
u.str.is_string(coreVal, coreStr); u.str.is_string(coreVal, coreStr);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
if (oneUnroll == nullptr) { if (oneUnroll == nullptr) {
oneUnroll = *itor; oneUnroll = *itor;
oneCoreStr = coreStr; oneCoreStr = coreStr;
@ -2266,6 +2268,7 @@ namespace smt {
expr * coreVal = to_app(str2RegFunc)->get_arg(0); expr * coreVal = to_app(str2RegFunc)->get_arg(0);
zstring coreStr; zstring coreStr;
u.str.is_string(coreVal, coreStr); u.str.is_string(coreVal, coreStr);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
unsigned int core1Len = coreStr.length(); unsigned int core1Len = coreStr.length();
zstring uStr = get_unrolled_string(coreStr, (lcm / core1Len)); zstring uStr = get_unrolled_string(coreStr, (lcm / core1Len));
if (uStr != lcmStr) { if (uStr != lcmStr) {
@ -2353,6 +2356,7 @@ namespace smt {
} else { } else {
zstring testerStr; zstring testerStr;
u.str.is_string(testerVal, testerStr); u.str.is_string(testerVal, testerStr);
// NSB: is argument always a string? Then use VERIFY, or otherwise test return value
TRACE("str", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";); TRACE("str", tout << "Tester [" << mk_pp(tester, mgr) << "] = " << testerStr << "\n";);
if (testerStr == "more") { if (testerStr == "more") {
litems.push_back(ctx.mk_eq_atom(tester, moreAst)); litems.push_back(ctx.mk_eq_atom(tester, moreAst));
@ -2556,8 +2560,8 @@ namespace smt {
zstring str_lo, str_hi; zstring str_lo, str_hi;
SASSERT(u.str.is_string(lo)); SASSERT(u.str.is_string(lo));
SASSERT(u.str.is_string(hi)); SASSERT(u.str.is_string(hi));
u.str.is_string(lo, str_lo); VERIFY(u.str.is_string(lo, str_lo));
u.str.is_string(hi, str_hi); VERIFY(u.str.is_string(hi, str_hi));
SASSERT(str_lo.length() == 1); SASSERT(str_lo.length() == 1);
SASSERT(str_hi.length() == 1); SASSERT(str_hi.length() == 1);
unsigned int c1 = str_lo[0]; unsigned int c1 = str_lo[0];