[PPL-devel] To represent z->Empty and w->Universe.

[Gianluca Amato]

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