Mercurial > hg > Members > kono > jpf-core

comparison src/main/gov/nasa/jpf/vm/ClassInfo.java @ 17:e15b03204dc7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added a @NoJPFExecution annotation, which sets a NoJPFExec system attr on marked methods during class load time, which gets checked by ThreadInfo.enter(). Useful to flag methods which have to be intercepted/cut off when executing classes under JPF that can also be used outside. Especially useful to avoid the recursive JPF problem that can be caused by tests (which mix classpath and native_classpath). This currently throws a JPFException, but we could also turn this into a AssertionError in the SUT so that we get the SUT stack trace
author Peter Mehlitz <pcmehlitz@gmail.com>
date Mon, 23 Mar 2015 12:54:20 -0700
parents b822e7665585
children db918c531e6d
comparison
equal deleted inserted replaced
16:08ca336d5928 17:e15b03204dc7
361 staticFields[iStatic++] = fi; 361 staticFields[iStatic++] = fi;
362 } else { 362 } else {
363 instanceFields[iInstance++] = fi; 363 instanceFields[iInstance++] = fi;
364 } 364 }
365 365
366 processJPFAttrAnnotation(fi); 366 processJPFAnnotations(fi);
367 } 367 }
368 368
369 iFields = instanceFields; 369 iFields = instanceFields;
370 sFields = staticFields; 370 sFields = staticFields;
371 371
374 } 374 }
375 375
376 protected void setMethod (MethodInfo mi){ 376 protected void setMethod (MethodInfo mi){
377 mi.linkToClass(this); 377 mi.linkToClass(this);
378 methods.put( mi.getUniqueName(), mi); 378 methods.put( mi.getUniqueName(), mi);
379 processJPFAttrAnnotation(mi); 379 processJPFAnnotations(mi);
380 } 380 }
381 381
382 public void setMethods (MethodInfo[] newMethods) { 382 public void setMethods (MethodInfo[] newMethods) {
383 if (newMethods != null && newMethods.length > 0) { 383 if (newMethods != null && newMethods.length > 0) {
384 methods = new LinkedHashMap<String, MethodInfo>(); 384 methods = new LinkedHashMap<String, MethodInfo>();
414 } 414 }
415 } 415 }
416 } 416 }
417 } 417 }
418 418
419 public AnnotationInfo getResolvedAnnotationInfo (String typeName){ 419 protected void processNoJPFExecutionAnnotation(InfoObject infoObj) {
420 AnnotationInfo ai = infoObj.getAnnotation("gov.nasa.jpf.annotation.NoJPFExecution");
421 if (ai != null) {
422 infoObj.addAttr(NoJPFExec.SINGLETON);
423 }
424 }
425
426 protected void processJPFAnnotations(InfoObject infoObj) {
427 processJPFAttrAnnotation(infoObj);
428 processNoJPFExecutionAnnotation(infoObj);
429 }
430
431 public AnnotationInfo getResolvedAnnotationInfo (String typeName){
420 return classLoader.getResolvedAnnotationInfo( typeName); 432 return classLoader.getResolvedAnnotationInfo( typeName);
421 } 433 }
422 434
423 @Override 435 @Override
424 public void setAnnotations(AnnotationInfo[] annotations) { 436 public void setAnnotations(AnnotationInfo[] annotations) {
540 552
541 linkFields(); // computes field offsets 553 linkFields(); // computes field offsets
542 554
543 setAssertionStatus(); 555 setAssertionStatus();
544 processJPFConfigAnnotation(); 556 processJPFConfigAnnotation();
545 processJPFAttrAnnotation(this); 557 processJPFAnnotations(this);
546 loadAnnotationListeners(); 558 loadAnnotationListeners();
547 } 559 }
548 560
549 protected ClassInfo(){ 561 protected ClassInfo(){
550 nClassInfos++; 562 nClassInfos++;
1656 } 1668 }
1657 1669
1658 1670
1659 /** 1671 /**
1660 * Loads the ClassInfo for named class. 1672 * Loads the ClassInfo for named class.
1661 * @param set a Set to which the interface names (String) are added
1662 * @param ifcs class to find interfaceNames for.
1663 */ 1673 */
1664 void loadInterfaceRec (Set<ClassInfo> set, String[] interfaces) throws ClassInfoException { 1674 void loadInterfaceRec (Set<ClassInfo> set, String[] interfaces) throws ClassInfoException {
1665 if (interfaces != null) { 1675 if (interfaces != null) {
1666 for (String iname : interfaces) { 1676 for (String iname : interfaces) {
1667 1677