[Soot-list] Query regarding SPARK points-to analysis

[Aniya Aggarwal]

Hi All,
I am trying to do points-to analysis using SPARK framework. For the code
mentioned below, the analysis yields the following points-to sets for 'obj'
and 'arr'..

arr: {obj}
obj: empty points-to set

The analysis can detect 'obj' in the points-to set of 'arr' using
*reachingObjectsOfArrayElement() *as the elements of the array 'arr'
points-to 'obj' in the first loop. But in the second loop, even though
'obj' points to an element of the array 'arr', the latter is not detected
in the points-to set of 'obj' while using *reachingObjects*(Local l).

I am using SPARK with the following options.

propagator=worklist, simple-edges-bidirectional=false, on-fly-cg=true,
set-impl=double, double-set-old=hybrid, double-set-new=hybrid

Please let me know if this is something that SPARK cannot handle or some
option is set incorrectly. Kindly suggest an alternative to detect 'arr' in
the points-to set of 'obj'.

//Test code
private void testPool( final int POINTS_COUNT){

PointPoolObject obj;
PointPoolObject[] arr = new PointPoolObject[POINTS_COUNT];

for (int i = 0; i < POINTS_COUNT; i++) {

obj = new PointPoolObject();
arr[i] = obj;

}
for (int i = 0; i < POINTS_COUNT; i++) {

obj = arr[i];

}

}

Thanks & Regards,
Aniya Aggarwal
MT-12034
M.Tech CSE (Data Engineering)
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20141102/b237bf04/attachment-0001.html