123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960openAnnotationstypereturnaddress_kind=|OnStack|OnRegtypef_annot={retaddr_kind:returnaddress_kindoption;stack_allocation_size:Z.toption;stack_size:Z.toption;stack_align:wsizeoption;max_call_depth:Z.toption;stack_zero_strategy:(Stack_zero_strategy.stack_zero_strategy*wsizeoption)option;f_user_annot:annotations;}letf_annot_empty={retaddr_kind=None;stack_allocation_size=None;stack_size=None;stack_align=None;max_call_depth=None;stack_zero_strategy=None;f_user_annot=[];}typearg_ret_info={returned_params:intoptionlist}(** When a non-inlined function returns a `ptr` array, it has to be one of its
arguments. [returned_params] associates to each return value the index of
the corresponding argument if it is a `ptr` array, and [None] otherwise. *)typecall_conv=|Exportofarg_ret_info(** The function should be exported to the outside word *)|Subroutineofarg_ret_info(** internal function that should not be inlined *)|Internal(** internal function that should be inlined *)letis_subroutine=function|Subroutine_->true|_->falseletis_export=function|Export_->true|_->false(* ------------------------------------------------------------------------ *)typereturn_info={ret_annot:Annotations.annotationslist;(* annotation attached to return type *)ret_loc:Location.t;(* location of the return statement *)}(* ------------------------------------------------------------------------ *)typet=Location.t*f_annot*call_conv*return_infoletentry_info(fi:t):IInfo.t=let(fl,_,_,_)=fiin(Location.i_loc0fl,[])letret_info(fi:t):IInfo.t=let(_,_,_,ri)=fiin(Location.i_loc0ri.ret_loc,[])