Precision of Spark Analysis

[buckley <buckley@fmi.uni-passau.de>]

Hi,

I've got a question about the precision of SPARK's points-to analysis.
In my small example below I calculated the points-to sets with the
standard options.
The sets always include that "A.f()" points to "c" which is not possible
I think.
What I want know is, whether it is possible to enhance SPARK's precision

(by some combination of switches maybe) so that it is able to handle
this kind of
problem.

Greetings,
     Thorsten Buckley

----------------------------------------------
public class A {
 public int f() { return(g()); }
 public int g() { return(x); }
 public int x;
}

public class B extends A {
 public int g() { return(y); }
 public int y;
}

public class C extends B {
 public C() {}
 public int f() { return( g() + z ); }
 public int z;
}


public class Test {
 public static void main(String[] args) {
  A a = new A(); B b = new B(); C c = new C();
  A ap;
  if(args.length == 0) { ap = a; }
  else { if(args.length == 1) { ap = b; }
     else { ap = c; } }
  ap.f();
 }
}