@ -117,9 +117,9 @@ type find_canonical_duplicate = Procdesc.Node.t -> Procdesc.Node.t
 
			
		
	
		
		
			
				
					
					type  checks  =  { eradicate :  bool ;  check_ret_type :  check_return_type  list } type  checks  =  { eradicate :  bool ;  check_ret_type :  check_return_type  list }  
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					(* *  Typecheck an expression.  *) (* *  Typecheck an expression.  *)  
			
		
	
		
		
			
				
					
					let  rec  typecheck_expr  ( { IntraproceduralAnalysis . tenv ;  }  as  analysis_data )  ~ nullsafe_mode  let  rec  typecheck_expr  ( { IntraproceduralAnalysis . tenv ;  proc_desc = curr_proc  _desc }  as  analysis_data )  
			
				
				
			
		
	
		
		
			
				
					
					    find_canonical_duplicate  visited  checks  node  instr_ref  typestate  e  tr_default  loc  :  
    ~ nullsafe_mode  find_canonical_duplicate  visited  checks  node  instr_ref  typestate  e  tr_default  loc 
 
			
				
				
			
		
	
		
		
			
				
					
					    TypeState . range  = 
    :  TypeState . range  = 
 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
	
		
		
			
				
					
					  L . d_with_indent  ~ name : " typecheck_expr "  ~ pp_result : TypeState . pp_range  ( fun  ()  -> 
  L . d_with_indent  ~ name : " typecheck_expr "  ~ pp_result : TypeState . pp_range  ( fun  ()  -> 
 
			
		
	
		
		
			
				
					
					      L . d_printfln  " Expr: %a "  Exp . pp  e  ; 
      L . d_printfln  " Expr: %a "  Exp . pp  e  ; 
 
			
		
	
		
		
			
				
					
					      match  e  with 
      match  e  with 
 
			
		
	
	
		
		
			
				
					
						
							
								 
						
						
							
								 
						
						
					 
					@ -161,8 +161,14 @@ let rec typecheck_expr ({IntraproceduralAnalysis.tenv; _} as analysis_data) ~nul
 
			
		
	
		
		
			
				
					
					              loc 
              loc 
 
			
		
	
		
		
			
				
					
					          in 
          in 
 
			
		
	
		
		
			
				
					
					          let  object_origin  =  InferredNullability . get_simple_origin  inferred_nullability  in 
          let  object_origin  =  InferredNullability . get_simple_origin  inferred_nullability  in 
 
			
		
	
		
		
			
				
					
					          let  curr_procname  = 
 
			
		
	
		
		
			
				
					
					            Procdesc . get_proc_name  curr_proc_desc 
 
			
		
	
		
		
			
				
					
					            | >  Procname . as_java_exn 
 
			
		
	
		
		
			
				
					
					                 ~ explanation : " typecheck_expr: attempt to typecheck non-Java method " 
 
			
		
	
		
		
			
				
					
					          in 
 
			
		
	
		
		
			
				
					
					          let  class_under_analysis  =  Procname . Java . get_class_type_name  curr_procname  in 
 
			
		
	
		
		
			
				
					
					          let  tr_new  = 
          let  tr_new  = 
 
			
		
	
		
		
			
				
					
					            match  AnnotatedField . get  tenv  field_name  typ  with 
            match  AnnotatedField . get  tenv  field_name  ~ class_typ : typ  ~ class_under_analysis   with 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					            |  Some  AnnotatedField . { annotated_type =  field_type }  -> 
            |  Some  AnnotatedField . { annotated_type =  field_type }  -> 
 
			
		
	
		
		
			
				
					
					                (  field_type . typ 
                (  field_type . typ 
 
			
		
	
		
		
			
				
					
					                ,  InferredNullability . create 
                ,  InferredNullability . create 
 
			
		
	
	
		
		
			
				
					
						
							
								 
						
						
							
								 
						
						
					 
					@ -252,12 +258,13 @@ let funcall_exp_to_original_pvar_exp tenv curr_pname typestate exp ~is_assignmen
 
			
		
	
		
		
			
				
					
					      exp 
      exp 
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					
 
			
		
	
		
		
			
				
					
					let  add_field_to_typestate_if_absent  tenv  access_loc  typestate  pvar  object_origin  field_name  typ  = let  add_field_to_typestate_if_absent  tenv  access_loc  typestate  pvar  object_origin  field_name  
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					    ~ field_class_typ  ~ class_under_analysis  = 
 
			
		
	
		
		
			
				
					
					  match  TypeState . lookup_pvar  pvar  typestate  with 
  match  TypeState . lookup_pvar  pvar  typestate  with 
 
			
		
	
		
		
			
				
					
					  |  Some  _  -> 
  |  Some  _  -> 
 
			
		
	
		
		
			
				
					
					      typestate 
      typestate 
 
			
		
	
		
		
			
				
					
					  |  None  ->  ( 
  |  None  ->  ( 
 
			
		
	
		
		
			
				
					
					    match  AnnotatedField . get  tenv  field_name  with 
    match  AnnotatedField . get  tenv  field_name  ~ class_ typ: field_class_typ  ~ class_under_analysis with 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					    |  Some  AnnotatedField . { annotated_type =  field_type }  -> 
    |  Some  AnnotatedField . { annotated_type =  field_type }  -> 
 
			
		
	
		
		
			
				
					
					        let  range  = 
        let  range  = 
 
			
		
	
		
		
			
				
					
					          (  field_type . typ 
          (  field_type . typ 
 
			
		
	
	
		
		
			
				
					
						
							
								 
						
						
							
								 
						
						
					 
					@ -303,7 +310,7 @@ let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_
 
			
		
	
		
		
			
				
					
					              default  ) 
              default  ) 
 
			
		
	
		
		
			
				
					
					      |  Exp . Lvar  _  -> 
      |  Exp . Lvar  _  -> 
 
			
		
	
		
		
			
				
					
					          default 
          default 
 
			
		
	
		
		
			
				
					
					      |  Exp . Lfield  ( exp_ ,  fn ,  )  -> 
      |  Exp . Lfield  ( exp_ ,  fn ,  field_class_ typ)  -> 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					          let  inner_origin  = 
          let  inner_origin  = 
 
			
		
	
		
		
			
				
					
					            (  match  exp_  with 
            (  match  exp_  with 
 
			
		
	
		
		
			
				
					
					            |  Exp . Lvar  pvar  -> 
            |  Exp . Lvar  pvar  -> 
 
			
		
	
	
		
		
			
				
					
						
							
								 
						
						
							
								 
						
						
					 
					@ -330,13 +337,19 @@ let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_
 
			
		
	
		
		
			
				
					
					          let  pvar_to_str  pvar  = 
          let  pvar_to_str  pvar  = 
 
			
		
	
		
		
			
				
					
					            if  Exp . is_this  ( Exp . Lvar  pvar )  then  " "  else  Pvar . to_string  pvar  ^  " _ " 
            if  Exp . is_this  ( Exp . Lvar  pvar )  then  " "  else  Pvar . to_string  pvar  ^  " _ " 
 
			
		
	
		
		
			
				
					
					          in 
          in 
 
			
		
	
		
		
			
				
					
					          let  class_under_analysis  = 
 
			
		
	
		
		
			
				
					
					            Procname . Java . get_class_type_name 
 
			
		
	
		
		
			
				
					
					              ( Procname . as_java_exn  curr_pname 
 
			
		
	
		
		
			
				
					
					                 ~ explanation : " Attempt to typecheck non-Java procname " ) 
 
			
		
	
		
		
			
				
					
					          in 
 
			
		
	
		
		
			
				
					
					          let  res  = 
          let  res  = 
 
			
		
	
		
		
			
				
					
					            match  exp'  with 
            match  exp'  with 
 
			
		
	
		
		
			
				
					
					            |  Exp . Lvar  pv  when  is_parameter_field  pv  | |  is_static_field  pv  -> 
            |  Exp . Lvar  pv  when  is_parameter_field  pv  | |  is_static_field  pv  -> 
 
			
		
	
		
		
			
				
					
					                let  fld_name  =  pvar_to_str  pv  ^  Fieldname . to_string  fn  in 
                let  fld_name  =  pvar_to_str  pv  ^  Fieldname . to_string  fn  in 
 
			
		
	
		
		
			
				
					
					                let  pvar  =  Pvar . mk  ( Mangled . from_string  fld_name )  curr_pname  in 
                let  pvar  =  Pvar . mk  ( Mangled . from_string  fld_name )  curr_pname  in 
 
			
		
	
		
		
			
				
					
					                let  typestate'  = 
                let  typestate'  = 
 
			
		
	
		
		
			
				
					
					                  add_field_to_typestate_if_absent  tenv  loc  typestate  pvar  inner_origin  fn  typ 
                  add_field_to_typestate_if_absent  tenv  loc  typestate  pvar  inner_origin  fn 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					                    ~ field_class_typ  ~ class_under_analysis 
 
			
		
	
		
		
			
				
					
					                in 
                in 
 
			
		
	
		
		
			
				
					
					                ( Exp . Lvar  pvar ,  typestate' ) 
                ( Exp . Lvar  pvar ,  typestate' ) 
 
			
		
	
		
		
			
				
					
					            |  Exp . Lfield  ( _ exp' ,  fn' ,  _ )  when  Fieldname . is_java_outer_instance  fn'  -> 
            |  Exp . Lfield  ( _ exp' ,  fn' ,  _ )  when  Fieldname . is_java_outer_instance  fn'  -> 
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -344,7 +357,8 @@ let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_
 
			
		
	
		
		
			
				
					
					                let  fld_name  =  Fieldname . to_string  fn'  ^  " _ "  ^  Fieldname . to_string  fn  in 
                let  fld_name  =  Fieldname . to_string  fn'  ^  " _ "  ^  Fieldname . to_string  fn  in 
 
			
		
	
		
		
			
				
					
					                let  pvar  =  Pvar . mk  ( Mangled . from_string  fld_name )  curr_pname  in 
                let  pvar  =  Pvar . mk  ( Mangled . from_string  fld_name )  curr_pname  in 
 
			
		
	
		
		
			
				
					
					                let  typestate'  = 
                let  typestate'  = 
 
			
		
	
		
		
			
				
					
					                  add_field_to_typestate_if_absent  tenv  loc  typestate  pvar  inner_origin  fn  typ 
                  add_field_to_typestate_if_absent  tenv  loc  typestate  pvar  inner_origin  fn 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					                    ~ field_class_typ  ~ class_under_analysis 
 
			
		
	
		
		
			
				
					
					                in 
                in 
 
			
		
	
		
		
			
				
					
					                ( Exp . Lvar  pvar ,  typestate' ) 
                ( Exp . Lvar  pvar ,  typestate' ) 
 
			
		
	
		
		
			
				
					
					            |  Exp . Lvar  _  |  Exp . Lfield  _  ->  ( 
            |  Exp . Lvar  _  |  Exp . Lfield  _  ->  ( 
 
			
		
	
	
		
		
			
				
					
						
						
						
							
								 
						
					 
					@ -353,7 +367,8 @@ let convert_complex_exp_to_pvar_and_register_field_in_typestate tenv idenv curr_
 
			
		
	
		
		
			
				
					
					              |  Some  exp_str  -> 
              |  Some  exp_str  -> 
 
			
		
	
		
		
			
				
					
					                  let  pvar  =  Pvar . mk  ( Mangled . from_string  exp_str )  curr_pname  in 
                  let  pvar  =  Pvar . mk  ( Mangled . from_string  exp_str )  curr_pname  in 
 
			
		
	
		
		
			
				
					
					                  let  typestate'  = 
                  let  typestate'  = 
 
			
		
	
		
		
			
				
					
					                    add_field_to_typestate_if_absent  tenv  loc  typestate  pvar  inner_origin  fn  typ 
                    add_field_to_typestate_if_absent  tenv  loc  typestate  pvar  inner_origin  fn 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					                      ~ field_class_typ  ~ class_under_analysis 
 
			
		
	
		
		
			
				
					
					                  in 
                  in 
 
			
		
	
		
		
			
				
					
					                  ( Exp . Lvar  pvar ,  typestate' ) 
                  ( Exp . Lvar  pvar ,  typestate' ) 
 
			
		
	
		
		
			
				
					
					              |  None  -> 
              |  None  -> 
 
			
		
	
	
		
		
			
				
					
						
							
								 
						
						
							
								 
						
						
					 
					@ -1232,12 +1247,19 @@ let typecheck_instr ({IntraproceduralAnalysis.proc_desc= curr_pdesc; tenv; _} as
 
			
		
	
		
		
			
				
					
					      let  check_field_assign  ()  = 
      let  check_field_assign  ()  = 
 
			
		
	
		
		
			
				
					
					        match  e1  with 
        match  e1  with 
 
			
		
	
		
		
			
				
					
					        |  Exp . Lfield  ( _ ,  field_name ,  field_class_type )  ->  ( 
        |  Exp . Lfield  ( _ ,  field_name ,  field_class_type )  ->  ( 
 
			
		
	
		
		
			
				
					
					          match  AnnotatedField . get  tenv  field_name  field_class_type  with 
            let  class_under_analysis  = 
 
			
				
				
			
		
	
		
		
	
		
		
			
				
					
					              Procname . Java . get_class_type_name 
 
			
		
	
		
		
			
				
					
					                ( Procname . as_java_exn  curr_pname 
 
			
		
	
		
		
			
				
					
					                   ~ explanation : " Attempt to typecheck non-Java method " ) 
 
			
		
	
		
		
			
				
					
					            in 
 
			
		
	
		
		
			
				
					
					            match 
 
			
		
	
		
		
			
				
					
					              AnnotatedField . get  tenv  field_name  ~ class_typ : field_class_type  ~ class_under_analysis 
 
			
		
	
		
		
			
				
					
					            with 
 
			
		
	
		
		
			
				
					
					            |  Some  annotated_field  -> 
            |  Some  annotated_field  -> 
 
			
		
	
		
		
			
				
					
					                if  checks . eradicate  then 
                if  checks . eradicate  then 
 
			
		
	
		
		
			
				
					
					                  EradicateChecks . check_field_assignment  analysis_data  ~ nullsafe_mode 
                  EradicateChecks . check_field_assignment  analysis_data  ~ nullsafe_mode 
 
			
		
	
		
		
			
				
					
					                  find_canonical_duplicate  node  instr_ref  typestate  ~ expr_rhs : e2  ~ field_type : typ  loc 
                     find_canonical_duplicate  node  instr_ref  typestate  ~ expr_rhs : e2  ~ field_type : typ 
 
			
				
				
			
		
	
		
		
			
				
					
					                  field_name  annotated_field 
                    loc   field_name  annotated_field 
 
			
				
				
			
		
	
		
		
	
		
		
	
		
		
			
				
					
					                    ( typecheck_expr  analysis_data  ~ nullsafe_mode  find_canonical_duplicate  calls_this 
                    ( typecheck_expr  analysis_data  ~ nullsafe_mode  find_canonical_duplicate  calls_this 
 
			
		
	
		
		
			
				
					
					                       checks ) 
                       checks ) 
 
			
		
	
		
		
			
				
					
					            |  None  -> 
            |  None  ->