Octagonal_Shape::affine_image seems a bit too imprecise when treating assignments of the form Y = -Y + c.<br><br>Here's the code involved:<br><br> // Here `w_coeff == -denominator'.<br> // Remove the binary constraints on `var'.<br>
forget_binary_octagonal_constraints(var_id);<br> const Row_Iterator m_begin = matrix.row_begin();<br> Row_Iterator m_iter = m_begin + n_var;<br> N& m_v_cv = (*m_iter)[n_var+1];<br>
++m_iter;<br> N& m_cv_v = (*m_iter)[n_var];<br> // Swap the unary constraints on `var'.<br> std::swap(m_v_cv, m_cv_v);<br> // Strong closure is not preserved.<br> reset_strongly_closed();<br>
if (b != 0) {<br> // Translate the unary constraints on `var',<br> // adding or subtracting the value `b/denominator'.<br> PPL_DIRTY_TEMP(N, d);<br> div_round_up(d, b, denominator);<br>
mul_2exp_assign_r(d, d, 1, ROUND_UP);<br> add_assign_r(m_cv_v, m_cv_v, d, ROUND_UP);<br> PPL_DIRTY_TEMP(N, minus_d);<br> div_round_up(minus_d, b, minus_den);<br> mul_2exp_assign_r(minus_d, minus_d, 1, ROUND_UP);<br>
add_assign_r(m_v_cv, m_v_cv, minus_d, ROUND_UP);<br> }<br> incremental_strong_closure_assign(var);<br> }<br><br>This approach that discards all old binary constraints on the assigned variable looks a little too naive to me. Consider for instance this assigment sequence:<br>
<br>X = Y;<br>Y = -Y;<br><br>The octagonal domain will not be able to deduce X + Y = 0 as I would expect. A similar problem probably exists for BD Shapes.<br>