Value check fix (#496)

* Add failing test for local var listener. * Fix: Copy/paste error in listener.
javapathfinder · Sep 6, 2024 · 0de04fa · 0de04fa
1 parent 7d2f7a9
commit 0de04fa
Show file tree

Hide file tree

Showing 2 changed files with 15 additions and 1 deletion.
diff --git 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
@@ -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){