diff --git a/src/main/gov/nasa/jpf/listener/NumericValueChecker.java b/src/main/gov/nasa/jpf/listener/NumericValueChecker.java index ee7da7e6..7c90d59b 100644 --- a/src/main/gov/nasa/jpf/listener/NumericValueChecker.java +++ b/src/main/gov/nasa/jpf/listener/NumericValueChecker.java @@ -69,7 +69,7 @@ String check (long v){ String check (double v){ if (v < min){ return String.format("%f < %f", v, min); - } else if (v > (long)max){ + } else if (v > (double)max){ return String.format("%f > %f", v, max); } return null; diff --git a/src/tests/gov/nasa/jpf/test/mc/data/NumericValueCheckerTest.java b/src/tests/gov/nasa/jpf/test/mc/data/NumericValueCheckerTest.java index 05403962..851e4d7b 100644 --- a/src/tests/gov/nasa/jpf/test/mc/data/NumericValueCheckerTest.java +++ b/src/tests/gov/nasa/jpf/test/mc/data/NumericValueCheckerTest.java @@ -33,6 +33,10 @@ static class C1 { void setValue(double v){ d = v; } + + void setLocalVar() { + double x = 0.5; + } } @Test @@ -47,6 +51,16 @@ public void testField(){ } } + @Test + public void testLocalVar() { + if (verifyNoPropertyViolation("+listener=.listener.NumericValueChecker", + "+range.vars=x", + "+range.x.var=*$C1.setLocalVar():x", + "+range.x.max=0.9")) { + C1 c1= new C1(); + c1.setLocalVar(); + } + } static class C2 { void doSomething(int d){