diff --git a/infer/src/IR/Instrs.ml b/infer/src/IR/Instrs.ml index 652cea65c..4972461b6 100644 --- a/infer/src/IR/Instrs.ml +++ b/infer/src/IR/Instrs.ml @@ -12,7 +12,7 @@ type t = Sil.instr list let empty = [] -let single instr = [instr] +let singleton instr = [instr] let append_list = List.append diff --git a/infer/src/IR/Instrs.mli b/infer/src/IR/Instrs.mli index e2b6b2022..cf0f89870 100644 --- a/infer/src/IR/Instrs.mli +++ b/infer/src/IR/Instrs.mli @@ -11,7 +11,7 @@ type t val empty : t -val single : Sil.instr -> t +val singleton : Sil.instr -> t val append_list : t -> Sil.instr list -> t diff --git a/infer/src/absint/AbstractInterpreter.ml b/infer/src/absint/AbstractInterpreter.ml index 57cb7ee4b..066c75332 100644 --- a/infer/src/absint/AbstractInterpreter.ml +++ b/infer/src/absint/AbstractInterpreter.ml @@ -67,7 +67,7 @@ struct (* hack to ensure that we call `exec_instr` on a node even if it has no instructions *) let instrs = let instrs = CFG.instrs node in - if Instrs.is_empty instrs then Instrs.single Sil.skip_instr else instrs + if Instrs.is_empty instrs then Instrs.singleton Sil.skip_instr else instrs in if debug then NodePrinter.start_session diff --git a/infer/src/absint/ProcCfg.ml b/infer/src/absint/ProcCfg.ml index 7a99d8fea..c64d19913 100644 --- a/infer/src/absint/ProcCfg.ml +++ b/infer/src/absint/ProcCfg.ml @@ -297,7 +297,8 @@ end = struct let instrs (node, index) = let instrs = Base.instrs node in - if Instrs.is_empty instrs then Instrs.empty else Instrs.nth_exn instrs index |> Instrs.single + if Instrs.is_empty instrs then Instrs.empty + else Instrs.nth_exn instrs index |> Instrs.singleton let first_of_node node = (node, 0) diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index c17294e4b..94893be7d 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -20,7 +20,7 @@ let execute___builtin_va_arg {Builtin.pdesc; tenv; prop_; path; args; loc; exe_e match args with | [_; _; (lexp3, typ3)] -> let instr' = Sil.Store (lexp3, typ3, Exp.zero, loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.single instr') [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton instr') [(prop_, path)] | _ -> raise (Exceptions.Wrong_argument_number __POS__) @@ -628,7 +628,7 @@ let execute___cxx_typeid ({Builtin.pdesc; tenv; prop_; args; loc; exe_env} as r) let set_instr = Sil.Store (field_exp, Typ.mk Tvoid, Exp.Const (Const.Cstr typ_string), loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.single set_instr) res + SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton set_instr) res | _ -> res ) | _ -> @@ -758,7 +758,7 @@ let execute___infer_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} let set_instr = Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.single set_instr) [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton set_instr) [(prop_, path)] (* translate builtin assertion failure *) @@ -773,7 +773,7 @@ let execute___assert_fail {Builtin.pdesc; tenv; prop_; path; args; loc; exe_env} let set_instr = Sil.Store (Exp.Lvar Sil.custom_error, Typ.mk Tvoid, Exp.Const (Const.Cstr error_str), loc) in - SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.single set_instr) [(prop_, path)] + SymExec.instrs ~mask_errors:true exe_env tenv pdesc (Instrs.singleton set_instr) [(prop_, path)] let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt @@ -792,7 +792,7 @@ let execute_objc_alloc_no_fail symb_state typ alloc_fun_opt Sil.Call (ret_id_typ, alloc_fun, [(sizeof_typ, ptr_typ)] @ alloc_fun_exp, loc, CallFlags.default) in - SymExec.instrs exe_env tenv pdesc (Instrs.single alloc_instr) symb_state + SymExec.instrs exe_env tenv pdesc (Instrs.singleton alloc_instr) symb_state (* NSArray models *) diff --git a/infer/src/biabduction/SymExec.ml b/infer/src/biabduction/SymExec.ml index 88e3355a9..8445e3516 100644 --- a/infer/src/biabduction/SymExec.ml +++ b/infer/src/biabduction/SymExec.ml @@ -1623,7 +1623,7 @@ and check_variadic_sentinel ?(fails_on_nil= false) n_formals (sentinel, null_pos (* simulate a Load for [lexp] *) let tmp_id_deref = Ident.create_fresh Ident.kprimed in let load_instr = Sil.Load (tmp_id_deref, lexp, typ, loc) in - try instrs exe_env tenv pdesc (Instrs.single load_instr) result + try instrs exe_env tenv pdesc (Instrs.singleton load_instr) result with e when SymOp.exn_not_failure e -> IExn.reraise_if e ~f:(fun () -> fails_on_nil) ; let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in @@ -1722,7 +1722,7 @@ and sym_exec_alloc_model exe_env pname ret_typ tenv ret_id_typ pdesc loc prop pa let alloc_fun = Exp.Const (Const.Cfun BuiltinDecl.malloc_no_fail) in let alloc_instr = Sil.Call (ret_id_typ, alloc_fun, args, loc, CallFlags.default) in L.d_strln "No spec found, method should be model as alloc, executing alloc... " ; - instrs exe_env tenv pdesc (Instrs.single alloc_instr) [(prop, path)] + instrs exe_env tenv pdesc (Instrs.singleton alloc_instr) [(prop, path)] (** Perform symbolic execution for a function call *) diff --git a/infer/src/unit/procCfgTests.ml b/infer/src/unit/procCfgTests.ml index c5dde4cc2..31343434f 100644 --- a/infer/src/unit/procCfgTests.ml +++ b/infer/src/unit/procCfgTests.ml @@ -93,13 +93,13 @@ let tests = assert_failure "Expected exactly one node" in check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n1 - (Instrs.single dummy_instr2) ; + (Instrs.singleton dummy_instr2) ; let backward_instr_n2 = BackwardInstrCfg.Node.of_underlying_node n2 in check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n2 Instrs.empty ; let backward_instr_n3 = BackwardInstrCfg.Node.of_underlying_node n3 in check_backward_instr_ BackwardInstrCfg.fold_preds backward_instr_n3 Instrs.empty ; check_backward_instr_ BackwardInstrCfg.fold_normal_succs backward_instr_n2 - (Instrs.single dummy_instr2) + (Instrs.singleton dummy_instr2) in "instr_test" >:: instr_test_ in