java - JPF 符号字符串未生成预期 PC 的 [Java 路径查找器]

Question

我正在尝试在符号字符串上运行 Jpf，但它没有生成预期的输出。以下是我正在尝试的玩具程序。

import gov.nasa.jpf.symbc.Debug;
import static org.junit.Assert.*;

public class Toy {
public static void main(String args[]) {
    
    String s1,s2,s3;
    s1=Debug.makeSymbolicString("s1");
    s2=Debug.makeSymbolicString("s2");
    s3=Debug.makeSymbolicString("s3");
    
    checkEqual(s1,s2,s3);
}

static void checkEqual(String s1,String s2,String s3) {
    if(!s1.equals(s3)) 
        {
        if(!s2.equals(s3))  {
                
                System.out.println("s1.equals(s3)="+s1.equals(s3)+"\n");
                System.out.println("s2.equals(s3)="+s2.equals(s3)+"\n");
        }
    }
    System.out.println(Debug.getSolvedPC());
    }   
}

.jpf 文件如下：

target=Toy
classpath=${jpf-symbc}/build/examples
sourcepath=${jpf-symbc}/src/examples

symbolic.strings = true
symbolic.debug=true

在嵌套的 if 条件中，我正在打印字符串比较的值，只有当字符串 s1,s2 不等于 s3 时，才应该打印打印语句。我还使用 symbolic.debug=true 打印了 PC

以下是我有疑问的输出片段。这里的输出表明 s1,s2 同时与 s3 相等且不相等。这怎么可能？打印语句也显示“s2.equals(s3)=true”，那么程序不应该进入 if 块。

string analysis: SPC # = 4
(s2 equals s3) && (s1 equals s3) && (s2 notequals s3) && (s1 notequals s3)
NPC constraint # = 0
s2.equals(s3)=true

string analysis: SPC # = 4
(s2 equals s3) && (s1 equals s3) && (s2 notequals s3) && (s1 notequals s3) 
NPC constraint # = 0
constraint # = 0
## Warning: empty path condition
### PCs: total:9 sat:9 unsat:0

当我使用 int 而不是 String 时，代码可以工作。如果你能帮助我，那就太好了。如果我的 jpf 配置中缺少某些内容，请告诉我。先感谢您

标签： javajpf