pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

[infer] Get rid of verbose Typ.mk Tvoid

Browse Source 
Summary: Instead use `Typ.void` which does the same thing

Reviewed By: ngorogiannis

Differential Revision: D19640598

fbshipit-source-id: 01ff1f6a0
master
Ezgi Çiçek 5 years ago committed by Facebook Github Bot
parent 17c5f5c424
commit 43a99745b6
23 changed files with 63 additions and 75 deletions
Show Stats Download Patch File Download Diff File

2
infer/src/IR/HilInstr.ml
Unescape View File

@ -85,7 +85,7 @@ let of_sil ~include_array_indexes ~f_resolve_id (instr : Sil.instr) =
| Call ((ret_id, ret_typ), call_exp, formals, loc, call_flags) -> | Call ((ret_id, ret_typ), call_exp, formals, loc, call_flags) ->
let hil_ret = (Var.of_id ret_id, ret_typ) in let hil_ret = (Var.of_id ret_id, ret_typ) in
let hil_call = let hil_call =
match exp_of_sil call_exp (Typ.mk Tvoid) with match exp_of_sil call_exp Typ.void with
| Constant (Cfun procname) | Closure (procname, _) -> | Constant (Cfun procname) | Closure (procname, _) ->
Direct procname Direct procname
| HilExp.AccessExpression access_expr -> | HilExp.AccessExpression access_expr ->

2
infer/src/IR/ProcAttributes.ml
Unescape View File

@ -89,7 +89,7 @@ let default translation_unit proc_name =
; method_annotation= Annot.Method.empty ; method_annotation= Annot.Method.empty
; objc_accessor= None ; objc_accessor= None
; proc_name ; proc_name
; ret_type= Typ.mk Typ.Tvoid } ; ret_type= Typ.void }
let pp_parameters = let pp_parameters =

2
infer/src/absint/LowerHil.ml
Unescape View File

