Fix lessOrEquals for CompositeDomain.

[jerhard]

Currently, in the lessOrEquals method of CompositeDomain, if the types of delegates are different, we "cast" the one of type BoundedSet to a StridedInterval. This can create erroneous behavior.

Thus, both StridedInterval and BoundedSet lessOrEqual should be able to compare to elements of both of these types.

[michael-schwarz]

I found an example for erroneous behavior (euler-48.c in samples folder) you can use for testing:

Strided Interval

VsaVisitor::print():for.inc
i.0 -> 1[1, 999]_32
rem.0 -> 1[0, 9999999999]_64
r.0 -> 1[0, 9999999999]_64
j.0 -> 1[0, 998]_32
mul -> T_64
rem4 -> 1[0, 9999999999]_64
inc -> 1[1, 999]_32
VsaVisitor::print():for.end
i.0 -> 1[1, 999]_32
rem.0 -> 1[0, 9999999999]_64
r.0 -> 1[0, 9999999999]_64
j.0 -> 1[1, 999]_32
add -> 1[0, 19999999998]_64
rem5 -> 1[0, 9999999999]_64
VsaVisitor::print():for.inc6
i.0 -> 1[1, 999]_32
rem.0 -> 1[0, 9999999999]_64
r.0 -> 1[0, 9999999999]_64
j.0 -> 1[1, 999]_32
add -> 1[0, 19999999998]_64
rem5 -> 1[0, 9999999999]_64
inc7 -> 1[2, 1000]_32
VsaVisitor::print():for.end8
i.0 -> 0[1000, 1000]_32
rem.0 -> 1[0, 9999999999]_64
VsaVisitor::print():entry
VsaVisitor::print():for.cond
i.0 -> 1[1, 1000]_32
rem.0 -> 1[0, 9999999999]_64
VsaVisitor::print():for.body
i.0 -> 1[1, 999]_32
rem.0 -> 1[0, 9999999999]_64
VsaVisitor::print():for.cond1
i.0 -> 1[1, 999]_32
rem.0 -> 1[0, 9999999999]_64
r.0 -> 1[0, 9999999999]_64
j.0 -> 1[0, 999]_32
VsaVisitor::print():for.body3
i.0 -> 1[1, 999]_32
rem.0 -> 1[0, 9999999999]_64
r.0 -> 1[0, 9999999999]_64
j.0 -> 1[0, 998]_32
mul -> T_64
rem4 -> 1[0, 9999999999]_64

BoundedSet
(all vars are T)

CompositeDomain (incorrect)

Global state after 6 visits
VsaVisitor::print():for.inc
i.0 -> {1}
rem.0 -> {0}
r.0 -> {1}
j.0 -> {0}
mul -> T_64
rem4 -> 1[0, 9999999999]_64
inc -> {1}
VsaVisitor::print():entry
VsaVisitor::print():for.cond
i.0 -> {1}
rem.0 -> {0}
VsaVisitor::print():for.body
i.0 -> {1}
rem.0 -> {0}
VsaVisitor::print():for.cond1
i.0 -> {1}
rem.0 -> {0}
r.0 -> {1}
j.0 -> {0}
VsaVisitor::print():for.body3
i.0 -> {1}
rem.0 -> {0}
r.0 -> {1}
j.0 -> {0}
mul -> T_64
rem4 -> 1[0, 9999999999]_64