diff --git a/infer/src/IR/BUILTINS.ml b/infer/src/IR/BUILTINS.ml index 5f8c7e98c..7aca071f2 100644 --- a/infer/src/IR/BUILTINS.ml +++ b/infer/src/IR/BUILTINS.ml @@ -50,6 +50,9 @@ module type S = sig val __infer_fail : t + val __infer_skip : t + (** used to represent behavior that is not modeled in infer *) + val __instanceof : t (** [__instanceof(val,typ)] implements java's [val instanceof typ] *) diff --git a/infer/src/IR/BuiltinDecl.ml b/infer/src/IR/BuiltinDecl.ml index 73cd1ae65..4eb18c416 100644 --- a/infer/src/IR/BuiltinDecl.ml +++ b/infer/src/IR/BuiltinDecl.ml @@ -71,6 +71,8 @@ let __infer_assume = create_procname "__infer_assume" let __infer_fail = create_procname "__infer_fail" +let __infer_skip = create_procname "__infer_skip" + let __instanceof = create_procname "__instanceof" let __method_set_ignore_attribute = create_procname "__method_set_ignore_attribute" diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 1c50702c1..42dbd9b93 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/infer/src/biabduction/BuiltinDefn.ml @@ -886,6 +886,8 @@ let __infer_assume = Builtin.register BuiltinDecl.__infer_assume execute___infer (* externally create new errors *) let __infer_fail = Builtin.register BuiltinDecl.__infer_fail execute___infer_fail +let __infer_skip = Builtin.register BuiltinDecl.__infer_skip execute_skip + (* [__instanceof(val,typ)] implements java's [val instanceof typ] *) let __instanceof = Builtin.register BuiltinDecl.__instanceof execute___instanceof diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 4c73a8451..77818db59 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -992,7 +992,6 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let context = trans_state.context in let fn_type_no_ref = CType_decl.get_type_from_expr_info expr_info context.CContext.tenv in let function_type = add_reference_if_glvalue fn_type_no_ref expr_info in - let procname = Procdesc.get_proc_name context.CContext.procdesc in let sil_loc = CLocation.get_sil_location si context in (* First stmt is the function expr and the rest are params *) let fun_exp_stmt, params_stmt = @@ -1039,6 +1038,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s if Int.equal (List.length params) (List.length params_stmt) then params else (* FIXME(t21762295) this is reachable *) + let procname = Procdesc.get_proc_name context.CContext.procdesc in CFrontend_config.incorrect_assumption __POS__ si.Clang_ast_t.si_source_range "In call to %a: stmt_list and res_trans_par.exps must have same size but they don't:@\n\ stmt_list(%d)=[%a]@\n\ @@ -3082,8 +3082,10 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s {empty_res_trans with exps= [(CTrans_utils.undefined_expression (), typ)]} - (* no-op translated for unsupported instructions that will at least translate subexpressions *) - and skip_unimplemented trans_state stmts = instructions trans_state stmts + (** no-op translated for unsupported instructions that will at least translate subexpressions *) + and skip_unimplemented ~reason trans_state stmts = + call_function_with_args reason BuiltinDecl.__infer_skip trans_state stmts + (* Translates a clang instruction into SIL instructions. It takes a *) (* a trans_state containing current info on the translation and it returns *) @@ -3306,8 +3308,12 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s sub-expressions *) | ObjCAvailabilityCheckExpr (_, _, expr_info, _) -> trans_into_undefined_expr trans_state expr_info - | ExtVectorElementExpr (_, stmts, _) | ShuffleVectorExpr (_, stmts, _) -> - skip_unimplemented trans_state stmts + | ExtVectorElementExpr (stmt_info, stmts, _) | ShuffleVectorExpr (stmt_info, stmts, _) -> + skip_unimplemented + ~reason: + (Printf.sprintf "unimplemented construct: %s" + (Clang_ast_proj.get_stmt_kind_string instr)) + trans_state stmt_info stmts (* Infer somehow ended up in templated non instantiated code - right now it's not supported and failure in those cases is expected. *) | SubstNonTypeTemplateParmExpr _ diff --git a/infer/tests/codetoanalyze/cpp/frontend/vectors/shuffle_vector.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/vectors/shuffle_vector.cpp.dot index de0e3a6d0..7aad11e76 100644 --- a/infer/tests/codetoanalyze/cpp/frontend/vectors/shuffle_vector.cpp.dot +++ b/infer/tests/codetoanalyze/cpp/frontend/vectors/shuffle_vector.cpp.dot @@ -7,7 +7,7 @@ digraph cfg { "simple#17639603251097432993.e5c9feb95ecff69f23df6ce422f34819_2" [label="2: Exit simple \n " color=yellow style=filled] -"simple#17639603251097432993.e5c9feb95ecff69f23df6ce422f34819_3" [label="3: Return Stmt \n n$0=*&vec:void [line 12, column 44]\n *&return:void=n$0 [line 12, column 37]\n " shape="box"] +"simple#17639603251097432993.e5c9feb95ecff69f23df6ce422f34819_3" [label="3: Return Stmt \n _fun___infer_skip(&vec:void&) [line 12, column 44]\n n$0=*-1:void [line 12, column 44]\n *&return:void=n$0 [line 12, column 37]\n " shape="box"] "simple#17639603251097432993.e5c9feb95ecff69f23df6ce422f34819_3" -> "simple#17639603251097432993.e5c9feb95ecff69f23df6ce422f34819_2" ;