Symbolic String operations

[João Matos]

Hello!

All string operations, with the exception of 'equals', are not working, i.e. they do not branch nor appear in the path condition. 

Could someone tell me what I'm missing?

Thanks in advance

Best regards

[Corina Pasareanu]

did you try any of the examples?

corina

--
 
---
You received this message because you are subscribed to the Google Groups "Java™ Pathfinder" group.
To unsubscribe from this group and stop receiving emails from it, send an email to java-pathfind...@googlegroups.com.
For more options, visit https://groups.google.com/groups/opt_out.
 
 

[João Matos]

Hi,

thanks for the quick reply. 

I tried the MSExample just now, and it seems to be working, at least for the operation 'startswith'. 

It's not working for my test cases, so I suppose this is a configuration problem?

[Corina Pasareanu]

hard to tell without knowing your test cases :)

corina

[João Matos]

Hi,

My test cases are too large to post here :)

Anyway, I figured out what the problem was. I want all user input to be symbolic, therefore

whenever I see an instruction of java.io or Scanner, I automatically skip it and create a 

symbolic variable in its place. The problem is that if I have something like:

String variable = scanner.next();

for some reason the ClassInfo of the variable becomes of type Scanner instead of String. As a consequence,

when INVOKEVIRTUAL.execute() takes place, 

            MethodInfo mi = getInvokedMethod(th, objRef);

    if (mi == null) {

      String clsName = th.getClassInfo(objRef).getName();

      return th.createAndThrowException("java.lang.NoSuchMethodError", clsName + '.' + mname);

    }

the method getInvokedMethod returns null, because String.startsWith() does not exist in class Scanner.

I don't know if this is a problem of JPF or not. Anyway I know how to circumvent this, but thanks for the attention anyway! 

Best Regards,

João Matos 

[Corina Pasareanu]

it could be a problem in jpf-core
anyway i am working on transitioning to jpf.v7 and hopefully this will go away

however it will still take some time to finish it (the symbolic part) as i want to clean and test the code before "officially" releasing it
thanks
corina