symbolic arrays in SymbolicListener

dah-fari7009 commented 4 years ago

Good morning,

When returning a symbolic array, I get the following exception with SymbolicListener

I checked the indicated line and it contained: ARETURN areturn = (ARETURN) insn; IntegerExpression returnAttr = (IntegerExpression) areturn.getReturnAttr(ti);

Shouldn't it be ARETURN areturn = (ARETURN) insn; ArrayExpression returnAttr = (ArrayExpression) areturn.getReturnAttr(ti); instead ?

dah-fari7009 commented 4 years ago

Additionally, the name of the symbolic array is java.lang.ClassLoader@1 which gives me no information about the type of the elements.

Is there a reason why it is not in the format [I@15c like concrete arrays ?

dah-fari7009 commented 4 years ago

Follow up : Here is the example, in case you would like to reproduce the described issues:

public static int[] snippet(int[] array,int x)
{
    int w = 100;
    if(x > 0){
        array[0] = x;
        array[1] = x + array[0];
    }
    return array;
}

.jpf file : target = Eq.newV symbolic.method = Eq.newV.snippet(sym#sym) classpath=target/classes symbolic.min_int=-100 symbolic.max_int=100 symbolic.min_long=-100 symbolic.max_long=100 symbolic.min_double=-100.0 symbolic.max_double=100.0 symbolic.debug = true symbolic.optimizechoices = false symbolic.lazy=on symbolic.arrays=true symbolic.strings = true symbolic.dp=z3 symbolic.string_dp_timeout_ms=300000 search.depth_limit=3 listener = gov.nasa.jpf.symbc.SymbolicListener search.multiple_errors=true

SymbolicPathFinder / jpf-symbc

symbolic arrays in SymbolicListener #53