diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index afa59d411..a7702129a 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -1092,17 +1092,28 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s (* In the translation of [LHS=RHS;], if [RHS] is a complicated expression that introduced new nodes, eg a conditional expression, it forces to introduce nodes for [LHS], in order to avoid an incorrect statement order. *) + let rec is_complex_rhs stmt = + match (stmt : Clang_ast_t.stmt) with + | ConditionalOperator _ + | UnaryOperator (_, _, _, {uoi_kind= `LNot}) + | BinaryOperator + (_, _, _, {boi_kind= `Cmp | `LT | `GT | `LE | `GE | `EQ | `NE | `LAnd | `LOr}) -> + true + | UnaryOperator (_, stmts, _, _) + | BinaryOperator (_, stmts, _, _) + | ImplicitCastExpr (_, stmts, _, _) + | ParenExpr (_, stmts, _) -> + List.exists stmts ~f:is_complex_rhs + | _ -> + false + in let e1_control = - match (binary_operator_info.Clang_ast_t.boi_kind, s2) with - | ( `Assign - , Clang_ast_t.( - ( ConditionalOperator _ - | UnaryOperator _ - | ImplicitCastExpr (_, ([ConditionalOperator _] | [UnaryOperator _]), _, _) )) ) -> + match binary_operator_info.Clang_ast_t.boi_kind with + | `Assign when is_complex_rhs s2 -> let trans_state' = PriorityNode.try_claim_priority_node trans_state' stmt_info in PriorityNode.compute_controls_to_parent trans_state' sil_loc node_name stmt_info [res_trans_e1.control] - | _, _ -> + | _ -> res_trans_e1.control in let all_res_trans = [e1_control; res_trans_e2.control] @ binop_control in diff --git a/infer/tests/codetoanalyze/c/pulse/frontend.c b/infer/tests/codetoanalyze/c/pulse/frontend.c index 69aea19a3..f177a7d3a 100644 --- a/infer/tests/codetoanalyze/c/pulse/frontend.c +++ b/infer/tests/codetoanalyze/c/pulse/frontend.c @@ -35,3 +35,31 @@ void assign_implicit_cast_bad() { free(b); } } + +void assign_paren_ok() { + bool* b = (bool*)malloc(sizeof(bool)); + int x = 42, y = 33; + if (b) { + *b = true; + *b = (x == y); + if (*b) { + int* p = 0; + *p = 5; + } + free(b); + } +} + +void assign_paren_bad() { + bool* b = (bool*)malloc(sizeof(bool)); + int x = 42, y = 42; + if (b) { + *b = false; + *b = (x == y); + if (*b) { + int* p = 0; + *p = 5; + } + free(b); + } +} diff --git a/infer/tests/codetoanalyze/c/pulse/issues.exp b/infer/tests/codetoanalyze/c/pulse/issues.exp index 71e76c6c8..f8bfe2f5a 100644 --- a/infer/tests/codetoanalyze/c/pulse/issues.exp +++ b/infer/tests/codetoanalyze/c/pulse/issues.exp @@ -1,4 +1,5 @@ codetoanalyze/c/pulse/frontend.c, assign_implicit_cast_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] +codetoanalyze/c/pulse/frontend.c, assign_paren_bad, 8, NULLPTR_DEREFERENCE, no_bucket, ERROR, [invalidation part of the trace starts here,assigned,is the null pointer,use-after-lifetime part of the trace starts here,assigned,invalid access occurs here] codetoanalyze/c/pulse/interprocedural.c, if_freed_invalid_latent, 3, USE_AFTER_FREE, no_bucket, ERROR, [*** LATENT ***,invalidation part of the trace starts here,parameter `y` of if_freed_invalid_latent,was invalidated by call to `free()`,use-after-lifetime part of the trace starts here,parameter `y` of if_freed_invalid_latent,invalid access occurs here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad, 0, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,when calling `create_p` here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here] codetoanalyze/c/pulse/memory_leak.c, malloc_interproc_no_free_bad2, 4, MEMORY_LEAK, no_bucket, ERROR, [allocation part of the trace starts here,allocated by call to `malloc` (modelled),allocation part of the trace ends here,memory becomes unreachable here]