Inquire about running gdart on a specific function in large code

[BEbillionaireUSD]

Hi, Thanks for this wonderful work.
I'm wondering how to run symbolic execution on a specific function. For example

public class Example {
    private static int i;
    public static void main(String[] args) {
       foo(3);
      bar(2);
    }

    public static int foo(int x) {
	return 1/x;
    }
     public static int bar(int x) {
	return x+1;
    }

}

What should I do if I just want to run gdart on bar?

[mmuesly]

Hi, you are welcome. It is necessary to write a test harness (A main method potentially in another class) that calls only bar. We do not support any kind of annotations that do this for you at the moment.

You can use the Verifier Stub Class to create nonDeterministic values in the test harness that can be used as parameters to bar.
The test driver might look similar to this skeleton:

public class DriverBar {
    public static ... main(String...){
      int x = Verfier.nondetInt()
      bar(x)
    }
}

Then run GDart on the DriverBar class. I hope this helps you to get started.

[BEbillionaireUSD]

Thanks for your reply! I followed your guidance, and it seems to work, but my function involves too many loops, so it takes a very long time. Could you please tell me how to set some extra constraints on the function's parameter(s)?
For example, 0<=x<=10?

In addition, can I record the specific paths with respect to a specific input?
For example, in

public static int bar(int x) {
    if(x>=1){
	return x+1;
    }else if (x<0){
    return x + 3;
   } else {
    return x;
   }
}

When setting x==2, gdart is expected to return x+1 only.