Mercurial > hg > Members > kono > jpf-core

comparison 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
comparison
equal deleted inserted replaced
21:caa0924e093d 22:cd7880ab73c7
343 cgArgs[0] = config; 343 cgArgs[0] = config;
344 cgArgs[1] = id; // good thing we are not multithreaded (other fields are const) 344 cgArgs[1] = id; // good thing we are not multithreaded (other fields are const)
345 345
346 String key = id + ".class"; 346 String key = id + ".class";
347 gen = config.getEssentialInstance(key, cgClass, cgArgTypes, cgArgs); 347 gen = config.getEssentialInstance(key, cgClass, cgArgTypes, cgArgs);
348
349 return gen; 348 return gen;
350 } 349 }
351 350
352 static <T> T registerChoiceGenerator (MJIEnv env, SystemState ss, ThreadInfo ti, ChoiceGenerator<T> cg, T dummyVal){ 351 static <T> T registerChoiceGenerator (MJIEnv env, SystemState ss, ThreadInfo ti, ChoiceGenerator<T> cg, T dummyVal){
353 352
354 int n = cg.getTotalNumberOfChoices(); 353 int n = cg.getTotalNumberOfChoices();
355 if (n == 0) { // we need a CG 354 if (n == 0) {
356 ss.setIgnored(true); 355 // nothing, just return the default value
357 ti.breakTransition( cg.getId());
358 356
359 } else if (n == 1 && !breakSingleChoice) { 357 } else if (n == 1 && !breakSingleChoice) {
360 // no choice -> no CG optimization 358 // no choice -> no CG optimization
361 cg.advance(); 359 cg.advance();
362 return cg.getNextChoice(); 360 return cg.getNextChoice();
495 SystemState ss = env.getSystemState(); 493 SystemState ss = env.getSystemState();
496 494
497 if (!ti.isFirstStepInsn()) { // first time around 495 if (!ti.isFirstStepInsn()) { // first time around
498 String id = env.getStringObject(idRef); 496 String id = env.getStringObject(idRef);
499 ReferenceChoiceGenerator cg = createChoiceGenerator( ReferenceChoiceGenerator.class, ss, id); 497 ReferenceChoiceGenerator cg = createChoiceGenerator( ReferenceChoiceGenerator.class, ss, id);
500 return registerChoiceGenerator(env,ss,ti,cg, 0); 498 return registerChoiceGenerator(env,ss,ti,cg, MJIEnv.NULL);
501 499
502 } else { 500 } else {
503 String id = env.getStringObject(idRef); 501 String id = env.getStringObject(idRef);
504 return getNextChoice(ss, id, ReferenceChoiceGenerator.class,Integer.class); 502 return getNextChoice(ss, id, ReferenceChoiceGenerator.class,Integer.class);
505 } 503 }