Add constanttime class
authorbdemsky <bdemsky@uci.edu>
Thu, 1 Aug 2019 21:18:26 +0000 (14:18 -0700)
committerbdemsky <bdemsky@uci.edu>
Thu, 1 Aug 2019 21:18:26 +0000 (14:18 -0700)
jpf.properties
main.jpf
src/main/gov/nasa/jpf/vm/ConstantTime.java [new file with mode: 0644]

index 0bdb036..8c0270d 100644 (file)
@@ -293,7 +293,7 @@ vm.sysprop.source = SELECTED
 #vm.sysprop.keys =
 
 # class we use to model execution time
 #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
 
 # if this is set to true, we throw an exception if we encounter any orphan native peer methods
 vm.no_orphan_methods = false
index c044182..04f14be 100644 (file)
--- a/main.jpf
+++ b/main.jpf
@@ -5,9 +5,9 @@ listener=gov.nasa.jpf.listener.VariableConflictTracker
 
 # Potentially conflicting variables
 # Alarms
 
 # Potentially conflicting variables
 # Alarms
-#variables=currentAlarm
+variables=currentAlarm
 # Locks
 # Locks
-variables=currentLock
+#variables=currentLock
 # Thermostats
 #variables=currentHeatingSetpoint,thermostatSetpoint,currentCoolingSetpoint,thermostatOperatingState,thermostatFanMode,currentThermostatMode
 # Switches
 # 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 (file)
index 0000000..889abcd
--- /dev/null
@@ -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;
+  }
+}