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

[Zell]

Dear all,

I think I was not precise enough in my last email.

Say I have two boxes of type Int64_box:
box1 with one dimension,  A->[1,1]
box2 of two dimensions,  A -> [10,10], B->[4,4]

For example,  let us analyze the merge point in the end of the snippet
int a,b,c,d
if (?)  {A=1}
else {A=10; B=4;}

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].*

I realize that what I really wanted was to expand box1 to
A->[1,1],* B->empty*
so that the box1 joined with box2 gives A->[1,10], B->[4,4]

I don't see how to extend box1 in that way, because if one dimension is
empty, the whole int64_box  becomes empty as well, which seems to be
reasonable but does not go with my above example.

Could you pls help me out from there? I certainly misunderstood something,
yet the question should be (hopefully) much more clear now.

Thanks a lot.
Zell.



On Sun, Aug 19, 2012 at 2:56 PM, Zell <zell08v at orange.fr> wrote:

> Hello,
>
> I still have a superficial question.
>
> Consider the domain  D:= Var-> Interval, where "Interval"  contains two
> special  intervals, " Empty " and  " Universe " . I am now using Int_64
> from PPL to model this domain. However I feel confused when I need to
> represent elements that " mixes the 'Empty' and 'Universe' " . One such
> element is,  { x->[3,5], y->[4,7], z->empty, w->universe}.
>
> I find that, whenever a constraint like "z->empty" is added to a
> constraints_system, the constraints_system becomes "false". This seems
> reasonable because the constraint_system in PPL models a conjunction of
> constraints and thus one constraint is false make the whole constraint
> system unsatisfiable. However, I do not see how to represent elements  like
> the one given above that mixes 'z->Empty' and 'w->Universe' . ( I would
> like to use 'z->empty' to mean 'z is not yet initialized', and
> 'w->universe' to mean that 'w is unknown' .)
>
> I probably misunderstand something basic here. What do you think?
>
> Thanks.
> Zell.
>
> p.s Due to the help of Enea and Roberto, I am not able to use PPL in my
> analysis. I really appreciate your help!!! By the way, I have been using
> the pseudo name "Zell" because I used to write my name as "Zell".  For
> information, my passport name is "Zhoulai", which can be more or less
> pronounced as "zell".
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.cs.unipr.it/pipermail/ppl-devel/attachments/20120823/350c56df/attachment.htm>