make_binary must not mess up types when dealing with pointers

[tautschnig]

No description provided.

[peterschrammel]

@tautschnig, @kroening, anything controversial about merging this?

[tautschnig]

The only question I'm aware of was a missing regression test or any kind of example where errors had been triggered. As far as I recall, this would only become necessary when using dereferencet (pointer-analysis/dereference.h).

[kroening]

I looked at this; I'd say that the multi-ary expressions should not be used for pointer arithmetic to begin with. The rule should be that all operands in a multi-ary expression must have the same type.

[tautschnig]

@kroening make_binary isn't used widely, git grep -l make_binary suggests that 3/8 users are pointer-related:

analyses/goto_check.cpp
analyses/local_bitvector_analysis.cpp
analyses/local_may_alias.cpp
goto-symex/adjust_float_expressions.cpp
pointer-analysis/dereference.cpp
solvers/prop/bdd_expr.cpp
solvers/refinement/refine_arithmetic.cpp
solvers/smt2/smt2_conv.cpp
util/expr_util.cpp
util/expr_util.h

I'll try to clean this up and remove the source of multi-ary pointer expressions (that should be the simplifier).

[kroening]

Thank you! If we wanted to be very conservative, we could check the rule "all operands must have same type" with an assertion, while at it.

[tautschnig]

I haven't tweaked the simplifier, but instead removed all uses of make_binary in contexts where such would not be safe - and added a check in make_binary to make sure no future such use creeps in.