janhaag/PSE2011 — Issue #34: Stack Overflow on array assignment verification
Author: ratefuchs
Created: 2012-02-26 15:11:07+00:00
State: open

When trying to prove the following program:

main(){
int[] i = array[2];
i[0]=0;
}

the program crashes with the following stacktrace:
Exception in thread "main" java.lang.StackOverflowError
at java.lang.AbstractStringBuilder.append(AbstractStringBuilder.java:391)
at java.lang.StringBuilder.append(StringBuilder.java:119)
at verifier.smtlib.SMTLibTranslator.getTypeString(SMTLibTranslator.java:155)
at verifier.smtlib.SMTLibTranslator.getTypeString(SMTLibTranslator.java:160)
at verifier.smtlib.SMTLibTranslator.getTypeString(SMTLibTranslator.java:160)
at verifier.smtlib.SMTLibTranslator.getTypeString(SMTLibTranslator.java:160)
(and some more copies of the last line).

This does, however, only occur if there are array assignments in the program;
array declarations and reads don't cause this behavior.