Dear all, <br><br>I think I was not precise enough in my last email. <br><br>Say I have two boxes of type Int64_box:<br>box1 with one dimension,  A->[1,1]<br>box2 of two dimensions,  A -> [10,10], B->[4,4] <br><br>
For example,  let us analyze the merge point in the end of the snippet<br>int a,b,c,d<br>if (?)  {A=1}<br>else {A=10; B=4;}<br><br>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 <b>add_dimension_and_embed </b>before <b>upper_bound_assign</b>. But that will extend box1 to A->[1,1],B->[-inf,+inf] so that the upper_bound_assign will  give A->[1,10],<u> B->[-inf,+inf].</u><br>
<br>I realize that what I really wanted was to expand box1 to <br>A->[1,1],<u> B->empty</u><br>so that the box1 joined with box2 gives A->[1,10], B->[4,4]<br><br>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. <br>
<br>Could you pls help me out from there? I certainly misunderstood something, yet the question should be (hopefully) much more clear now.  <br><br>Thanks a lot. <br>Zell.  <br>
<br><br> <br><div class="gmail_quote">On Sun, Aug 19, 2012 at 2:56 PM, Zell <span dir="ltr"><<a href="mailto:zell08v@orange.fr" target="_blank">zell08v@orange.fr</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Hello, <br><br>I still have a superficial question. <br><br>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}. <br>


<br>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' .) <br>

<br>I probably misunderstand something basic here. What do you think?<br><br>Thanks. <br><span class="HOEnZb"><font color="#888888">Zell. <br></font></span><br>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". <br>


</blockquote></div><br>