From 0de04fa90871624b55eb501a5bb984234c70d3ef Mon Sep 17 00:00:00 2001
From: cyrille-artho <cyrille-artho@users.noreply.github.com>
Date: Fri, 6 Sep 2024 13:28:52 +0200
Subject: [PATCH] Value check fix (#496)

* Add failing test for local var listener.

* Fix: Copy/paste error in listener.
---
 .../gov/nasa/jpf/listener/NumericValueChecker.java |  2 +-
 .../jpf/test/mc/data/NumericValueCheckerTest.java  | 14 ++++++++++++++
 2 files changed, 15 insertions(+), 1 deletion(-)

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){