Mercurial > hg > Members > kono > jpf-core

diff src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java @ 22:cd7880ab73c7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed JPF_.._Verify.registerChoiceGenerator() to not break and ignore the transition if there are no choices, but to just return the provided default value. Thanks to Pascal Kessell for reporting added a .include_null option for the TypedObjectChoice CG. If it is set (default) 'null' is included in the choice set added a dedicated reg test for TypedObjectChoice, removed the one in DataChoiceTest
author Peter Mehlitz <pcmehlitz@gmail.com>
date Tue, 14 Apr 2015 15:01:25 -0700
parents caa0924e093d
children
line wrap: on
line diff
--- a/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Fri Apr 10 20:53:11 2015 -0700
+++ b/src/main/gov/nasa/jpf/vm/JPF_gov_nasa_jpf_vm_Verify.java	Tue Apr 14 15:01:25 2015 -0700
@@ -345,16 +345,14 @@
 
     String key = id + ".class";
     gen = config.getEssentialInstance(key, cgClass, cgArgTypes, cgArgs);
-
     return gen;
   }
 
   static <T> T registerChoiceGenerator (MJIEnv env, SystemState ss, ThreadInfo ti, ChoiceGenerator<T> cg, T dummyVal){
 
     int n = cg.getTotalNumberOfChoices();
-    if (n == 0) { // we need a CG
-      ss.setIgnored(true);
-      ti.breakTransition( cg.getId());
+    if (n == 0) {
+      // nothing, just return the default value
 
     } else if (n == 1 && !breakSingleChoice) {
       // no choice -> no CG optimization
@@ -497,7 +495,7 @@
     if (!ti.isFirstStepInsn()) { // first time around
       String id = env.getStringObject(idRef);
       ReferenceChoiceGenerator cg = createChoiceGenerator( ReferenceChoiceGenerator.class, ss, id);
-      return registerChoiceGenerator(env,ss,ti,cg, 0);
+      return registerChoiceGenerator(env,ss,ti,cg, MJIEnv.NULL);
 
     } else {
       String id = env.getStringObject(idRef);