24 Aug
2012
24 Aug
'12
11:28 a.m.
On 08/23/2012 01:02 PM, Zell wrote:
I use Int64_box as abstract domains, so that the if- part and else- part give box1 and box2 as shown above. To reason about the merge point, I use *add_dimension_and_embed *before *upper_bound_assign*. But that will extend box1 to A->[1,1],B->[-inf,+inf] so that the upper_bound_assign will give A->[1,10],_B->[-inf,+inf]._
Why you do not like this result? It is the correct one. It means that you don't know anything about B. In other words, B may hold whatever value is there after initialization.
In any case, there is no way to have an object like A->[1,1], B->empty with any of the standard numerical domains.
--gianluca amato