Mercurial > hg > Members > kono > jpf-core

diff src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java @ 21:caa0924e093d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
reshuffled Event hierarchy, introducing SystemEvent, with CheckEvent and ControlEvent being subclasses of SystemEvent added Loggable.setLogLevel changed old UserHeuristic to use a Verify.heuristicValue instead of a hardwired "Main" class with hardwired fields (which was just an outdated leftover). Call Verify.setHeuristicValue() to control state priorities from the SUT. This also fixes the bug that UserHeuristic was not properly checking for "Main" resolution.
author Peter Mehlitz <pcmehlitz@gmail.com>
date Fri, 10 Apr 2015 20:53:11 -0700
parents f6886b2bda4a
children cd7880ab73c7
line wrap: on
line diff
--- a/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Mon Apr 06 12:08:03 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Fri Apr 10 20:53:11 2015 -0700
@@ -53,7 +53,7 @@
  * its use is supposed to be JPF global (without classloader namespaces)
  */
 public class JPF_gov_nasa_jpf_vm_Verify extends NativePeer {
-  static final int MAX_COUNTERS = 10;
+  static final int MAX_COUNTERS = 127;
 
   static boolean isInitialized;
   
@@ -61,6 +61,7 @@
   static int[] counter;
   static IntTable<String> map;
 
+  public static int heuristicSearchValue;
   
   static boolean supportIgnorePath;
   static boolean breakSingleChoice;
@@ -85,6 +86,8 @@
       breakSingleChoice = conf.getBoolean("cg.break_single_choice");
       enableAtomic = conf.getBoolean("cg.enable_atomic", true);
 
+      heuristicSearchValue = conf.getInt("search.heuristic.default_value");
+
       counter = null;
       map = null;
       
@@ -106,7 +109,7 @@
 
       RunRegistry.getDefaultRegistry().addListener( new RunListener() {
         @Override
-		public void reset (RunRegistry reg){
+		    public void reset (RunRegistry reg){
           isInitialized = false;
         }
       });
@@ -955,7 +958,7 @@
    */
   @MJI
   public static int random__I__I (MJIEnv env, int clsObjRef, int x) {
-   return getInt__II__I( env, clsObjRef, 0, x);
+   return getInt__II__I(env, clsObjRef, 0, x);
   }
 
   static void boring__Z__V (MJIEnv env, int clsObjRef, boolean b) {
@@ -986,6 +989,20 @@
     jpf.getSearch().terminate();
   }
 
+  @MJI public static void setHeuristicSearchValue__I__V (MJIEnv env, int clsObjRef, int val){
+    heuristicSearchValue =  val;
+  }
+
+  @MJI public static int getHeuristicSearchValue____I (MJIEnv env, int clsObjRef){
+    return heuristicSearchValue;
+  }
+
+  @MJI public static void resetHeuristicSearchValue____V (MJIEnv env, int clsObjRef){
+    heuristicSearchValue = config.getInt("search.heuristic.default_value");
+  }
+
+
+
   @MJI
   public static boolean isTraceReplay____Z (MJIEnv env, int clsObjRef) {
     return env.getVM().isTraceReplay();