[Soot-list] Assertions in source code

[Bodden, Eric]

Hi Mihir.

Good question. Can you make a minimal example and post it as a bug on github?

Cheers,
Eric

> On 04.12.2014, at 19:39, Mihir Mehta <mihir.cs.iitd at gmail.com> wrote:
> 
> (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.
> 
> _______________________________________________
> Soot-list mailing list
> Soot-list at CS.McGill.CA
> https://mailman.CS.McGill.CA/mailman/listinfo/soot-list

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 841 bytes
Desc: Message signed with OpenPGP using GPGMail
Url : http://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20141206/b3df8d0a/attachment.bin