[Soot-list] How does Jimple preserve semantics with its partial SSA without Phi-node mechanism?? (with an example illustrating my idea)

[Z]

Hello,

If I understand correctly, Jimple introduces a unique names for each use of
local variable, but Jimple does not use Phi-node. So I wonder how Jimple
preserves the semantics? My question is more clear with the following
example:

-------------------source----------
    static void test7() {
        int x,y;
        x = 0;
        while (x<10);{
            y = x;
            x = x +1;
        }
    }
------------here is the Jimple program from the bytecode generated from the
source--------
    static void test7()
    {
        byte b0, b1;
        int i2;

        b0 = 0;

     label0:
        if b0 < 10 goto label0;

        b1 = b0;
        i2 = b0 + 1;
        return;
    }
-----------------------

It is clear that  this Jimple is actually
-------
b0=0
while b0<10{
  b1=b0;
  i2=b0+1;
}
-----

My naive conclusion is that the transformed Jimple does not preserve the
semantics of the original program, since the original one terminates but
the transformed one does not.

Could you pls tell me where I am wrong?

Thanks a lot.

Zell.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20120712/b596c741/attachment-0001.html