From: bdemsky <bdemsky@uci.edu>
Date: Thu, 1 Aug 2019 21:18:26 +0000 (-0700)
Subject: Add constanttime class
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=a25e4f9ce1b9f5aab028a18ec09c1e3471bef36a;ds=inline

Add constanttime class
---

diff --git a/jpf.properties b/jpf.properties
index 0bdb036..8c0270d 100644
--- a/jpf.properties
+++ b/jpf.properties
@@ -293,7 +293,7 @@ vm.sysprop.source = SELECTED
 #vm.sysprop.keys =
 
 # class we use to model execution time
-vm.time.class = gov.nasa.jpf.vm.SystemTime
+vm.time.class = gov.nasa.jpf.vm.ConstantTime
 
 # if this is set to true, we throw an exception if we encounter any orphan native peer methods
 vm.no_orphan_methods = false
diff --git a/main.jpf b/main.jpf
index c044182..04f14be 100644
--- a/main.jpf
+++ b/main.jpf
@@ -5,9 +5,9 @@ listener=gov.nasa.jpf.listener.VariableConflictTracker
 
 # Potentially conflicting variables
 # Alarms
-#variables=currentAlarm
+variables=currentAlarm
 # Locks
-variables=currentLock
+#variables=currentLock
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
diff --git a/src/main/gov/nasa/jpf/vm/ConstantTime.java b/src/main/gov/nasa/jpf/vm/ConstantTime.java
new file mode 100644
index 0000000..889abcd
--- /dev/null
+++ b/src/main/gov/nasa/jpf/vm/ConstantTime.java
@@ -0,0 +1,42 @@
+/*
+ * Copyright (C) 2014, United States Government, as represented by the
+ * Administrator of the National Aeronautics and Space Administration.
+ * All rights reserved.
+ *
+ * The Java Pathfinder core (jpf-core) platform is licensed under the
+ * Apache License, Version 2.0 (the "License"); you may not use this file except
+ * in compliance with the License. You may obtain a copy of the License at
+ * 
+ *        http://www.apache.org/licenses/LICENSE-2.0. 
+ *
+ * Unless required by applicable law or agreed to in writing, software
+ * distributed under the License is distributed on an "AS IS" BASIS,
+ * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ * See the License for the specific language governing permissions and 
+ * limitations under the License.
+ */
+package gov.nasa.jpf.vm;
+
+import gov.nasa.jpf.Config;
+
+/**
+ * simple delegating TimeModel implementation that just returns System time.
+ * While elapsed time is not path sensitive, it is at least strictly increasing
+ * along any given path
+ */
+public class ConstantTime implements TimeModel {
+
+  public ConstantTime(VM vm, Config conf){
+    // we don't need these, but it speeds up VM initialization
+  }
+  
+  @Override
+  public long currentTimeMillis() {
+    return 1564694080896L;
+  }
+
+  @Override
+  public long nanoTime() {
+    return 365341665679019L;
+  }
+}