NULL-initialize pointers to help GCC static analyzer Fixes: variable may be used uninitialized

src/ast/rewriter/poly_rewriter_def.h

@@ -431,7 +431,8 @@ struct poly_rewriter<Config>::hoist_cmul_lt {
     hoist_cmul_lt(poly_rewriter<Config> & r):m_r(r) {}
 
     bool operator()(expr * t1, expr * t2) const {
-        expr * pp1, * pp2;
+        expr * pp1 = nullptr;
+        expr * pp2 = nullptr;
         numeral c1, c2;
         bool is_mul1 = m_r.is_mul(t1, c1, pp1);
         bool is_mul2 = m_r.is_mul(t2, c2, pp2);

src/ast/rewriter/rewriter_def.h

@@ -336,9 +336,9 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
             UNREACHABLE();
         }
         // TODO: add rewrite rules support
-        expr * def;
+        expr * def = nullptr;
-        proof * def_pr;
+        proof * def_pr = nullptr;
-        quantifier * def_q;
+        quantifier * def_q = nullptr;
         // When get_macro succeeds, then
         // we know that:
         // forall X. f(X) = def[X]

src/smt/theory_str.cpp

@@ -1423,9 +1423,9 @@ namespace smt {
         //     len(hd) = i
         //     str.indexof(tl, N, 0)
 
-        expr * H; // "haystack"
+        expr * H = nullptr; // "haystack"
-        expr * N; // "needle"
+        expr * N = nullptr; // "needle"
-        expr * i; // start index
+        expr * i = nullptr; // start index
         u.str.is_index(e, H, N, i);
 
         expr_ref minus_one(m_autil.mk_numeral(rational::minus_one(), true), m);
@@ -6951,8 +6951,8 @@ namespace smt {
         ast_manager & m = get_manager();
 
         expr_ref_vector rhs(m);
-        expr * str;
+        expr * str = nullptr;
-        expr * re;
+        expr * re = nullptr;
         u.str.is_in_re(str_in_re, str, re);
         expr_ref strlen(mk_strlen(str), m);
 
@@ -9929,8 +9929,8 @@ namespace smt {
             bool regex_axiom_add = false;
             for (obj_hashtable<expr>::iterator it = regex_terms.begin(); it != regex_terms.end(); ++it) {
                 expr * str_in_re = *it;
-                expr * str;
+                expr * str = nullptr;
-                expr * re;
+                expr * re = nullptr;
                 u.str.is_in_re(str_in_re, str, re);
                 lbool current_assignment = ctx.get_assignment(str_in_re);
                 TRACE("str", tout << "regex term: " << mk_pp(str, m) << " in " << mk_pp(re, m) << " : " << current_assignment << std::endl;);
@@ -9944,7 +9944,7 @@ namespace smt {
 
                         if (regex_term_to_length_constraint.contains(str_in_re)) {
                             // use existing length constraint
-                            expr * top_level_length_constraint;
+                            expr * top_level_length_constraint = nullptr;
                             regex_term_to_length_constraint.find(str_in_re, top_level_length_constraint);
 
                             ptr_vector<expr> extra_length_vars;
@@ -10473,8 +10473,8 @@ namespace smt {
                 // that's consistent with the current length information
                 for (ptr_vector<expr>::iterator term_it = str_in_re_terms.begin();
                         term_it != str_in_re_terms.end(); ++term_it) {
-                    expr * _unused;
+                    expr * _unused = nullptr;
-                    expr * re;
+                    expr * re = nullptr;
                     SASSERT(u.str.is_in_re(*term_it));
                     u.str.is_in_re(*term_it, _unused, re);
 

src/tactic/core/solve_eqs_tactic.cpp

@@ -263,8 +263,8 @@ class solve_eqs_tactic : public tactic {
         bool solve_arith_core(app * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
             SASSERT(m_a_util.is_add(lhs));
             bool is_int  = m_a_util.is_int(lhs);
-            expr * a; 
+            expr * a = nullptr; 
-            expr * v;
+            expr * v = nullptr;
             rational a_val;
             unsigned num = lhs->get_num_args();
             unsigned i;