[Soot-list] Fwd: Assertions in source code

[Mihir Mehta]

Hi,

I was going to send a minimal example, per Eric's request, but before I 
could do that I saw Zhoulai's suggestion of using junit.assert, which 
works for me; I can assume that whenever a virtualinvoke instruction for 
the function junit.assert appears before a loop, it's a loop invariant.

Thanks, both.

Mihir.

On 12/06/14 14:00, Zhoulai wrote:
> Hi,
>
> I guess Soot may or may no recognize your /assert/ depending on 
> whether /assert/ is enabled/disabled by your compiler.
>
> See
> http://stackoverflow.com/questions/3018683/what-does-assert-do
>
> If I remember well, if enabled, java /assert/ is syntactically 
> equivalent to /if/ (...) statement which should be well captured by 
> soot's IR like /Jimple/.
>
> Otherwise, an alternative is to use /junit/./assert/ or your 
> customized /assert/ so they explicitly appear in your IR and then you 
> can do whatever you want.
>
> I hope  this answers to your question.
>
> Zhoulai
>
> On Thu, Dec 4, 2014 at 10:39 AM, Mihir Mehta <mihir.cs.iitd at gmail.com 
> <mailto: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 <mailto:Soot-list at CS.McGill.CA>
>     https://mailman.CS.McGill.CA/mailman/listinfo/soot-list
>
>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.CS.McGill.CA/pipermail/soot-list/attachments/20141206/84e31f82/attachment.html