[Soot-list] Fwd: Assertions in source code

[Mihir Mehta]

(Mods: I earlier sent the exact same email from the wrong email address,
sorry about that; this is the address with which I'm subscribed to the
list.)

Hi folks,

Does Soot offer some way to read assertions, expressed either via the Java
assert keyword (http://docs.oracle.com/javase/specs/jls/se8/html/jls-
14.html#jls-14.10) or in some other syntax inside comments? I'm trying to
do something that involved annotating loops with invariants to make my
verification task easier, and I tried inserting assert statements into the
source code towards this end. However, the soot parser failed with a
java.lang.ArrayIndexOutOfBoundsException in
soot.JastAddJ.BytecodeParser.parseThisClass,
which is consistent with what this document (http://www.sable.mcgill.ca/
soot/tutorial/useannotation/useannotation.pdf) says about soot only
supporting annotations for null pointer checks and array bound checks.

Am I doing something wrong, or is Soot indeed incapable of doing this for
me? I could make a minimal example of the problem but I don't think this is
about debugging as much as this is about figuring out the right Soot
feature for the job.

Thanks,
Mihir.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20141204/7d8d16d3/attachment.html