@ -13,7 +13,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  private  native  Object  externalFunc ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseLocalFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseLocalFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  ret  =  externalFunc ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -25,7 +25,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    return  new  Object ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseCalleeFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseCalleeFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  o  =  skipPointerDerefPreventsSpecInferenceRetObj ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    o . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -36,7 +36,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    return  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseCalleeFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseCalleeFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  ret  =  skipPointerDerefPreventsSpecInferenceRetZero ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  ret ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -45,7 +45,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  j  =  1  /  i ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseInterprocFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipPointerDerefMayCauseInterprocFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  skipPointerDerefPreventsSpecInferenceRetZero ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    divideByParam ( i ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -54,12 +54,12 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    return  ( String )  externalFunc ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  castFailureOnUndefinedObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  castFailureOnUndefinedObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    castExternalPreventsSpecInference ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  callOnCastUndefinedObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  callOnCastUndefinedObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    String  s  =  castExternalPreventsSpecInference ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    s . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -81,54 +81,54 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  private  native  MyObj  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  callOnUndefinedObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  callOnUndefinedObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  ret . retZero ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  callOnUndefinedObjMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  callOnUndefinedObjMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  ret . retOne ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldWriteOnUndefinedObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldWriteOnUndefinedObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . f  =  new  Object ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldWriteOnUndefinedObjMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldWriteOnUndefinedObjMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . f  =  new  Object ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . f . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadOnUndefinedObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadOnUndefinedObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  o  =  ret . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadOnUndefinedObjMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadOnUndefinedObjMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  o  =  ret . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    o . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  recursiveAngelicTypesMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  recursiveAngelicTypesMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  rec1  =  ret . rec ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  rec2  =  rec1 . rec ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  recursiveAngelicTypesMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  recursiveAngelicTypesMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  rec1  =  ret . rec ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    rec1 . rec . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  infiniteMaterializationMayCauseFalseNegative ( boolean  b )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  infiniteMaterializationMayCauseFalseNegative Bad ( boolean  b )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  rec  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    while  ( b )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					      rec  =  rec . rec ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -136,7 +136,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  infiniteMaterializationMayCauseFalsePositive ( boolean  b )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  infiniteMaterializationMayCauseFalsePositive Ok ( boolean  b )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  rec  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    while  ( b )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					      rec  =  rec . rec ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -144,7 +144,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    rec . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  primitiveFieldOfAngelicObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  primitiveFieldOfAngelicObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    if  ( ret . i  = =  0 )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					      int  i  =  1  /  0 ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -153,14 +153,14 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  primitiveFieldOfAngelicObjMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  primitiveFieldOfAngelicObjMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    if  ( ret . i  ! =  0 )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					      int  i  =  1  /  ret . i ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  heapFieldOfAngelicObjMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  heapFieldOfAngelicObjMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  obj  =  ret . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    if  ( obj  = =  ret . f )  { 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -168,7 +168,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  heapFieldOfAngelicObjMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  heapFieldOfAngelicObjMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  obj  =  ret . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    if  ( obj  ! =  ret . f )  { 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -176,7 +176,7 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadAferCastMayCauseFalseNegative ( Iterator < MyObj >  iter )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadAferCastMayCauseFalseNegative Bad ( Iterator < MyObj >  iter )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  iter . next ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  obj  =  ret . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    obj . toString ( ) ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -186,51 +186,51 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  derefParam ( MyObj  obj )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  derefParam Ok ( MyObj  obj )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  f  =  obj . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    f . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam Ok ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . f  =  null ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam Ok ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam ( ret . rec ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam Ok ( ret . rec ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeWithAngelicObjFieldMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  fieldReadInCalleeWithAngelicObjFieldMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . rec . f  =  null ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam ( ret . rec ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    derefParam Ok ( ret . rec ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  accessPathOnParam ( MyObj  obj )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  accessPathOnParam Ok ( MyObj  obj )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  obj . rec ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  f  =  ret . f ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    f . toString ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  accessPathInCalleeMayCauseFalsePositive ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  accessPathInCalleeMayCauseFalsePositive Ok ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    accessPathOnParam ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    accessPathOnParam Ok ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  accessPathInCalleeMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  accessPathInCalleeMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    MyObj  ret  =  externalFunc2 ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    ret . rec . f  =  null ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    accessPathOnParam ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    accessPathOnParam Ok ( ret ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipFunctionInLoopMayCauseFalseNegative ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  skipFunctionInLoopMayCauseFalseNegative Bad ( )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    Object  o  =  null ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    for  ( int  i  =  0 ;  i  <  10 ;  i + + )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					      externalFunc ( ) ; 
 
				
			 
			
		
	
	
		
			
				
					
						
						
						
							
								 
							 
						
					 
				
				 
				 
				
					@ -239,32 +239,32 @@ public class AnalysisStops {
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  // will fail to find error unless spec inference succeeds for all callees
 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  specInferenceMayFailAndCauseFalseNegative ( boolean  b ,  Iterator < MyObj >  iter )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefMayCauseLocalFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  public  void  specInferenceMayFailAndCauseFalseNegative Bad ( boolean  b ,  Iterator < MyObj >  iter )  { 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefMayCauseLocalFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefPreventsSpecInferenceRetObj ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefPreventsSpecInferenceRetZero ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefMayCauseCalleeFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefMayCauseInterprocFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    castFailureOnUndefinedObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    callOnCastUndefinedObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    callOnUndefinedObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    callOnUndefinedObjMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldWriteOnUndefinedObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldWriteOnUndefinedObjMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadOnUndefinedObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadOnUndefinedObjMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    recursiveAngelicTypesMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    recursiveAngelicTypesMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    infiniteMaterializationMayCauseFalseNegative ( b ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    infiniteMaterializationMayCauseFalsePositive ( b ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    primitiveFieldOfAngelicObjMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    primitiveFieldOfAngelicObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    heapFieldOfAngelicObjMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    heapFieldOfAngelicObjMayCauseFalseNegative ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadAferCastMayCauseFalseNegative ( iter ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadInCalleeMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    accessPathInCalleeMayCauseFalsePositive ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefMayCauseCalleeFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    skipPointerDerefMayCauseInterprocFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    castFailureOnUndefinedObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    callOnCastUndefinedObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    callOnUndefinedObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    callOnUndefinedObjMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldWriteOnUndefinedObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldWriteOnUndefinedObjMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadOnUndefinedObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadOnUndefinedObjMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    recursiveAngelicTypesMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    recursiveAngelicTypesMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    infiniteMaterializationMayCauseFalseNegative Bad ( b ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    infiniteMaterializationMayCauseFalsePositive Ok ( b ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    primitiveFieldOfAngelicObjMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    primitiveFieldOfAngelicObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    heapFieldOfAngelicObjMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    heapFieldOfAngelicObjMayCauseFalseNegative Bad ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadAferCastMayCauseFalseNegative Bad ( iter ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadInCalleeMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    fieldReadInCalleeWithAngelicObjFieldMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    accessPathInCalleeMayCauseFalsePositive Ok ( ) ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					    int  i  =  1  /  0 ; 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					  } 
 
				
			 
			
		
	
		
			
				
					 
					 
				
				 
				 
				
					}