diff --git a/CodeHawk/CHB/bchlib/bCHFloc.ml b/CodeHawk/CHB/bchlib/bCHFloc.ml index 960c2d1d..e7ab60e0 100644 --- a/CodeHawk/CHB/bchlib/bCHFloc.ml +++ b/CodeHawk/CHB/bchlib/bCHFloc.ml @@ -1404,6 +1404,21 @@ object (self) ^ " not yet handled"]) memoff_r) basevar_type_r + else if self#f#env#is_return_value v then + let callsite_r = self#f#env#get_call_site v in + TR.tbind + ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__)) + (fun callsite -> + let loc = ctxt_string_to_location self#fa callsite in + let fndata = functions_data#get_function self#fa in + if fndata#has_regvar_type_annotation loc#i then + fndata#get_regvar_type_annotation loc#i + else + Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": " + ^ "type of callsite return value " ^ (x2s (XVar v)) + ^ " at address " ^ loc#i#to_hex_string + ^ " not yet handled"]) + callsite_r else let ty = self#env#get_variable_type v in match ty with diff --git a/CodeHawk/CHB/bchlib/bCHVersion.ml b/CodeHawk/CHB/bchlib/bCHVersion.ml index d2791984..9f44e67d 100644 --- a/CodeHawk/CHB/bchlib/bCHVersion.ml +++ b/CodeHawk/CHB/bchlib/bCHVersion.ml @@ -95,8 +95,8 @@ end let version = new version_info_t - ~version:"0.6.0_20250313" - ~date:"2025-03-13" + ~version:"0.6.0_20250314" + ~date:"2025-03-14" ~licensee: None ~maxfilesize: None () diff --git a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml index a940b6ff..5a5b1f33 100644 --- a/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml +++ b/CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml @@ -407,7 +407,7 @@ object (self) (* no type information gained *) () - | BranchLink _ + | BranchLink _ | BranchLinkExchange _ when floc#has_call_target && floc#get_call_target#is_signature_valid -> let log_error (msg: string) = mk_tracelog_spec @@ -435,18 +435,33 @@ object (self) (* add constraint for return value *) (if not (is_void rtype) then let typevar = mk_reglhs_typevar rvreg faddr iaddr in - let opttc = mk_btype_constraint typevar rtype in - match opttc with - | Some tc -> - begin - log_type_constraint "BL-rv" tc; - store#add_constraint tc - end + match get_regvar_type_annotation () with + | Some t -> + let opttc = mk_btype_constraint typevar t in + (match opttc with + | Some tc -> + begin + log_type_constraint "BL-rv-intro" tc; + store#add_constraint tc + end + | _ -> + begin + log_no_type_constraint "BL-rv-intro" t; + () + end) | _ -> - begin - log_no_type_constraint "BL-rv" rtype; - () - end); + let opttc = mk_btype_constraint typevar rtype in + match opttc with + | Some tc -> + begin + log_type_constraint "BL-rv" tc; + store#add_constraint tc + end + | _ -> + begin + log_no_type_constraint "BL-rv" rtype; + () + end); (* add constraints for argument values *) List.iter (fun (p, x) ->