@ -49,7 +49,7 @@ module Make (TransferFunctions : TransferFunctions.HIL) (HilConfig : HilConfig)
"dump" all of the temporaries out of the id map, then execute the unlock instruction. *) "dump" all of the temporaries out of the id map, then execute the unlock instruction. *)
let actual_state' = let actual_state' =
Bindings.fold bindings ~init:actual_state ~f:(fun id access_expr astate_acc -> Bindings.fold bindings ~init:actual_state ~f:(fun id access_expr astate_acc ->
let lhs_access_path = HilExp.AccessExpression.base (id, Typ.mk Typ.Tvoid) in let lhs_access_path = HilExp.AccessExpression.base (id, Typ.void) in
let dummy_assign = let dummy_assign =
HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc) HilInstr.Assign (lhs_access_path, HilExp.AccessExpression access_expr, loc)
in in

6
infer/src/biabduction/Absarray.ml
Unescape View File

@ -602,7 +602,7 @@ let check_after_array_abstraction tenv prop =
() ()
| Predicates.Earray (_, esel, _) -> | Predicates.Earray (_, esel, _) ->
(* check that no more than 2 elements are in the array *) (* check that no more than 2 elements are in the array *)
let typ_elem = Typ.array_elem (Some (Typ.mk Tvoid)) typ in let typ_elem = Typ.array_elem (Some Typ.void) typ in
if List.length esel > 2 && array_typ_can_abstract typ then if List.length esel > 2 && array_typ_can_abstract typ then
if List.for_all ~f:(check_index root offs) esel then () else report_error prop if List.for_all ~f:(check_index root offs) esel then () else report_error prop
else else
@ -612,13 +612,13 @@ let check_after_array_abstraction tenv prop =
| Predicates.Estruct (fsel, _) -> | Predicates.Estruct (fsel, _) ->
List.iter List.iter
~f:(fun (f, se) -> ~f:(fun (f, se) ->
let typ_f = Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f typ in let typ_f = Struct.fld_typ ~lookup ~default:Typ.void f typ in
check_se root (offs @ [Predicates.Off_fld (f, typ)]) typ_f se ) check_se root (offs @ [Predicates.Off_fld (f, typ)]) typ_f se )
fsel fsel
in in
let check_hpred = function let check_hpred = function
| Predicates.Hpointsto (root, se, texp) -> | Predicates.Hpointsto (root, se, texp) ->
let typ = Exp.texp_to_typ (Some (Typ.mk Tvoid)) texp in let typ = Exp.texp_to_typ (Some Typ.void) texp in
check_se root [] typ se check_se root [] typ se
| Predicates.Hlseg _ | Predicates.Hdllseg _ -> | Predicates.Hlseg _ | Predicates.Hdllseg _ ->
() ()

2
infer/src/biabduction/Attribute.ml
Unescape View File

@ -364,7 +364,7 @@ let find_equal_formal_path tenv e prop =
| Predicates.Eexp (exp2, _) when Exp.equal exp2 e -> ( | Predicates.Eexp (exp2, _) when Exp.equal exp2 e -> (
match find_in_sigma exp1 seen_hpreds with match find_in_sigma exp1 seen_hpreds with
| Some vfs -> | Some vfs ->
Some (Exp.Lfield (vfs, field, Typ.mk Tvoid)) Some (Exp.Lfield (vfs, field, Typ.void))
| None -> | None ->
None ) None )
| _ -> | _ ->

18
infer/src/biabduction/BuiltinDefn.ml
Unescape View File

@ -624,8 +624,8 @@ let execute___cxx_typeid ({Builtin.summary; tenv; prop_; args; loc; exe_env} as
let set_instr = let set_instr =
Sil.Store Sil.Store
{ e1= field_exp { e1= field_exp
; root_typ= Typ.mk Tvoid ; root_typ= Typ.void
; typ= Typ.mk Tvoid ; typ= Typ.void
; e2= Exp.Const (Const.Cstr typ_string) ; e2= Exp.Const (Const.Cstr typ_string)
; loc } ; loc }
in in
@ -766,8 +766,8 @@ let execute___infer_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_env
let set_instr = let set_instr =
Sil.Store Sil.Store
{ e1= Exp.Lvar Predicates.custom_error { e1= Exp.Lvar Predicates.custom_error
; root_typ= Typ.mk Tvoid ; root_typ= Typ.void
; typ= Typ.mk Tvoid ; typ= Typ.void
; e2= Exp.Const (Const.Cstr error_str) ; e2= Exp.Const (Const.Cstr error_str)
; loc } ; loc }
in in
@ -787,8 +787,8 @@ let execute___assert_fail {Builtin.summary; tenv; prop_; path; args; loc; exe_en
let set_instr = let set_instr =
Sil.Store Sil.Store
{ e1= Exp.Lvar Predicates.custom_error { e1= Exp.Lvar Predicates.custom_error
; root_typ= Typ.mk Tvoid ; root_typ= Typ.void
; typ= Typ.mk Tvoid ; typ= Typ.void
; e2= Exp.Const (Const.Cstr error_str) ; e2= Exp.Const (Const.Cstr error_str)
; loc } ; loc }
in in
@ -801,11 +801,7 @@ let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt
let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in let ptr_typ = Typ.mk (Tptr (typ, Typ.Pk_pointer)) in
let sizeof_typ = Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in let sizeof_typ = Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} in
let alloc_fun_exp = let alloc_fun_exp =
match alloc_fun_opt with match alloc_fun_opt with Some pname -> [(Exp.Const (Const.Cfun pname), Typ.void)] | None -> []
| Some pname ->
[(Exp.Const (Const.Cfun pname), Typ.mk Tvoid)]
| None ->
[]
in in
let alloc_instr = let alloc_instr =
Sil.Call (ret_id_typ, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) Sil.Call (ret_id_typ, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default)

12
infer/src/biabduction/Prover.ml
Unescape View File

@ -1540,7 +1540,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 :
| (f1, se1) :: fsel1', (f2, se2) :: fsel2' -> ( | (f1, se1) :: fsel1', (f2, se2) :: fsel2' -> (
match Fieldname.compare f1 f2 with match Fieldname.compare f1 f2 with
| 0 -> | 0 ->
let typ' = Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in let typ' = Struct.fld_typ ~lookup ~default:Typ.void f2 typ2 in
let subs', se_frame, se_missing = let subs', se_frame, se_missing =
sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ' sexp_imply tenv (Exp.Lfield (source, f2, typ2)) false calc_missing subs se1 se2 typ'
in in
@ -1560,7 +1560,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 :
in in
(subs', (f1, se1) :: fld_frame, fld_missing) (subs', (f1, se1) :: fld_frame, fld_missing)
| _ -> | _ ->
let typ' = Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in let typ' = Struct.fld_typ ~lookup ~default:Typ.void f2 typ2 in
let subs' = let subs' =
sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ'
in in
@ -1570,7 +1570,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 :
let fld_missing' = (f2, se2) :: fld_missing in let fld_missing' = (f2, se2) :: fld_missing in
(subs', fld_frame, fld_missing') ) (subs', fld_frame, fld_missing') )
| [], (f2, se2) :: fsel2' -> | [], (f2, se2) :: fsel2' ->
let typ' = Struct.fld_typ ~lookup ~default:(Typ.mk Tvoid) f2 typ2 in let typ' = Struct.fld_typ ~lookup ~default:Typ.void f2 typ2 in
let subs' = let subs' =
sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ' sexp_imply_nolhs tenv (Exp.Lfield (source, f2, typ2)) calc_missing subs se2 typ'
in in
@ -1582,7 +1582,7 @@ and struct_imply tenv source calc_missing subs fsel1 fsel2 typ2 :
and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2 : and array_imply tenv source calc_index_frame calc_missing subs esel1 esel2 typ2 :
subst2 * (Exp.t * Predicates.strexp) list * (Exp.t * Predicates.strexp) list = subst2 * (Exp.t * Predicates.strexp) list * (Exp.t * Predicates.strexp) list =
let typ_elem = Typ.array_elem (Some (Typ.mk Tvoid)) typ2 in let typ_elem = Typ.array_elem (Some Typ.void) typ2 in
match (esel1, esel2) with match (esel1, esel2) with
| _, [] -> | _, [] ->
(subs, esel1, []) (subs, esel1, [])
@ -2048,7 +2048,7 @@ let rec hpred_imply tenv calc_index_frame calc_missing subs prop1 sigma2 hpred2
match Prop.prop_iter_current tenv iter1' with match Prop.prop_iter_current tenv iter1' with
| Predicates.Hpointsto (e1, se1, texp1), _ -> ( | Predicates.Hpointsto (e1, se1, texp1), _ -> (
try try
let typ2 = Exp.texp_to_typ (Some (Typ.mk Tvoid)) texp2 in let typ2 = Exp.texp_to_typ (Some Typ.void) texp2 in
let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in let typing_frame, typing_missing = texp_imply tenv subs texp1 texp2 e1 calc_missing in
let se1' = sexp_imply_preprocess se1 texp1 se2 in let se1' = sexp_imply_preprocess se1 texp1 se2 in
let subs', fld_frame, fld_missing = let subs', fld_frame, fld_missing =
@ -2371,7 +2371,7 @@ and sigma_imply tenv calc_index_frame calc_missing subs prop1 sigma2 : subst2 *
let subs' = let subs' =
match hpred2' with match hpred2' with
| Predicates.Hpointsto (e2, se2, te2) -> | Predicates.Hpointsto (e2, se2, te2) ->
let typ2 = Exp.texp_to_typ (Some (Typ.mk Tvoid)) te2 in let typ2 = Exp.texp_to_typ (Some Typ.void) te2 in
sexp_imply_nolhs tenv e2 calc_missing subs se2 typ2 sexp_imply_nolhs tenv e2 calc_missing subs se2 typ2
| _ -> | _ ->
subs subs

2
infer/src/biabduction/Rearrange.ml
Unescape View File

@ -422,7 +422,7 @@ let strexp_extend_values pname tenv orig_prop footprint_part kind max_stamp se t
| Exp.Sizeof sizeof_data -> | Exp.Sizeof sizeof_data ->
sizeof_data sizeof_data
| _ -> | _ ->
{Exp.typ= Typ.mk Typ.Tvoid; nbytes= None; dynamic_length= None; subtype= Subtype.exact} {Exp.typ= Typ.void; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
in in
List.map List.map
~f:(fun (atoms', se', typ') -> ~f:(fun (atoms', se', typ') ->

2
infer/src/biabduction/SymExec.ml
Unescape View File

@ -1831,7 +1831,7 @@ and sym_exec_objc_accessor callee_pname property_accesor ret_typ tenv ret_id pde
and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop path : and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ summary loc prop path :
Builtin.ret_typ = Builtin.ret_typ =
let alloc_source_function_arg = (Exp.Const (Const.Cfun pname), Typ.mk Tvoid) in let alloc_source_function_arg = (Exp.Const (Const.Cfun pname), Typ.void) in
let args = let args =
let sizeof_exp = let sizeof_exp =
Exp.Sizeof {typ= ret_typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact} Exp.Sizeof {typ= ret_typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact}

2
infer/src/clang/cField_decl.ml
Unescape View File

@ -115,7 +115,7 @@ let add_missing_fields tenv class_name missing_fields =
let modelled_fields_in_classes = let modelled_fields_in_classes =
[ ("NSData", "_bytes", Typ.mk (Tptr (Typ.mk Tvoid, Typ.Pk_pointer))) [ ("NSData", "_bytes", Typ.mk (Tptr (Typ.void, Typ.Pk_pointer)))
; ("NSArray", "elementData", Typ.mk (Tint Typ.IInt)) ] ; ("NSArray", "elementData", Typ.mk (Tint Typ.IInt)) ]

2
infer/src/clang/cMethod_trans.ml
Unescape View File

@ -278,7 +278,7 @@ let create_external_procdesc trans_unit_ctx cfg proc_name clang_method_kind type
| Some (ret_type, arg_types) -> | Some (ret_type, arg_types) ->
(ret_type, List.map ~f:(fun typ -> (Mangled.from_string "x", typ)) arg_types) (ret_type, List.map ~f:(fun typ -> (Mangled.from_string "x", typ)) arg_types)
| None -> | None ->
(Typ.mk Typ.Tvoid, []) (Typ.void, [])
in in
let proc_attributes = let proc_attributes =
{ (ProcAttributes.default trans_unit_ctx.CFrontend_config.source_file proc_name) with { (ProcAttributes.default trans_unit_ctx.CFrontend_config.source_file proc_name) with

20
infer/src/clang/cTrans.ml
Unescape View File

@ -1189,7 +1189,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
decl_ref_trans ~context:(MemberOrIvar this_res_trans) trans_state si decl_ref decl_ref_trans ~context:(MemberOrIvar this_res_trans) trans_state si decl_ref
in in
let res_trans = let res_trans =
cxx_method_construct_call_trans trans_state_pri res_trans_callee params_stmt si (Typ.mk Tvoid) cxx_method_construct_call_trans trans_state_pri res_trans_callee params_stmt si Typ.void
~is_injected_destructor:false ~is_cpp_call_virtual:false (Some tmp_res_trans) ~is_injected_destructor:false ~is_cpp_call_virtual:false (Some tmp_res_trans)
~is_inherited_ctor ~is_inherited_ctor
in in
@ -1212,7 +1212,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
| Some res_trans_callee when Option.is_some res_trans_callee.method_name -> | Some res_trans_callee when Option.is_some res_trans_callee.method_name ->
let is_cpp_call_virtual = res_trans_callee.is_cpp_call_virtual in let is_cpp_call_virtual = res_trans_callee.is_cpp_call_virtual in
Some Some
(cxx_method_construct_call_trans trans_state_pri res_trans_callee [] si' (Typ.mk Tvoid) (cxx_method_construct_call_trans trans_state_pri res_trans_callee [] si' Typ.void
~is_injected_destructor ~is_cpp_call_virtual None ~is_inherited_ctor:false) ~is_injected_destructor ~is_cpp_call_virtual None ~is_inherited_ctor:false)
| _ -> | _ ->
None None
@ -3054,7 +3054,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let stmt = match stmts with [stmt] -> stmt | _ -> assert false in let stmt = match stmts with [stmt] -> stmt | _ -> assert false in
let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in let res_trans_stmt = exec_with_glvalue_as_reference instruction trans_state' stmt in
let exp = res_trans_stmt.return in let exp = res_trans_stmt.return in
let args = [exp; (sizeof_expr, Typ.mk Tvoid)] in let args = [exp; (sizeof_expr, Typ.void)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call = Sil.Call ((ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in let call = Sil.Call ((ret_id, cast_type), builtin, args, sil_loc, CallFlags.default) in
let res_ex = Exp.Var ret_id in let res_ex = Exp.Var ret_id in
@ -3097,22 +3097,22 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
and gccAsmStmt_trans trans_state stmt_info stmts = and gccAsmStmt_trans trans_state stmt_info stmts =
call_function_with_args Procdesc.Node.GCCAsmStmt BuiltinDecl.__infer_skip_gcc_asm_stmt call_function_with_args Procdesc.Node.GCCAsmStmt BuiltinDecl.__infer_skip_gcc_asm_stmt
trans_state stmt_info (Typ.mk Tvoid) stmts trans_state stmt_info Typ.void stmts
and genericSelectionExprUnknown_trans trans_state stmt_info stmts = and genericSelectionExprUnknown_trans trans_state stmt_info stmts =
call_function_with_args Procdesc.Node.GenericSelectionExpr call_function_with_args Procdesc.Node.GenericSelectionExpr
BuiltinDecl.__infer_generic_selection_expr trans_state stmt_info (Typ.mk Tvoid) stmts BuiltinDecl.__infer_generic_selection_expr trans_state stmt_info Typ.void stmts
and objc_cxx_throw_trans trans_state stmt_info stmts = and objc_cxx_throw_trans trans_state stmt_info stmts =
call_function_with_args Procdesc.Node.ObjCCPPThrow BuiltinDecl.objc_cpp_throw trans_state call_function_with_args Procdesc.Node.ObjCCPPThrow BuiltinDecl.objc_cpp_throw trans_state
stmt_info (Typ.mk Tvoid) stmts stmt_info Typ.void stmts
and cxxPseudoDestructorExpr_trans () = and cxxPseudoDestructorExpr_trans () =
mk_trans_result mk_trans_result
(Exp.Const (Const.Cfun BuiltinDecl.__infer_skip_function), Typ.mk Tvoid) (Exp.Const (Const.Cfun BuiltinDecl.__infer_skip_function), Typ.void)
empty_control empty_control
@ -3135,7 +3135,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
let fun_name = BuiltinDecl.__cxx_typeid in let fun_name = BuiltinDecl.__cxx_typeid in
let sil_fun = Exp.Const (Const.Cfun fun_name) in let sil_fun = Exp.Const (Const.Cfun fun_name) in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let void_typ = Typ.mk Tvoid in let void_typ = Typ.void in
let type_info_objc = let type_info_objc =
(Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact}, void_typ) (Exp.Sizeof {typ; nbytes= None; dynamic_length= None; subtype= Subtype.exact}, void_typ)
in in
@ -3582,7 +3582,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
| None -> | None ->
genericSelectionExprUnknown_trans trans_state stmt_info stmts ) genericSelectionExprUnknown_trans trans_state stmt_info stmts )
| SizeOfPackExpr _ -> | SizeOfPackExpr _ ->
mk_trans_result (Exp.get_undefined false, Typ.mk Tvoid) empty_control mk_trans_result (Exp.get_undefined false, Typ.void) empty_control
| GCCAsmStmt (stmt_info, stmts) -> | GCCAsmStmt (stmt_info, stmts) ->
gccAsmStmt_trans trans_state stmt_info stmts gccAsmStmt_trans trans_state stmt_info stmts
| CXXPseudoDestructorExpr _ -> | CXXPseudoDestructorExpr _ ->
@ -3727,7 +3727,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s
((stmt_info, stmts), ret_typ) ((stmt_info, stmts), ret_typ)
| None -> | None ->
let stmt_tuple = Clang_ast_proj.get_stmt_tuple instr in let stmt_tuple = Clang_ast_proj.get_stmt_tuple instr in
(stmt_tuple, Typ.mk Tvoid) (stmt_tuple, Typ.void)
in in
skip_unimplemented skip_unimplemented
~reason: ~reason:

12
infer/src/clang/cTrans_utils.ml
Unescape View File

@ -382,7 +382,7 @@ let create_call_to_free_cf sil_loc exp typ =
let pname = BuiltinDecl.__free_cf in let pname = BuiltinDecl.__free_cf in
let stmt_call = let stmt_call =
Sil.Call Sil.Call
( (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) ( (Ident.create_fresh Ident.knormal, Typ.void)
, Exp.Const (Const.Cfun pname) , Exp.Const (Const.Cfun pname)
, [(exp, typ)] , [(exp, typ)]
, sil_loc , sil_loc
@ -456,9 +456,9 @@ let cast_operation cast_kind ((exp, typ) as exp_typ) cast_typ sil_loc =
let trans_assertion_failure sil_loc (context : CContext.t) = let trans_assertion_failure sil_loc (context : CContext.t) =
let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in let assert_fail_builtin = Exp.Const (Const.Cfun BuiltinDecl.__infer_fail) in
let args = [(Exp.Const (Const.Cstr Config.default_failure_name), Typ.mk Tvoid)] in let args = [(Exp.Const (Const.Cstr Config.default_failure_name), Typ.void)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let ret_typ = Typ.mk Tvoid in let ret_typ = Typ.void in
let call_instr = let call_instr =
Sil.Call ((ret_id, ret_typ), assert_fail_builtin, args, sil_loc, CallFlags.default) Sil.Call ((ret_id, ret_typ), assert_fail_builtin, args, sil_loc, CallFlags.default)
in in
@ -606,12 +606,12 @@ let is_logical_negation_of_int tenv ei uoi =
false false
let mk_fresh_void_exp_typ () = (Exp.Var (Ident.create_fresh Ident.knormal), Typ.mk Tvoid) let mk_fresh_void_exp_typ () = (Exp.Var (Ident.create_fresh Ident.knormal), Typ.void)
let mk_fresh_void_id_typ () = (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) let mk_fresh_void_id_typ () = (Ident.create_fresh Ident.knormal, Typ.void)
let mk_fresh_void_return () = let mk_fresh_void_return () =
let id = Ident.create_fresh Ident.knormal and void = Typ.mk Tvoid in let id = Ident.create_fresh Ident.knormal and void = Typ.void in
((id, void), (Exp.Var id, void)) ((id, void), (Exp.Var id, void))

20
infer/src/java/jTrans.ml
Unescape View File

@ -119,7 +119,7 @@ let translate_locals program tenv formals bytecode jbir_code =
Array.fold Array.fold
~f:(fun accu jbir_var -> ~f:(fun accu jbir_var ->
let var = Mangled.from_string (JBir.var_name_g jbir_var) in let var = Mangled.from_string (JBir.var_name_g jbir_var) in
collect accu (var, Typ.mk Tvoid) ) collect accu (var, Typ.void) )
~init:with_bytecode_vars (JBir.vars jbir_code) ~init:with_bytecode_vars (JBir.vars jbir_code)
in in
snd with_jbir_vars snd with_jbir_vars
@ -494,7 +494,7 @@ let rec expression (context : JContext.t) pc expr =
| _ -> | _ ->
assert false assert false
in in
let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.mk Tvoid)] in let args = [(sil_ex, type_of_ex); (sizeof_expr, Typ.void)] in
let ret_id = Ident.create_fresh Ident.knormal in let ret_id = Ident.create_fresh Ident.knormal in
let call = let call =
Sil.Call ((ret_id, Typ.mk (Tint IBool)), builtin, args, loc, CallFlags.default) Sil.Call ((ret_id, Typ.mk (Tint IBool)), builtin, args, loc, CallFlags.default)
@ -631,7 +631,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let return_type = let return_type =
match JBasics.ms_rtype ms with match JBasics.ms_rtype ms with
| None -> | None ->
Typ.mk Tvoid Typ.void
| Some vt -> | Some vt ->
JTransType.value_type program tenv vt JTransType.value_type program tenv vt
in in
@ -648,11 +648,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
| None -> | None ->
let call_instr = let call_instr =
Sil.Call Sil.Call
( (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) ((Ident.create_fresh Ident.knormal, Typ.void), callee_fun, call_args, loc, call_flags)
, callee_fun
, call_args
, loc
, call_flags )
in in
instrs @ [call_instr] instrs @ [call_instr]
| Some var -> | Some var ->
@ -690,7 +686,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let set_file_attr = let set_file_attr =
let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_file_attribute) in let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_file_attribute) in
Sil.Call Sil.Call
( (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) ( (Ident.create_fresh Ident.knormal, Typ.void)
, set_builtin , set_builtin
, [exp] , [exp]
, loc , loc
@ -703,7 +699,7 @@ let method_invocation (context : JContext.t) loc pc var_opt cn ms sil_obj_opt ex
let set_mem_attr = let set_mem_attr =
let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_mem_attribute) in let set_builtin = Exp.Const (Const.Cfun BuiltinDecl.__set_mem_attribute) in
Sil.Call Sil.Call
( (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) ( (Ident.create_fresh Ident.knormal, Typ.void)
, set_builtin , set_builtin
, [exp] , [exp]
, loc , loc
@ -773,7 +769,7 @@ let assume_not_null loc sil_expr =
let not_null_expr = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in let not_null_expr = Exp.BinOp (Binop.Ne, sil_expr, Exp.null) in
let call_args = [(not_null_expr, Typ.mk (Tint Typ.IBool))] in let call_args = [(not_null_expr, Typ.mk (Tint Typ.IBool))] in
Sil.Call Sil.Call
( (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) ( (Ident.create_fresh Ident.knormal, Typ.void)
, builtin_infer_assume , builtin_infer_assume
, call_args , call_args
, loc , loc
@ -797,7 +793,7 @@ let instruction (context : JContext.t) pc instr : translation =
let builtin_const = Exp.Const (Const.Cfun builtin) in let builtin_const = Exp.Const (Const.Cfun builtin) in
let instr = let instr =
Sil.Call Sil.Call
( (Ident.create_fresh Ident.knormal, Typ.mk Tvoid) ( (Ident.create_fresh Ident.knormal, Typ.void)
, builtin_const , builtin_const
, [(sil_expr, sil_type)] , [(sil_expr, sil_type)]
, loc , loc

2
infer/src/java/jTransExn.ml
Unescape View File

@ -84,7 +84,7 @@ let translate_exceptions (context : JContext.t) exit_nodes get_body_nodes handle
[ (Exp.Var id_exn_val, Typ.mk (Tptr (exn_type, Typ.Pk_pointer))) [ (Exp.Var id_exn_val, Typ.mk (Tptr (exn_type, Typ.Pk_pointer)))
; ( Exp.Sizeof ; ( Exp.Sizeof
{typ= exn_type; nbytes= None; dynamic_length= None; subtype= Subtype.exact} {typ= exn_type; nbytes= None; dynamic_length= None; subtype= Subtype.exact}
, Typ.mk Tvoid ) ] , Typ.void ) ]
in in
Sil.Call Sil.Call
( (id_instanceof, Typ.mk (Tint IBool)) ( (id_instanceof, Typ.mk (Tint IBool))

2
infer/src/java/jTransType.ml
Unescape View File

@ -471,4 +471,4 @@ let rec expr_type (context : JContext.t) expr =
(** Returns the return type of the method based on the return type specified in ms. *) (** Returns the return type of the method based on the return type specified in ms. *)
let return_type program tenv ms = let return_type program tenv ms =
match JBasics.ms_rtype ms with None -> Typ.mk Tvoid | Some vt -> value_type program tenv vt match JBasics.ms_rtype ms with None -> Typ.void | Some vt -> value_type program tenv vt

12
infer/src/nullsafe/typeCheck.ml
Unescape View File

@ -434,7 +434,7 @@ let typecheck_expr_for_errors ~is_strict_mode find_canonical_duplicate curr_pdes
tenv node instr_ref typestate1 exp1 loc1 : unit = tenv node instr_ref typestate1 exp1 loc1 : unit =
ignore ignore
(typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this checks (typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv node instr_ref typestate1 exp1 (Typ.mk Tvoid) TypeOrigin.Undef loc1) tenv node instr_ref typestate1 exp1 Typ.void TypeOrigin.Undef loc1)
(* Handle Preconditions.checkNotNull. *) (* Handle Preconditions.checkNotNull. *)
@ -701,8 +701,8 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
let e1 = Exp.Lvar pvar in let e1 = Exp.Lvar pvar in
let typ, ta = let typ, ta =
typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this
checks tenv original_node instr_ref typestate e1 (Typ.mk Tvoid) checks tenv original_node instr_ref typestate e1 Typ.void TypeOrigin.OptimisticFallback
TypeOrigin.OptimisticFallback loc loc
in in
let range = (typ, ta) in let range = (typ, ta) in
let typestate1 = TypeState.add pvar range typestate in let typestate1 = TypeState.add pvar range typestate in
@ -749,8 +749,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
in in
let typ, inferred_nullability = let typ, inferred_nullability =
typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this checks typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv original_node instr_ref typestate2 e' (Typ.mk Tvoid) TypeOrigin.OptimisticFallback tenv original_node instr_ref typestate2 e' Typ.void TypeOrigin.OptimisticFallback loc
loc
in in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node e' typ EradicateChecks.check_zero tenv find_canonical_duplicate curr_pdesc node e' typ
@ -786,8 +785,7 @@ let rec check_condition_for_sil_prune tenv idenv calls_this find_canonical_dupli
in in
let typ, inferred_nullability = let typ, inferred_nullability =
typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this checks typecheck_expr_simple ~is_strict_mode find_canonical_duplicate curr_pdesc calls_this checks
tenv original_node instr_ref typestate2 e' (Typ.mk Tvoid) TypeOrigin.OptimisticFallback tenv original_node instr_ref typestate2 e' Typ.void TypeOrigin.OptimisticFallback loc
loc
in in
if checks.eradicate then if checks.eradicate then
EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc original_node e' typ EradicateChecks.check_nonzero tenv find_canonical_duplicate curr_pdesc original_node e' typ

4
infer/src/unit/TaintTests.ml
Unescape View File

@ -108,10 +108,10 @@ let tests =
let call_sink actual_str = call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in let call_sink actual_str = call_sink_with_exp (Exp.Var (ident_of_str actual_str)) in
let assign_id_to_field root_str fld_str rhs_id_str = let assign_id_to_field root_str fld_str rhs_id_str =
let rhs_exp = Exp.Var (ident_of_str rhs_id_str) in let rhs_exp = Exp.Var (ident_of_str rhs_id_str) in
make_store ~rhs_typ:(Typ.mk Tvoid) (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp make_store ~rhs_typ:Typ.void (Exp.Var (ident_of_str root_str)) fld_str ~rhs_exp
in in
let read_field_to_id lhs_id_str root_str fld_str = let read_field_to_id lhs_id_str root_str fld_str =
make_load_fld ~rhs_typ:(Typ.mk Tvoid) lhs_id_str fld_str (Exp.Var (ident_of_str root_str)) make_load_fld ~rhs_typ:Typ.void lhs_id_str fld_str (Exp.Var (ident_of_str root_str))
in in
let assert_empty = invariant "{ }" in let assert_empty = invariant "{ }" in
let exe_env = Exe_env.mk () in let exe_env = Exe_env.mk () in

4
infer/src/unit/TraceTests.ml
Unescape View File

@ -116,9 +116,7 @@ let tests =
let append = let append =
let append_ _ = let append_ _ =
let call_site = CallSite.dummy in let call_site = CallSite.dummy in
let footprint_ap = let footprint_ap = AccessPath.Abs.Exact (AccessPath.of_id (Ident.create_none ()) Typ.void) in
AccessPath.Abs.Exact (AccessPath.of_id (Ident.create_none ()) (Typ.mk Tvoid))
in
let source_trace = MockTrace.of_source source1 in let source_trace = MockTrace.of_source source1 in
let footprint_trace = MockTrace.of_footprint footprint_ap |> MockTrace.add_sink sink1 in let footprint_trace = MockTrace.of_footprint footprint_ap |> MockTrace.add_sink sink1 in
let expected_trace = MockTrace.of_source source1 |> MockTrace.add_sink sink1 in let expected_trace = MockTrace.of_source source1 |> MockTrace.add_sink sink1 in

2
infer/src/unit/accessPathTestUtils.ml
Unescape View File

@ -9,7 +9,7 @@ open! IStd
let make_var var_str = Pvar.mk (Mangled.from_string var_str) Procname.empty_block let make_var var_str = Pvar.mk (Mangled.from_string var_str) Procname.empty_block
let make_base ?(typ = Typ.mk Tvoid) base_str = AccessPath.base_of_pvar (make_var base_str) typ let make_base ?(typ = Typ.void) base_str = AccessPath.base_of_pvar (make_var base_str) typ
let make_fieldname field_name = let make_fieldname field_name =
assert (not (String.contains field_name '.')) ; assert (not (String.contains field_name '.')) ;

4
infer/src/unit/accessPathTests.ml
Unescape View File

@ -18,7 +18,7 @@ let tests =
let xFG = make_access_path "x" ["f"; "g"] in let xFG = make_access_path "x" ["f"; "g"] in
let yF = make_access_path "y" ["f"] in let yF = make_access_path "y" ["f"] in
let xArr = let xArr =
let dummy_typ = Typ.mk Tvoid in let dummy_typ = Typ.void in
let dummy_arr_typ = Typ.mk_array dummy_typ in let dummy_arr_typ = Typ.mk_array dummy_typ in
let base = make_base "x" ~typ:dummy_arr_typ in let base = make_base "x" ~typ:dummy_arr_typ in
(base, [make_array_access dummy_typ]) (base, [make_array_access dummy_typ])
@ -67,7 +67,7 @@ let tests =
in in
let of_exp_test = let of_exp_test =
let f_resolve_id _ = None in let f_resolve_id _ = None in
let dummy_typ = Typ.mk Tvoid in let dummy_typ = Typ.void in
let check_make_ap exp expected_ap ~f_resolve_id = let check_make_ap exp expected_ap ~f_resolve_id =
let make_ap exp = let make_ap exp =
match AccessPath.of_lhs_exp ~include_array_indexes:true exp dummy_typ ~f_resolve_id with match AccessPath.of_lhs_exp ~include_array_indexes:true exp dummy_typ ~f_resolve_id with

2
infer/src/unit/accessTreeTests.ml
Unescape View File

@ -62,7 +62,7 @@ let tests =
let z_base = make_base "z" in let z_base = make_base "z" in
let f = make_field_access "f" in let f = make_field_access "f" in
let g = make_field_access "g" in let g = make_field_access "g" in
let array = make_array_access (Typ.mk Tvoid) in let array = make_array_access Typ.void in
let x = AccessPath.Abs.Exact (make_access_path "x" []) in let x = AccessPath.Abs.Exact (make_access_path "x" []) in
let xF = AccessPath.Abs.Exact (make_access_path "x" ["f"]) in let xF = AccessPath.Abs.Exact (make_access_path "x" ["f"]) in
let xG = AccessPath.Abs.Exact (make_access_path "x" ["g"]) in let xG = AccessPath.Abs.Exact (make_access_path "x" ["g"]) in

2
infer/src/unit/analyzerTester.ml
Unescape View File

@ -83,7 +83,7 @@ module StructuredSil = struct
| Some ret_id_typ -> | Some ret_id_typ ->
ret_id_typ ret_id_typ
| None -> | None ->
(Ident.create_fresh Ident.knormal, Typ.mk Tvoid) (Ident.create_fresh Ident.knormal, Typ.void)
in in
let call_exp = Exp.Const (Const.Cfun procname) in let call_exp = Exp.Const (Const.Cfun procname) in
Cmd (Sil.Call (ret_id_typ, call_exp, args, dummy_loc, CallFlags.default)) Cmd (Sil.Call (ret_id_typ, call_exp, args, dummy_loc, CallFlags.default))

Write Preview
Loading…
Cancel
Save