diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index de007d1f1..fb81649ee 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -930,65 +930,32 @@ struct Sil.mk_pvar (Mangled.from_string ("SIL_temp_conditional___"^(string_of_int id))) procname in let sil_loc = CLocation.get_sil_location stmt_info parent_line_number context in let line_number = CLocation.get_line stmt_info parent_line_number in - (* We have two different kind of join type for conditional operator. *) - (* If it's a simple conditional operator then we use a standard join *) - (* node. If it's a nested conditional operator then we need to *) - (* assign the temp variable of the inner conditional to the outer *) - (* conditional. In that case we use a statement node for join. This *) - (* node make the assignment of the temp variables. *) - let compute_join_node typ = - let join_node' = match succ_nodes with - | [n] when is_join_node n -> - let n'= create_node (Cfg.Node.Stmt_node "Temp Join Node") [] [] sil_loc context in - let id = Ident.create_fresh Ident.knormal in - let pvar = mk_temp_var (Cfg.Node.get_id n) in - let pvar' = mk_temp_var (Cfg.Node.get_id n') in - let ilist =[Sil.Letderef (id, Sil.Lvar pvar', typ, sil_loc); - Sil.Declare_locals([(pvar, typ)], sil_loc); - Sil.Set (Sil.Lvar pvar, typ, Sil.Var id, sil_loc); - Sil.Nullify(pvar', sil_loc, true)] in - Cfg.Node.append_instrs_temps n' ilist [id]; n' - | _ -> create_node (Cfg.Node.Join_node) [] [] sil_loc context in - Cfg.Node.set_succs_exn join_node' succ_nodes []; - join_node' in let do_branch branch stmt typ prune_nodes join_node pvar = - let trans_state' = { trans_state with succ_nodes = [join_node]; parent_line_number = line_number } in - let res_trans_b = - exec_with_priority_exception trans_state' stmt instruction in - let node_b = res_trans_b.root_nodes in + let trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in + let trans_state' = { trans_state_pri with + succ_nodes = []; + parent_line_number = line_number } in + let res_trans_b = instruction trans_state' stmt in let (e', e'_typ) = extract_exp_from_list res_trans_b.exps "\nWARNING: Missing branch expression for Conditional operator. Need to be fixed\n" in - (* If e' is the address of a prog var, we need to get its value in a temp before assign it to temp_var*) - let e'', instr_e'', id_e'' = match e' with - | Sil.Lvar _ -> - let id = Ident.create_fresh Ident.knormal in - Sil.Var id,[Sil.Letderef (id, e', typ, sil_loc)], [id] - | _ -> e', [], [] in - let set_temp_var = [Sil.Declare_locals([(pvar, typ)], sil_loc); Sil.Set (Sil.Lvar pvar, typ, e'', sil_loc)] in - let nodes_branch = (match node_b, is_join_node join_node with - | [], _ -> let n = create_node (Cfg.Node.Stmt_node "ConditinalStmt Branch" ) (res_trans_b.ids@id_e'') (res_trans_b.instrs @ instr_e'' @ set_temp_var) sil_loc context in - Cfg.Node.set_succs_exn n [join_node] []; - [n] - | _, true -> - IList.iter - (fun n' -> - (* If there is a node with instructions we need to only *) - (* add the set of the temp variable *) - if not (is_prune_node n') then - Cfg.Node.append_instrs_temps n' - (res_trans_b.instrs @ instr_e''@ set_temp_var) - (res_trans_b.ids @ id_e'') - ) node_b; - node_b - | _, false -> node_b) in + let set_temp_var = [ + Sil.Declare_locals([(pvar, typ)], sil_loc); + Sil.Set (Sil.Lvar pvar, typ, e', sil_loc) + ] in + let tmp_var_res_trans = { empty_res_trans with instrs = set_temp_var } in + let trans_state'' = { trans_state' with succ_nodes = [join_node] } in + let all_res_trans = [res_trans_b; tmp_var_res_trans] in + let res_trans = PriorityNode.compute_results_to_parent trans_state'' sil_loc + "ConditinalStmt Branch" stmt_info all_res_trans in let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes in let prune_nodes' = if branch then prune_nodes_t else prune_nodes_f in - IList.iter (fun n -> Cfg.Node.set_succs_exn n nodes_branch []) prune_nodes' in + IList.iter (fun n -> Cfg.Node.set_succs_exn n res_trans.root_nodes []) prune_nodes' in (match stmt_list with | [cond; exp1; exp2] -> let typ = CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in - let join_node = compute_join_node typ in + let join_node = create_node (Cfg.Node.Join_node) [] [] sil_loc context in + Cfg.Node.set_succs_exn join_node succ_nodes []; let pvar = mk_temp_var (Cfg.Node.get_id join_node) in let continuation' = mk_cond_continuation trans_state.continuation in let trans_state' = { trans_state with continuation = continuation'; parent_line_number = line_number; succ_nodes =[]} in @@ -1312,7 +1279,7 @@ struct | Loops.While (decl_stmt_opt, _, _) -> decl_stmt_opt | _ -> None in let res_trans_decl = match decl_stmt_opt with - | Some decl_stmt -> declStmt_in_condition_trans trans_state_cond decl_stmt res_trans_cond + | Some decl_stmt -> declStmt_in_condition_trans trans_state decl_stmt res_trans_cond | _ -> res_trans_cond in let body_succ_nodes = match loop_kind with diff --git a/infer/src/clang/cTrans_utils.ml b/infer/src/clang/cTrans_utils.ml index 55d1820c4..549609034 100644 --- a/infer/src/clang/cTrans_utils.ml +++ b/infer/src/clang/cTrans_utils.ml @@ -200,6 +200,10 @@ struct Printing.log_out "Priority busy in %s. No claim possible\n@." stmt_info.Clang_ast_t.si_pointer; trans_state + let force_claim_priority_node trans_state stmt_info = + { trans_state with priority = Busy stmt_info.Clang_ast_t.si_pointer } + + let is_priority_free trans_state = match trans_state.priority with | Free -> true @@ -222,7 +226,7 @@ struct (* Invariant: if leaf_nodes is empty then the params have not created a node.*) let res_state_param = collect_res_trans res_states_children in let create_node = own_priority_node trans_state.priority stmt_info && res_state_param.instrs <> [] in - match res_state_param.leaf_nodes, create_node with + match res_state_param.root_nodes, create_node with | _, false -> (* The node is created by the parent. We just pass back nodes/leafs params *) { res_state_param with exps = []} | [], true -> (* We need to create a node and params did not create a node.*) @@ -428,7 +432,7 @@ let trans_assertion_failure sil_loc context = Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [] [call_instr] sil_loc context in Cfg.Node.set_succs_exn failure_node [exit_node] []; { root_nodes = [failure_node]; - leaf_nodes = [failure_node]; + leaf_nodes = []; ids = []; instrs =[]; exps = [] } diff --git a/infer/src/clang/cTrans_utils.mli b/infer/src/clang/cTrans_utils.mli index b4da92de4..a98b00361 100644 --- a/infer/src/clang/cTrans_utils.mli +++ b/infer/src/clang/cTrans_utils.mli @@ -152,6 +152,8 @@ sig val try_claim_priority_node : trans_state -> Clang_ast_t.stmt_info -> trans_state + val force_claim_priority_node : trans_state -> Clang_ast_t.stmt_info -> trans_state + val own_priority_node : t -> Clang_ast_t.stmt_info -> bool (* Used by translation functions to handle potenatial cfg nodes. *) diff --git a/infer/tests/codetoanalyze/c/frontend/conditional_operator/cond2.c.dot b/infer/tests/codetoanalyze/c/frontend/conditional_operator/cond2.c.dot index 36d39eb51..2d2ea41e2 100644 --- a/infer/tests/codetoanalyze/c/frontend/conditional_operator/cond2.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/conditional_operator/cond2.c.dot @@ -1,172 +1,176 @@ digraph iCFG { -57 [label="57: BinaryOperatorStmt: Assign \n n$6=*&SIL_temp_conditional___51:int [line 23]\n NULLIFY(&SIL_temp_conditional___51,true); [line 23]\n *&y:int =n$6 [line 23]\n REMOVE_TEMPS(n$6); [line 23]\n NULLIFY(&y,false); [line 23]\n " shape="box"] +58 [label="58: BinaryOperatorStmt: Assign \n n$6=*&SIL_temp_conditional___52:int [line 23]\n NULLIFY(&SIL_temp_conditional___52,true); [line 23]\n *&y:int =n$6 [line 23]\n REMOVE_TEMPS(n$6); [line 23]\n NULLIFY(&y,false); [line 23]\n " shape="box"] - 57 -> 41 ; - 57 -> 42 ; -56 [label="56: UnaryOperator \n n$5=*&x:int [line 23]\n *&x:int =(n$5 - 1) [line 23]\n DECLARE_LOCALS(&SIL_temp_conditional___51); [line 23]\n *&SIL_temp_conditional___51:int =n$5 [line 23]\n REMOVE_TEMPS(n$5); [line 23]\n NULLIFY(&x,false); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"] + 58 -> 42 ; + 58 -> 43 ; +57 [label="57: ConditinalStmt Branch \n n$5=*&x:int [line 23]\n *&x:int =(n$5 - 1) [line 23]\n DECLARE_LOCALS(&SIL_temp_conditional___52); [line 23]\n *&SIL_temp_conditional___52:int =n$5 [line 23]\n REMOVE_TEMPS(n$5); [line 23]\n NULLIFY(&x,false); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"] - 56 -> 51 ; -55 [label="55: UnaryOperator \n n$4=*&x:int [line 23]\n *&x:int =(n$4 + 1) [line 23]\n DECLARE_LOCALS(&SIL_temp_conditional___51); [line 23]\n *&SIL_temp_conditional___51:int =(n$4 + 1) [line 23]\n REMOVE_TEMPS(n$4); [line 23]\n NULLIFY(&x,false); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"] + 57 -> 52 ; +56 [label="56: ConditinalStmt Branch \n n$4=*&x:int [line 23]\n *&x:int =(n$4 + 1) [line 23]\n DECLARE_LOCALS(&SIL_temp_conditional___52); [line 23]\n *&SIL_temp_conditional___52:int =(n$4 + 1) [line 23]\n REMOVE_TEMPS(n$4); [line 23]\n NULLIFY(&x,false); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"] - 55 -> 51 ; -54 [label="54: Prune (false branch) \n PRUNE(((n$3 > 1) == 0), false); [line 23]\n REMOVE_TEMPS(n$3); [line 23]\n " shape="invhouse"] + 56 -> 52 ; +55 [label="55: Prune (false branch) \n PRUNE(((n$3 > 1) == 0), false); [line 23]\n REMOVE_TEMPS(n$3); [line 23]\n " shape="invhouse"] + + + 55 -> 57 ; +54 [label="54: Prune (true branch) \n PRUNE(((n$3 > 1) != 0), true); [line 23]\n REMOVE_TEMPS(n$3); [line 23]\n " shape="invhouse"] 54 -> 56 ; -53 [label="53: Prune (true branch) \n PRUNE(((n$3 > 1) != 0), true); [line 23]\n REMOVE_TEMPS(n$3); [line 23]\n " shape="invhouse"] +53 [label="53: BinaryOperatorStmt: GT \n *&x:int =1 [line 23]\n n$3=*&x:int [line 23]\n " shape="box"] + 53 -> 54 ; 53 -> 55 ; -52 [label="52: BinaryOperatorStmt: GT \n *&x:int =1 [line 23]\n n$3=*&x:int [line 23]\n " shape="box"] +52 [label="52: + \n " ] - 52 -> 53 ; - 52 -> 54 ; -51 [label="51: + \n " ] + 52 -> 58 ; +51 [label="51: Return Stmt \n n$2=*&SIL_temp_conditional___40:int [line 24]\n NULLIFY(&SIL_temp_conditional___40,true); [line 24]\n *&return:int =(0 + n$2) [line 24]\n REMOVE_TEMPS(n$2); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] - 51 -> 57 ; -50 [label="50: Return Stmt \n n$2=*&SIL_temp_conditional___39:int [line 24]\n NULLIFY(&SIL_temp_conditional___39,true); [line 24]\n *&return:int =(0 + n$2) [line 24]\n REMOVE_TEMPS(n$2); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] + 51 -> 39 ; +50 [label="50: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 24]\n *&SIL_temp_conditional___40:int =0 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] - 50 -> 38 ; -49 [label="49: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___39); [line 24]\n *&SIL_temp_conditional___39:int =0 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] + 50 -> 40 ; +49 [label="49: ConditinalStmt Branch \n *&x:int =1 [line 24]\n n$1=*&x:int [line 24]\n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 24]\n *&SIL_temp_conditional___40:int =n$1 [line 24]\n REMOVE_TEMPS(n$1); [line 24]\n NULLIFY(&x,false); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] - 49 -> 39 ; -48 [label="48: BinaryOperatorStmt: Assign \n *&x:int =1 [line 24]\n n$1=*&x:int [line 24]\n DECLARE_LOCALS(&SIL_temp_conditional___39); [line 24]\n *&SIL_temp_conditional___39:int =n$1 [line 24]\n REMOVE_TEMPS(n$1); [line 24]\n NULLIFY(&x,false); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] + 49 -> 40 ; +48 [label="48: Prune (false branch) \n PRUNE(((n$0 > 1) == 0), false); [line 24]\n REMOVE_TEMPS(n$0); [line 24]\n " shape="invhouse"] - 48 -> 39 ; -47 [label="47: Prune (false branch) \n PRUNE(((n$0 > 1) == 0), false); [line 24]\n REMOVE_TEMPS(n$0); [line 24]\n " shape="invhouse"] + 48 -> 50 ; +47 [label="47: Prune (true branch) \n PRUNE(((n$0 > 1) != 0), true); [line 24]\n REMOVE_TEMPS(n$0); [line 24]\n " shape="invhouse"] 47 -> 49 ; -46 [label="46: Prune (true branch) \n PRUNE(((n$0 > 1) != 0), true); [line 24]\n REMOVE_TEMPS(n$0); [line 24]\n " shape="invhouse"] +46 [label="46: BinaryOperatorStmt: GT \n n$0=*&SIL_temp_conditional___41:int [line 24]\n NULLIFY(&SIL_temp_conditional___41,true); [line 24]\n " shape="box"] + 46 -> 47 ; 46 -> 48 ; -45 [label="45: BinaryOperatorStmt: GT \n n$0=*&SIL_temp_conditional___40:int [line 24]\n NULLIFY(&SIL_temp_conditional___40,true); [line 24]\n " shape="box"] +45 [label="45: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___41); [line 24]\n *&SIL_temp_conditional___41:int =2 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] - 45 -> 46 ; - 45 -> 47 ; -44 [label="44: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 24]\n *&SIL_temp_conditional___40:int =2 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] + 45 -> 41 ; +44 [label="44: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___41); [line 24]\n *&SIL_temp_conditional___41:int =1 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] - 44 -> 40 ; -43 [label="43: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 24]\n *&SIL_temp_conditional___40:int =1 [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] + 44 -> 41 ; +43 [label="43: Prune (false branch) \n PRUNE(((3 > 4) == 0), false); [line 24]\n " shape="invhouse"] - 43 -> 40 ; -42 [label="42: Prune (false branch) \n PRUNE(((3 > 4) == 0), false); [line 24]\n " shape="invhouse"] + 43 -> 45 ; +42 [label="42: Prune (true branch) \n PRUNE(((3 > 4) != 0), true); [line 24]\n " shape="invhouse"] 42 -> 44 ; -41 [label="41: Prune (true branch) \n PRUNE(((3 > 4) != 0), true); [line 24]\n " shape="invhouse"] +41 [label="41: + \n " ] - 41 -> 43 ; + 41 -> 46 ; 40 [label="40: + \n " ] - 40 -> 45 ; -39 [label="39: + \n " ] + 40 -> 51 ; +39 [label="39: Exit bar \n " color=yellow style=filled] - 39 -> 50 ; -38 [label="38: Exit bar \n " color=yellow style=filled] +38 [label="38: Start bar\nFormals: \nLocals: y:int x:int \n DECLARE_LOCALS(&return,&y,&x); [line 21]\n NULLIFY(&x,false); [line 21]\n NULLIFY(&y,false); [line 21]\n " color=yellow style=filled] -37 [label="37: Start bar\nFormals: \nLocals: y:int x:int \n DECLARE_LOCALS(&return,&y,&x); [line 21]\n NULLIFY(&x,false); [line 21]\n NULLIFY(&y,false); [line 21]\n " color=yellow style=filled] + 38 -> 53 ; +37 [label="37: DeclStmt \n *&x:int =5 [line 12]\n " shape="box"] - 37 -> 52 ; -36 [label="36: DeclStmt \n *&x:int =5 [line 12]\n " shape="box"] + 37 -> 31 ; + 37 -> 32 ; +36 [label="36: BinaryOperatorStmt: Assign \n NULLIFY(&x,false); [line 13]\n *&x:int =0 [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="box"] 36 -> 30 ; - 36 -> 31 ; -35 [label="35: BinaryOperatorStmt: Assign \n NULLIFY(&x,false); [line 13]\n *&x:int =0 [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="box"] +35 [label="35: Prune (false branch) \n PRUNE(((7 < n$6) == 0), false); [line 13]\n REMOVE_TEMPS(n$6); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] - 35 -> 29 ; -34 [label="34: Prune (false branch) \n PRUNE(((7 < n$7) == 0), false); [line 13]\n REMOVE_TEMPS(n$7); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] + 35 -> 30 ; +34 [label="34: Prune (true branch) \n PRUNE(((7 < n$6) != 0), true); [line 13]\n REMOVE_TEMPS(n$6); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] - 34 -> 29 ; -33 [label="33: Prune (true branch) \n PRUNE(((7 < n$7) != 0), true); [line 13]\n REMOVE_TEMPS(n$7); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] + 34 -> 36 ; +33 [label="33: BinaryOperatorStmt: LT \n n$6=*&x:int [line 13]\n *&x:int =(n$6 + 1) [line 13]\n " shape="box"] + 33 -> 34 ; 33 -> 35 ; -32 [label="32: BinaryOperatorStmt: LT \n n$7=*&x:int [line 13]\n *&x:int =(n$7 + 1) [line 13]\n " shape="box"] +32 [label="32: Prune (false branch) \n PRUNE(((3 < 4) == 0), false); [line 13]\n " shape="invhouse"] 32 -> 33 ; - 32 -> 34 ; -31 [label="31: Prune (false branch) \n PRUNE(((3 < 4) == 0), false); [line 13]\n " shape="invhouse"] +31 [label="31: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] - 31 -> 32 ; -30 [label="30: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] + 31 -> 36 ; +30 [label="30: + \n " ] - 30 -> 35 ; -29 [label="29: + \n " ] + 30 -> 29 ; +29 [label="29: DeclStmt \n *&y:int =19 [line 14]\n " shape="box"] - 29 -> 28 ; -28 [label="28: DeclStmt \n *&y:int =19 [line 14]\n " shape="box"] + 29 -> 21 ; + 29 -> 22 ; +28 [label="28: DeclStmt \n n$5=*&SIL_temp_conditional___20:int [line 15]\n NULLIFY(&SIL_temp_conditional___20,true); [line 15]\n *&n:int =n$5 [line 15]\n REMOVE_TEMPS(n$5); [line 15]\n NULLIFY(&n,false); [line 15]\n " shape="box"] - 28 -> 20 ; - 28 -> 21 ; -27 [label="27: DeclStmt \n n$6=*&SIL_temp_conditional___19:int [line 15]\n NULLIFY(&SIL_temp_conditional___19,true); [line 15]\n *&n:int =n$6 [line 15]\n REMOVE_TEMPS(n$6); [line 15]\n NULLIFY(&n,false); [line 15]\n " shape="box"] + 28 -> 10 ; + 28 -> 11 ; +27 [label="27: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___20); [line 15]\n *&SIL_temp_conditional___20:int =2 [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"] - 27 -> 10 ; - 27 -> 11 ; -26 [label="26: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___19); [line 15]\n *&SIL_temp_conditional___19:int =2 [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"] + 27 -> 20 ; +26 [label="26: ConditinalStmt Branch \n NULLIFY(&x,false); [line 15]\n NULLIFY(&y,false); [line 15]\n DECLARE_LOCALS(&SIL_temp_conditional___20); [line 15]\n *&SIL_temp_conditional___20:int =1 [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"] - 26 -> 19 ; -25 [label="25: ConditinalStmt Branch \n NULLIFY(&x,false); [line 15]\n NULLIFY(&y,false); [line 15]\n DECLARE_LOCALS(&SIL_temp_conditional___19); [line 15]\n *&SIL_temp_conditional___19:int =1 [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"] + 26 -> 20 ; +25 [label="25: Prune (false branch) \n PRUNE(((7 < (n$3 - n$4)) == 0), false); [line 15]\n REMOVE_TEMPS(n$3,n$4); [line 15]\n " shape="invhouse"] - 25 -> 19 ; -24 [label="24: Prune (false branch) \n PRUNE(((7 < (n$4 - n$5)) == 0), false); [line 15]\n REMOVE_TEMPS(n$4,n$5); [line 15]\n " shape="invhouse"] + 25 -> 27 ; +24 [label="24: Prune (true branch) \n PRUNE(((7 < (n$3 - n$4)) != 0), true); [line 15]\n REMOVE_TEMPS(n$3,n$4); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="invhouse"] 24 -> 26 ; -23 [label="23: Prune (true branch) \n PRUNE(((7 < (n$4 - n$5)) != 0), true); [line 15]\n REMOVE_TEMPS(n$4,n$5); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="invhouse"] +23 [label="23: BinaryOperatorStmt: LT \n n$3=*&x:int [line 15]\n *&x:int =(n$3 + 1) [line 15]\n n$4=*&y:int [line 15]\n NULLIFY(&x,false); [line 15]\n NULLIFY(&y,false); [line 15]\n " shape="box"] + 23 -> 24 ; 23 -> 25 ; -22 [label="22: BinaryOperatorStmt: LT \n n$4=*&x:int [line 15]\n *&x:int =(n$4 + 1) [line 15]\n n$5=*&y:int [line 15]\n NULLIFY(&x,false); [line 15]\n NULLIFY(&y,false); [line 15]\n " shape="box"] +22 [label="22: Prune (false branch) \n PRUNE(((3 < 4) == 0), false); [line 15]\n " shape="invhouse"] 22 -> 23 ; - 22 -> 24 ; -21 [label="21: Prune (false branch) \n PRUNE(((3 < 4) == 0), false); [line 15]\n " shape="invhouse"] +21 [label="21: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="invhouse"] - 21 -> 22 ; -20 [label="20: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="invhouse"] + 21 -> 26 ; +20 [label="20: + \n " ] - 20 -> 25 ; -19 [label="19: + \n " ] + 20 -> 28 ; +19 [label="19: BinaryOperatorStmt: Assign \n n$2=*&SIL_temp_conditional___9:int [line 16]\n NULLIFY(&SIL_temp_conditional___9,true); [line 16]\n *&n:int =n$2 [line 16]\n REMOVE_TEMPS(n$2); [line 16]\n NULLIFY(&n,false); [line 16]\n " shape="box"] - 19 -> 27 ; -18 [label="18: BinaryOperatorStmt: Assign \n n$3=*&SIL_temp_conditional___9:int [line 16]\n NULLIFY(&SIL_temp_conditional___9,true); [line 16]\n *&n:int =n$3 [line 16]\n REMOVE_TEMPS(n$3); [line 16]\n NULLIFY(&n,false); [line 16]\n " shape="box"] + 19 -> 4 ; + 19 -> 5 ; +18 [label="18: ConditinalStmt Branch \n n$1=*&SIL_temp_conditional___13:int [line 16]\n NULLIFY(&SIL_temp_conditional___13,true); [line 16]\n DECLARE_LOCALS(&SIL_temp_conditional___9); [line 16]\n *&SIL_temp_conditional___9:int =n$1 [line 16]\n REMOVE_TEMPS(n$1); [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"] - 18 -> 4 ; - 18 -> 5 ; + 18 -> 9 ; 17 [label="17: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___13); [line 16]\n *&SIL_temp_conditional___13:int =2 [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"] @@ -183,10 +187,10 @@ digraph iCFG { 14 -> 16 ; -13 [label="13: Temp Join Node \n n$1=*&SIL_temp_conditional___13:int [line 16]\n DECLARE_LOCALS(&SIL_temp_conditional___9); [line 16]\n *&SIL_temp_conditional___9:int =n$1 [line 16]\n NULLIFY(&SIL_temp_conditional___13,true); [line 16]\n REMOVE_TEMPS(n$1); [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"] +13 [label="13: + \n " ] - 13 -> 9 ; + 13 -> 18 ; 12 [label="12: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___9); [line 16]\n *&SIL_temp_conditional___9:int =1 [line 16]\n APPLY_ABSTRACTION; [line 16]\n " shape="box"] @@ -203,7 +207,7 @@ digraph iCFG { 9 [label="9: + \n " ] - 9 -> 18 ; + 9 -> 19 ; 8 [label="8: Return Stmt \n n$0=*&SIL_temp_conditional___3:int [line 17]\n NULLIFY(&SIL_temp_conditional___3,true); [line 17]\n *&return:int =(0 + n$0) [line 17]\n REMOVE_TEMPS(n$0); [line 17]\n APPLY_ABSTRACTION; [line 17]\n " shape="box"] @@ -234,5 +238,5 @@ digraph iCFG { 1 [label="1: Start foo\nFormals: \nLocals: n:int y:int x:int \n DECLARE_LOCALS(&return,&n,&y,&x); [line 10]\n NULLIFY(&n,false); [line 10]\n NULLIFY(&x,false); [line 10]\n NULLIFY(&y,false); [line 10]\n " color=yellow style=filled] - 1 -> 36 ; + 1 -> 37 ; } diff --git a/infer/tests/codetoanalyze/c/frontend/conditional_operator/conditional_operator.c.dot b/infer/tests/codetoanalyze/c/frontend/conditional_operator/conditional_operator.c.dot index edde9f2b1..7cb271fa9 100644 --- a/infer/tests/codetoanalyze/c/frontend/conditional_operator/conditional_operator.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/conditional_operator/conditional_operator.c.dot @@ -7,7 +7,7 @@ digraph iCFG { 53 -> 49 ; -52 [label="52: UnaryOperator \n n$1=*&p:int * [line 42]\n n$2=*n$1:int [line 42]\n DECLARE_LOCALS(&SIL_temp_conditional___49); [line 42]\n *&SIL_temp_conditional___49:int =n$2 [line 42]\n REMOVE_TEMPS(n$1,n$2); [line 42]\n NULLIFY(&p,false); [line 42]\n APPLY_ABSTRACTION; [line 42]\n " shape="box"] +52 [label="52: ConditinalStmt Branch \n n$1=*&p:int * [line 42]\n n$2=*n$1:int [line 42]\n DECLARE_LOCALS(&SIL_temp_conditional___49); [line 42]\n *&SIL_temp_conditional___49:int =n$2 [line 42]\n REMOVE_TEMPS(n$1,n$2); [line 42]\n NULLIFY(&p,false); [line 42]\n APPLY_ABSTRACTION; [line 42]\n " shape="box"] 52 -> 49 ; diff --git a/infer/tests/codetoanalyze/c/frontend/conditional_operator/member_access.c.dot b/infer/tests/codetoanalyze/c/frontend/conditional_operator/member_access.c.dot index 3d9566b5c..e7871734b 100644 --- a/infer/tests/codetoanalyze/c/frontend/conditional_operator/member_access.c.dot +++ b/infer/tests/codetoanalyze/c/frontend/conditional_operator/member_access.c.dot @@ -7,7 +7,7 @@ digraph iCFG { 23 -> 19 ; -22 [label="22: Call _fun_ret_ptr \n n$0=_fun_ret_ptr(4:int ) [line 25]\n n$1=*n$0.field:int [line 25]\n DECLARE_LOCALS(&SIL_temp_conditional___19); [line 25]\n *&SIL_temp_conditional___19:int =n$1 [line 25]\n REMOVE_TEMPS(n$0,n$1); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="box"] +22 [label="22: ConditinalStmt Branch \n n$0=_fun_ret_ptr(4:int ) [line 25]\n n$1=*n$0.field:int [line 25]\n DECLARE_LOCALS(&SIL_temp_conditional___19); [line 25]\n *&SIL_temp_conditional___19:int =n$1 [line 25]\n REMOVE_TEMPS(n$0,n$1); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="box"] 22 -> 19 ; diff --git a/infer/tests/codetoanalyze/objc/frontend/assertions/NSAssert_example.dot b/infer/tests/codetoanalyze/objc/frontend/assertions/NSAssert_example.dot index 04357ecd7..31bdd605f 100644 --- a/infer/tests/codetoanalyze/objc/frontend/assertions/NSAssert_example.dot +++ b/infer/tests/codetoanalyze/objc/frontend/assertions/NSAssert_example.dot @@ -8,7 +8,7 @@ digraph iCFG { 107 -> 101 ; -106 [label="106: Message Call: stringWithUTF8String: \n n$17=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 36]\n DECLARE_LOCALS(&SIL_temp_conditional___102); [line 36]\n *&SIL_temp_conditional___102:class NSString *=n$17 [line 36]\n REMOVE_TEMPS(n$17); [line 36]\n APPLY_ABSTRACTION; [line 36]\n " shape="box"] +106 [label="106: ConditinalStmt Branch \n n$17=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 36]\n DECLARE_LOCALS(&SIL_temp_conditional___102); [line 36]\n *&SIL_temp_conditional___102:class NSString *=n$17 [line 36]\n REMOVE_TEMPS(n$17); [line 36]\n APPLY_ABSTRACTION; [line 36]\n " shape="box"] 106 -> 102 ; @@ -37,7 +37,7 @@ digraph iCFG { 100 -> 94 ; -99 [label="99: Message Call: stringWithUTF8String: \n n$11=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 36]\n DECLARE_LOCALS(&SIL_temp_conditional___95); [line 36]\n *&SIL_temp_conditional___95:class NSString *=n$11 [line 36]\n REMOVE_TEMPS(n$11); [line 36]\n APPLY_ABSTRACTION; [line 36]\n " shape="box"] +99 [label="99: ConditinalStmt Branch \n n$11=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 36]\n DECLARE_LOCALS(&SIL_temp_conditional___95); [line 36]\n *&SIL_temp_conditional___95:class NSString *=n$11 [line 36]\n REMOVE_TEMPS(n$11); [line 36]\n APPLY_ABSTRACTION; [line 36]\n " shape="box"] 99 -> 95 ; @@ -128,7 +128,7 @@ digraph iCFG { 78 -> 72 ; -77 [label="77: Message Call: stringWithUTF8String: \n n$16=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___73); [line 31]\n *&SIL_temp_conditional___73:class NSString *=n$16 [line 31]\n REMOVE_TEMPS(n$16); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"] +77 [label="77: ConditinalStmt Branch \n n$16=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___73); [line 31]\n *&SIL_temp_conditional___73:class NSString *=n$16 [line 31]\n REMOVE_TEMPS(n$16); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"] 77 -> 73 ; @@ -157,7 +157,7 @@ digraph iCFG { 71 -> 65 ; -70 [label="70: Message Call: stringWithUTF8String: \n n$10=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___66); [line 31]\n *&SIL_temp_conditional___66:class NSString *=n$10 [line 31]\n REMOVE_TEMPS(n$10); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"] +70 [label="70: ConditinalStmt Branch \n n$10=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 31]\n DECLARE_LOCALS(&SIL_temp_conditional___66); [line 31]\n *&SIL_temp_conditional___66:class NSString *=n$10 [line 31]\n REMOVE_TEMPS(n$10); [line 31]\n APPLY_ABSTRACTION; [line 31]\n " shape="box"] 70 -> 66 ; @@ -263,7 +263,7 @@ digraph iCFG { 45 -> 39 ; -44 [label="44: Message Call: stringWithUTF8String: \n n$26=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 24]\n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 24]\n *&SIL_temp_conditional___40:class NSString *=n$26 [line 24]\n REMOVE_TEMPS(n$26); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] +44 [label="44: ConditinalStmt Branch \n n$26=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 24]\n DECLARE_LOCALS(&SIL_temp_conditional___40); [line 24]\n *&SIL_temp_conditional___40:class NSString *=n$26 [line 24]\n REMOVE_TEMPS(n$26); [line 24]\n APPLY_ABSTRACTION; [line 24]\n " shape="box"] 44 -> 40 ; @@ -358,7 +358,7 @@ digraph iCFG { 22 -> 16 ; -21 [label="21: Message Call: stringWithUTF8String: \n n$11=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 19]\n DECLARE_LOCALS(&SIL_temp_conditional___17); [line 19]\n *&SIL_temp_conditional___17:class NSString *=n$11 [line 19]\n REMOVE_TEMPS(n$11); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"] +21 [label="21: ConditinalStmt Branch \n n$11=_fun_NSString_stringWithUTF8String:(\"\":char *) [line 19]\n DECLARE_LOCALS(&SIL_temp_conditional___17); [line 19]\n *&SIL_temp_conditional___17:class NSString *=n$11 [line 19]\n REMOVE_TEMPS(n$11); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"] 21 -> 17 ;