search

SymbolicPathFinder / jpf-symbc

Symbolic PathFinder
https://github.com/SymbolicPathFinder/jpf-symbc
130 stars 91 forks source link

Divide by zero unsafe code report safe #100

Open Ao-senXiong opened 3 months ago

Ao-senXiong commented 3 months ago

.jpf

classpath=/Users/aosenxiong/spf/spf-java11/jpf-symbc/build/classes:/var/folders/0v/xw7b2vwd7bzd3n8b3kc0gxj00000gn/T/jpf-benchmark.XXXXXX.iX86tsSpOU/target/classes:/Users/aosenxiong/spf/spf-java11/sv-benchmarks/java/common
symbolic.dp=z3bitvector
symbolic.bvlength=64
search.depth_limit=200
symbolic.strings=true
symbolic.string_dp=ABC
symbolic.string_dp_timeout_ms=3000
symbolic.lazy=on
symbolic.arrays=true

Java

public class Main {
  public static void main(String args[]) {
    try {
      double i = 0;
      double j = 10 / i;
    } catch (ArithmeticException exc) {
      assert false;
    }
  }
}