How to use this for some functions in a huge repo?

[BEbillionaireUSD]

Hi, I would like to express my sincere gratitude for all the hard work and excellent efforts you have put into this project. It has been extremely helpful and inspiring for someone like me who is new to Java and symbolic execution.

I am currently facing some challenges when I hope to jdart for certain functions in a large repo, such as jfreechart[https://github.com/jfree/jfreechart].

1. I am having trouble understanding how the jpf file should be configured. At present, my jpf is as follows...

@include = ../../config/jdart.jpf
target=org.jfree.data.time.TimeSeries
concolic.method.m1=org.jfree.data.time.TimeSeries.createCopy(start:int,end:int)
concolic.method=m1

I hope to run jdart for the following function createCopy

public class TimeSeries extends Series implements Cloneable, Serializable {
...
  public TimeSeries createCopy(int start, int end)
              throws CloneNotSupportedException {
          if (start < 0) {
              throw new IllegalArgumentException("Requires start >= 0.");
          }
          if (end < start) {
              throw new IllegalArgumentException("Requires start <= end.");
          }
          TimeSeries copy = (TimeSeries) super.clone();
          copy.data = new java.util.ArrayList();
          if (this.data.size() > 0) {
              for (int index = start; index <= end; index++) {
                  TimeSeriesDataItem item
                          = (TimeSeriesDataItem) this.data.get(index);
                  TimeSeriesDataItem clone = (TimeSeriesDataItem) item.clone();
                  try {
                      copy.add(clone);
                  }
                  catch (SeriesException e) {
                      e.printStackTrace();
                  }
              }
          }
          return copy;
      }
    
  public static void main(String[] args) {
          System.out.println("In main");
          TimeSeries series = new TimeSeries("Series");
          series.add(new Month(MonthConstants.JANUARY, 2003), 45.0);
          series.add(new Month(MonthConstants.FEBRUARY, 2003), 55.0);
          series.add(new Month(MonthConstants.JUNE, 2003), 35.0);
          series.add(new Month(MonthConstants.NOVEMBER, 2003), 85.0);
          series.add(new Month(MonthConstants.DECEMBER, 2003), 75.0);
  
          try {
              TimeSeries result1 = series.createCopy(
                      new Month(MonthConstants.NOVEMBER, 2002),
                      new Month(MonthConstants.DECEMBER, 2002));
          }
          catch (CloneNotSupportedException e) {
          }
      }
  }
  

The static main function is manually constructed. This brings up the second question. In a large repo with numerous functions, do I have to manually construct a main function for each function?

The above content leads to a result where symbolic execution is not running correctly, but there is also no error reported.

[FINEST] ============ End JPF Config ============
[FINEST] Producer(): perturb.m1
[FINEST] ConcolicListener()
[FINEST] Producer.getChoiceGeneratorType()
[FINEST] ConcolicListener.searchStarted(): -1
In main
[FINEST] ConcolicListener.searchFinished(): -1
[FINEST] JDart.run() -- end
[INFO] Profiling:
JDART-run: 413 ms [0 s]
JPF-boot: 133 ms [0 s]

[INFO] Completed Analyses: 0
Completed Analyses: 0

I would like to know where the problem lies. Is it that I misunderstood the configuration and jdart?

I'm looking forward to your reply.

[mmuesly]

We discontinued the development of JDart in favor of GDart: https://github.com/tudo-aqua/gdart and I am sorry, but I will not have the capacity to debug this problem with you.

To run the concept on modern software, I strongly recommend trying out GDart and I might support you there, if required.

Regarding: In a large repo with numerous functions, do I have to manually construct a main function for each function?
Yes, you need to setup drivers for these functions.