How to solve: java.lang.NoSuchMethodException when running JPF-Symbc

[Xuan Bach]

Hi All,

I have successfully run JPF-Symbc on many small example. Now I am trying to run it with a larger target application, which is
common math library. I am running into the following exception thrown by JPF (bellow). I was wondering what could the
the source of the problem? I suppose I need to model some native peer class myself?
Note that the SUT is common math library. I created a test driver to call to a test method, and run JPF-symbc on that driver.

Running Symbolic PathFinder ...
symbolic.dp=iasolver
symbolic.string_dp_timeout_ms=0
symbolic.string_dp=none
symbolic.max_pc_length=2147483647
symbolic.max_pc_msec=0
symbolic.min_int=-1000000
symbolic.max_int=1000000
symbolic.min_double=-8.0
symbolic.max_double=7.0
JavaPathfinder core system v8.0 (rev 31) - (C) 2005-2014 United States Government. All rights reserved.


====================================================== system under test
org.apache.commons.math.distribution.CustomUnitTestCaller.main("/home/dxble/workspace/jangelix/angelix/instrumented/solvedPC.txt","true")

====================================================== search started: 9/17/16 1:20 AM
Creating and running test driver...
[WARNING] orphan NativePeer method: java.util.ResourceBundle.getClassContext()[Ljava/lang/Class;

====================================================== error 1
gov.nasa.jpf.vm.NoUncaughtExceptionsProperty
java.lang.ClassNotFoundException: class not found: java.lang.NoSuchMethodException!!
    at java.text.MessageFormat.subformat(MessageFormat.java:1271)
    at java.text.MessageFormat.format(MessageFormat.java:865)
    at java.text.Format.format(Format.java:41)
    at org.apache.commons.math.MathException.buildMessage(MathException.java:85)
    at org.apache.commons.math.MathException.<init>(MathException.java:106)
    at org.apache.commons.math.ConvergenceException.<init>(ConvergenceException.java:45)
    at org.apache.commons.math.MaxIterationsExceededException.<init>(MaxIterationsExceededException.java:43)
    at org.apache.commons.math.special.Gamma.regularizedGammaP(Gamma.java:181)
    at org.apache.commons.math.special.Erf.erf(Erf.java:51)
    at org.apache.commons.math.distribution.NormalDistributionImpl.cumulativeProbability(NormalDistributionImpl.java:126)
    at org.apache.commons.math.distribution.AbstractContinuousDistribution$1.value(AbstractContinuousDistribution.java:73)
    at org.apache.commons.math.analysis.solvers.UnivariateRealSolverUtils.bracket(UnivariateRealSolverUtils.java:195)
    at org.apache.commons.math.analysis.solvers.UnivariateRealSolverUtils.bracket(UnivariateRealSolverUtils.java:129)
    at org.apache.commons.math.distribution.AbstractContinuousDistribution.inverseCumulativeProbability(AbstractContinuousDistribution.java:85)
    at org.apache.commons.math.distribution.NormalDistributionImpl.inverseCumulativeProbability(NormalDistributionImpl.java:162)
    at org.apache.commons.math.distribution.NormalDistributionTest.testMath280(NormalDistributionTest.java:171)
    at org.apache.commons.math.distribution.CustomUnitTestCaller.main(CustomUnitTestCaller.java:19)


====================================================== snapshot #1
thread java.lang.Thread:{id:0,name:main,status:RUNNING,priority:5,isDaemon:false,lockCount:0,suspendCount:0}
  call stack:
    at java.text.MessageFormat.subformat(MessageFormat.java:1271)
    at java.text.MessageFormat.format(MessageFormat.java:865)
    at java.text.Format.format(Format.java:41)
    at org.apache.commons.math.MathException.buildMessage(MathException.java:85)
    at org.apache.commons.math.MathException.<init>(MathException.java:106)
    at org.apache.commons.math.ConvergenceException.<init>(ConvergenceException.java:45)
    at org.apache.commons.math.MaxIterationsExceededException.<init>(MaxIterationsExceededException.java:43)
    at org.apache.commons.math.special.Gamma.regularizedGammaP(Gamma.java:181)
    at org.apache.commons.math.special.Erf.erf(Erf.java:51)
    at org.apache.commons.math.distribution.NormalDistributionImpl.cumulativeProbability(NormalDistributionImpl.java:126)
    at org.apache.commons.math.distribution.AbstractContinuousDistribution$1.value(AbstractContinuousDistribution.java:73)
    at org.apache.commons.math.analysis.solvers.UnivariateRealSolverUtils.bracket(UnivariateRealSolverUtils.java:195)
    at org.apache.commons.math.analysis.solvers.UnivariateRealSolverUtils.bracket(UnivariateRealSolverUtils.java:129)
    at org.apache.commons.math.distribution.AbstractContinuousDistribution.inverseCumulativeProbability(AbstractContinuousDistribution.java:85)
    at org.apache.commons.math.distribution.NormalDistributionImpl.inverseCumulativeProbability(NormalDistributionImpl.java:162)
    at org.apache.commons.math.distribution.NormalDistributionTest.testMath280(NormalDistributionTest.java:171)
    at org.apache.commons.math.distribution.CustomUnitTestCaller.main(CustomUnitTestCaller.java:19)


====================================================== results
error #1: gov.nasa.jpf.vm.NoUncaughtExceptionsProperty "java.lang.ClassNotFoundException: class not found:..."

[Xuan Bach]

It seems that using jpf-nhandler fixes the problem. I set the option in nhandler to delegate the method java.text.Format.format, then it runs without any exception thrown by jpf.

Vào 01:33:10 UTC-4 Thứ Bảy, ngày 17 tháng 9 năm 2016, Xuan Bach đã viết: