ApacheCLI issues - sohah/VeritestingTransformations GitHub Wiki

  1. The original ApacheCLI used a LinkedHashMap inside Options.java methods that check if a Option exists (hasOption()) and, if it does, get the Option (getOption()). But, neither does SPF branch inside a HashMap.containsKey() method nor does it return a symbolic boolean from it, causing the symbolic exploration from this point on to be lost. I was able to confirm this by replacing this HashMap lookup with a simple enumeration of the HashMap which did cause more symbolic branching to be explored by SPF.
  2. With an increase in the value of maxStaticExplorationDepth in VeritestingListener and with the last argument to mainProcess set to symbolic, Java Ranger summarizes and instantiates a region inside one of the Parser.parse() methods which branches on stopOnNonOption. But, this branching makes other state symbolic and therefore, does not lead to a reduction in the execution path count.
  3. Java Ranger reduces the execution path count significantly but increases execution time with most of its execution time spent in solving, most of that time spent in "parsing" aka communicating the query to the solver. Incremental solving should alleviate this problem for us.