@ -1566,11 +1566,15 @@ let is_only_pt_by_fld_or_param_nonnull pdesc tenv prop deref_exp =
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					let  check_dereference_error  tenv  pdesc  ( prop  :  Prop . normal  Prop . t )  lexp  loc  = 
 
					 
					 
					 
					let  check_dereference_error  tenv  pdesc  ( prop  :  Prop . normal  Prop . t )  lexp  loc  = 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  let  pname  =  Procdesc . get_proc_name  pdesc  in 
 
					 
					 
					 
					  let  pname  =  Procdesc . get_proc_name  pdesc  in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  let  root  =  Exp . root_of_lexp  lexp  in 
 
					 
					 
					 
					  let  root  =  Exp . root_of_lexp  lexp  in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  let  nullable_var_opt  =  is_only_pt_by_fld_or_param_nullable  pdesc  tenv  prop  root  in 
 
					 
					 
					 
					  let  nullable_var_opt  = 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					  let  is_deref_of_nullable  = 
 
					 
					 
					 
					 
				
			 
			
		
	
		
		
	
		
		
			
				
					
					 
					 
					 
					    let  is_definitely_non_null  exp  prop  =  Prover . check_disequal  tenv  prop  exp  Exp . zero  in 
 
					 
					 
					 
					    let  is_definitely_non_null  exp  prop  =  Prover . check_disequal  tenv  prop  exp  Exp . zero  in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					    Config . report_nullable_inconsistency  &&  Option . is_some  nullable_var_opt 
 
					 
					 
					 
					    if  Config . report_nullable_inconsistency  then 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					    &&  not  ( is_definitely_non_null  root  prop ) 
 
					 
					 
					 
					      match  is_only_pt_by_fld_or_param_nullable  pdesc  tenv  prop  root  with 
 
				
			 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					 
					 
					 
					 
					 
					 
					 
					      |  Some  _  as  nullable_var  when  not  ( is_definitely_non_null  root  prop )  -> 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					 
					 
					 
					 
					          nullable_var 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					 
					 
					 
					 
					      |  _  -> 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					 
					 
					 
					 
					          None 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					 
					 
					 
					 
					    else  None 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  in 
 
					 
					 
					 
					  in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  let  relevant_attributes_getters  =  [ Attribute . get_resource  tenv ;  Attribute . get_undef  tenv ]  in 
 
					 
					 
					 
					  let  relevant_attributes_getters  =  [ Attribute . get_resource  tenv ;  Attribute . get_undef  tenv ]  in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  let  get_relevant_attributes  exp  = 
 
					 
					 
					 
					  let  get_relevant_attributes  exp  = 
 
				
			 
			
		
	
	
		
		
			
				
					
						
							
								 
							 
						
						
							
								 
							 
						
						
					 
					 
					@ -1597,21 +1601,18 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc =
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					        in 
 
					 
					 
					 
					        in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					        get_relevant_attributes  root_no_offset 
 
					 
					 
					 
					        get_relevant_attributes  root_no_offset 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  in 
 
					 
					 
					 
					  in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					  (  if  Prover . check_zero  tenv  ( Exp . root_of_lexp  root )  | |  is_deref_of_nullable   then 
 
					 
					 
					 
					  (  if  Prover . check_zero  tenv  ( Exp . root_of_lexp  root )  | |  Option . is_some  nullable_var_opt   then 
 
				
			 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					 
					 
					 
					    let  deref_str  = 
 
					 
					 
					 
					    let  deref_str  = 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					      if  is_deref_of_nullable  then 
 
					 
					 
					 
					      match  nullable_var_opt  with 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					        match  nullable_var_opt  with 
 
					 
					 
					 
					      |  Some  str  -> 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					        |  Some  str  -> 
 
					 
					 
					 
					          if  is_weak_captured_var  pdesc  str  then  Localise . deref_str_weak_variable_in_block  None  str 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					            if  is_weak_captured_var  pdesc  str  then 
 
					 
					 
					 
					          else  Localise . deref_str_nullable  None  str 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					              Localise . deref_str_weak_variable_in_block  None  str 
 
					 
					 
					 
					      |  None  -> 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					            else  Localise . deref_str_nullable  None  str 
 
					 
					 
					 
					          Localise . deref_str_null  None 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					        |  None  -> 
 
					 
					 
					 
					 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					            Localise . deref_str_nullable  None  " " 
 
					 
					 
					 
					 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					      else  Localise . deref_str_null  None 
 
					 
					 
					 
					 
				
			 
			
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					 
					 
					 
					    in 
 
					 
					 
					 
					    in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					    let  err_desc  = 
 
					 
					 
					 
					    let  err_desc  = 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					      Errdesc . explain_dereference  pname  tenv  ~ use_buckets : true  ~ is_nullable : is_deref_of_nullable  
 
					 
					 
					 
					      Errdesc . explain_dereference  pname  tenv  ~ use_buckets : true 
 
				
			 
			
				
				
			
		
	
		
		
			
				
					
					 
					 
					 
					        deref_str  prop  loc 
 
					 
					 
					 
					        ~ is_nullable : ( Option . is_some  nullable_var_opt )  deref_str  prop  loc 
 
				
			 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					 
					 
					 
					    in 
 
					 
					 
					 
					    in 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					    if  Localise . is_parameter_not_null_checked_desc  err_desc  then 
 
					 
					 
					 
					    if  Localise . is_parameter_not_null_checked_desc  err_desc  then 
 
				
			 
			
		
	
		
		
			
				
					
					 
					 
					 
					      raise  ( Exceptions . Parameter_not_null_checked  ( err_desc ,  _ _ POS__ ) ) 
 
					 
					 
					 
					      raise  ( Exceptions . Parameter_not_null_checked  ( err_desc ,  _ _ POS__ ) )