how to understand PathCondition of SymString input

[BryanSJZ]

for the String type param input, I tried a example of GoodbyeWorld.java at the end of this
My problem is, why is there no inputs printed that can cover all paths.
I rewrite printMethodSummary in SymbolicListener.java

private void printMethodSummary(PrintWriter pw, MethodSummary methodSummary) {

    System.out.println("Inputs: " + methodSummary.getSymValues());
    System.out.println("method: " + methodSummary.getMethodName());
    System.out.println("argTypes: " + methodSummary.getArgTypes());
    System.out.println("value: " + methodSummary.getArgValues());
    for (Pair pathCondition : methodSummary.getPathConditions()) {
        System.out.println("pc: " + pathCondition._1);
        System.out.println("return: " + pathCondition._2);
    }
}

to print all the PCs and return. we can know that SPF can generate all the PC to cover all the return value. But how to understand the output? Or, how to print the String input (like "Goodbye, World!" or "i" or "a") how to understand the CONST_30/CONST_1? I only know that SYMSTRING[21] means that the string input have 21 characters.

GoodbyeWorld.java

package strings;

public class GoodbyeWorld {
   public static void main (String [] args) {
      hello("Goodbye, World!");
   }

   public static int hello(String var_1) {
      int i = 0;
      if (var_1.contains("i")){
         return 1;
      }
      if (var_1.length() > 20) {
         return 5;
      }
      if (var_1.endsWith("a")) {
         return 6;
      }
      if (var_1.equals("Goodbye, World!")) {
         return 3;
      }
      return 4;
   }
}

GoodbyeWorld.jpf targ``` et=strings.GoodbyeWorld classpath=${jpf-symbc}/build/examples sourcepath=${jpf-symbc}/src/examples

symbolic.strings=true symbolic.string_dp=z3 symbolic.string_dp_timeout_ms=3000 symbolic.debug=true

symbolic.method= strings.GoodbyeWorld.hello(sym) search.depth_limit = 10 search.multiple_errors=true listener = gov.nasa.jpf.symbc.SymbolicListener

listener = sidechannel.TimingChannelListener

vm.storage.class=nil symbolic.regression_output=true

[sohah]

String support on the current branch is not sound. The latest changes on the String support happened during GSoC 2022. Changes can be found in this link. We need to get that work on String support pushed to SPF's main repo.

@yannicnoller , I think we can close this issue. I'll make another one where we can follow up on the task of importing the changes of string support on a new branch for SPF.