<div dir="ltr"><div style="font-size:12.800000190734863px">Hello,</div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px">  We are interested in trying to instrument the Java Symbolic Pathfinder model checker in order to support static symbolic execution of code regions (Veritesting).  To be able to do this, we need to identify regions of code that can be statically executed and to translate the static regions.  We were hoping to use Soot to do this; Shimple is an SSA form that is straightforward to translate into static symbolic execution regions.  </div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px">However in order to do so, we need to be able to precisely map bytecode addresses for instructions corresponding to locations in Shimple, as well as stack offsets and object field references to identifiers in Shimple.  The instruction locations will be used to "trap" the SPF execution to start static symbolic execution.  At these trap points, we need to be able to transfer information in and out of the stack locations and field references that are used by the static code region.</div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px">Is it possible to use "as-is" or modify Soot in order to provide this information?  We are interested either in the information from the original code, or, if it is easier, rewritten bytecode from the Soot Shimple form.  In previous versions of Soot, we could grab the bytecode instructions, but it looks like the current version using the ASM front end no longer has support for this.</div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px">Once again, the things we need specifically are:</div><div style="font-size:12.800000190734863px">  - the java bytecode offsets corresponding to Shimple branching statements</div><div style="font-size:12.800000190734863px">  - the stack offsets for local variables referenced in Shimple</div><div style="font-size:12.800000190734863px">  - the field numbers associated with field references in Shimple.</div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px">Thank you very much for your time!</div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px"><br></div><div style="font-size:12.800000190734863px">Soha</div></div>