SPARK handling of String constants

[Manu Sridharan <manu_s@eecs.berkeley.edu>]

Hi,

I am trying to understand how SPARK handles String constants.  Browsing 
the source and writing a couple of small tests seemed to indicate that all 
String constants all unified, so any two String variables that are 
assigned a String constant will have intersecting points-to sets.  
However, I believe that SPARK also attempts to figure out the targets of 
reflective calls through inspecting String constant values.  Is there any 
documentation on how exactly SPARK handles Strings?  This is for the 1.2.5 
release, BTW.

Thanks,
Manu