Z3Prover / z3

The Z3 Theorem Prover
Other
10.42k stars 1.47k forks source link

In member function ‘void lp::lp_bound_propagator<T>::try_add_equation_with_val_table(const lp::lp_bound_propagator<T>::vertex*) [with T = smt::theory_lra::imp]’: 7src/util/map.h:34:18: warning: ‘u’ may be used uninitialized #4606

Closed XVilka closed 4 years ago

XVilka commented 4 years ago
 711 [ 72%] Building CXX object src/smt/CMakeFiles/smt.dir/theory_utvpi.cpp.o
 712 In file included from /home/user/data/math/z3/src/math/lp/lar_term.h:22,
 713                  from /home/user/data/math/z3/src/math/lp/lar_constraints.h:31,
 714                  from /home/user/data/math/z3/src/math/lp/implied_bound.h:22,             
 715                  from /home/user/data/math/z3/src/math/lp/bound_analyzer_on_row.h:25,
 716                  from /home/user/data/math/z3/src/math/lp/lp_solver.h:31,
 717                  from /home/user/data/math/z3/src/smt/theory_lra.cpp:22:
 718 /home/user/data/math/z3/src/util/map.h: In member function ‘void lp::lp_bound_propagator<T>::try_add_equation_with_val_table(const lp::lp_bound_propagator<T>::vertex*) [with T = smt::theory_lra::imp]’:
 719 /home/user/data/math/z3/src/util/map.h:34:18: warning: ‘u’ may be used uninitialized in this function [-Wmaybe-uninitialized]
 720    34 |         m_value(v) {
 721       |                  ^
 722 In file included from /home/user/data/math/z3/src/math/lp/lar_solver.h:45,
 723                  from /home/user/data/math/z3/src/smt/theory_lra.cpp:26:
 724 /home/user/data/math/z3/src/math/lp/lp_bound_propagator.h:208:17: note: ‘u’ was declared here
 725   208 |         vertex *u;
 726       |                 ^
NikolajBjorner commented 4 years ago

@levnach - the insertion seems wrong because m_vals_to_verts will then get a null value for u (if we set u to null).

levnach commented 4 years ago

Fixed now.