[Soot-list] points-to analysis output

[Ondrej Lhotak]

On Mon, Aug 07, 2006 at 04:35:09PM -0400, Hiroshi Yamauchi wrote:
> Hi,
> 
> I would like to see and make sense of the results of the SPARK points- 
> to analysis.
> Is there any document that explains the formats of the dump files  
> (dump-html,
> dump-solution, dump-pag, dump-answer, etc)? They are not obvious to me.
> Alternatively, is there a more readable dump file that shows analysis  
> results?

The dump-html option outputs the entire pointer assignment graph in
human-readable HTML. Each PAG node is one page, with links representing
PAG edges into and out of the node. These web pages should be
self-documenting to someone who understands the PAG. For an explanation
of the PAG, see my master's thesis.

The dump-pag and dump-answer options output the PAG in a form
suitable for input to other PAG solvers (such as the BDD solver
http://www.sable.mcgill.ca/bdd/). Only the structure of the PAG is
preserved, and not the metadata for each node. Each node is represented
as an integer, and the output contains pairs of lines indicating edges
between nodes. The edge types in the file correspond to the edge types
described in my master's thesis. A more detailed explanation of the
exact file format (for parsing) appeared on the soot-list at some point
and should be somewhere in the mailing list archives.

The dump-answer option creates a file called types. For each local
variable of reference type in the program, the file contains a line
starting with V and identification of the variable (its declaring method
and variable name), followed by 0 or more lines starting with T, each
indicating a potential run-time type of the object to which the variable
may point.

Ondrej


> 
> Best regards,
> -Hiroshi
> 
> 
> _______________________________________________
> Soot-list mailing list
> Soot-list at sable.mcgill.ca
> http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>