There is a problem with the exception handling.
Running this code in coastal
package mine;
import za.ac.sun.cs.coastal.Symbolic;
public class MyExample {
public static void main(String[] args) {
test("a");
}
public static void test(String body) {
try {
if (body.length()>0)
throw new RuntimeException("a");
} catch (Exception e) {
Symbolic.mark(-1);
}
Symbolic.mark(1);
}
}
with these settings
coastal.target.main = mine.MyExample
coastal.target.instrument = mine.*
coastal.settings.trace-all = true
coastal.target.trigger = mine.MyExample.test(S: String)
coastal.settings.constant-elimination = false
coastal.delegates = string
coastal.delegates.string.for = java.lang.String
coastal.delegates.string.model = za.ac.sun.cs.coastal.model.String
the diver returns the following unsatisfiable path condition: [0==1#0,[3!=0#0,[1<=0#0]]]
There is a problem with the exception handling.
Running this code in coastal
with these settings
the diver returns the following unsatisfiable path condition:
[0==1#0,[3!=0#0,[1<=0#0]]]