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

Use priority node for branches inside coditional operator

Browse Source 
Summary:
public
Modify do_branch inside conditionalOperator_trans:
1. Remove TempJoinNode optimization - instead create join node as usually. It produces one more node, but it's much cleaner
2. Claim priority inside do_branch instead of appending instructions to node created by children
3. Use compute_results_to_parent to some extent
4. Random changes to loop_instruction and trans_assertion_failure to make tests pass

Reviewed By: ddino

Differential Revision: D2708076

fb-gh-sync-id: d429167
master
Andrzej Kotulski 9 years ago committed by facebook-github-bot-5
parent 9db84e3a86
commit a1c1b10862
7 changed files with 118 additions and 141 deletions
Show Stats Download Patch File Download Diff File

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

@ -930,65 +930,32 @@ struct
Sil.mk_pvar (Mangled.from_string ("SIL_temp_conditional___"^(string_of_int id))) procname in 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 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 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 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 trans_state_pri = PriorityNode.force_claim_priority_node trans_state stmt_info in
let res_trans_b = let trans_state' = { trans_state_pri with
exec_with_priority_exception trans_state' stmt instruction in succ_nodes = [];
let node_b = res_trans_b.root_nodes in 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 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 "\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 set_temp_var = [
let e'', instr_e'', id_e'' = match e' with Sil.Declare_locals([(pvar, typ)], sil_loc);
| Sil.Lvar _ -> Sil.Set (Sil.Lvar pvar, typ, e', sil_loc)
let id = Ident.create_fresh Ident.knormal in ] in
Sil.Var id,[Sil.Letderef (id, e', typ, sil_loc)], [id] let tmp_var_res_trans = { empty_res_trans with instrs = set_temp_var } in
| _ -> e', [], [] in let trans_state'' = { trans_state' with succ_nodes = [join_node] } in
let set_temp_var = [Sil.Declare_locals([(pvar, typ)], sil_loc); Sil.Set (Sil.Lvar pvar, typ, e'', sil_loc)] in let all_res_trans = [res_trans_b; tmp_var_res_trans] in
let nodes_branch = (match node_b, is_join_node join_node with let res_trans = PriorityNode.compute_results_to_parent trans_state'' sil_loc
| [], _ -> 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 "ConditinalStmt Branch" stmt_info all_res_trans 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 prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node prune_nodes 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 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 (match stmt_list with
| [cond; exp1; exp2] -> | [cond; exp1; exp2] ->
let typ = let typ =
CTypes_decl.type_ptr_to_sil_type context.CContext.tenv expr_info.Clang_ast_t.ei_type_ptr in 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 pvar = mk_temp_var (Cfg.Node.get_id join_node) in
let continuation' = mk_cond_continuation trans_state.continuation 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 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 | Loops.While (decl_stmt_opt, _, _) -> decl_stmt_opt
| _ -> None in | _ -> None in
let res_trans_decl = match decl_stmt_opt with 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 | _ -> res_trans_cond in
let body_succ_nodes = let body_succ_nodes =
match loop_kind with match loop_kind with

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

@ -200,6 +200,10 @@ struct
Printing.log_out "Priority busy in %s. No claim possible\n@." stmt_info.Clang_ast_t.si_pointer; Printing.log_out "Priority busy in %s. No claim possible\n@." stmt_info.Clang_ast_t.si_pointer;
trans_state 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 = let is_priority_free trans_state =
match trans_state.priority with match trans_state.priority with
| Free -> true | Free -> true
@ -222,7 +226,7 @@ struct
(* Invariant: if leaf_nodes is empty then the params have not created a node.*) (* 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 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 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 *) | _, false -> (* The node is created by the parent. We just pass back nodes/leafs params *)
{ res_state_param with exps = []} { res_state_param with exps = []}
| [], true -> (* We need to create a node and params did not create a node.*) | [], 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 Nodes.create_node (Cfg.Node.Stmt_node "Assertion failure") [] [call_instr] sil_loc context in
Cfg.Node.set_succs_exn failure_node [exit_node] []; Cfg.Node.set_succs_exn failure_node [exit_node] [];
{ root_nodes = [failure_node]; { root_nodes = [failure_node];
leaf_nodes = [failure_node]; leaf_nodes = [];
ids = []; ids = [];
instrs =[]; instrs =[];
exps = [] } exps = [] }

2
infer/src/clang/cTrans_utils.mli
Unescape View File

@ -152,6 +152,8 @@ sig
val try_claim_priority_node : trans_state -> Clang_ast_t.stmt_info -> trans_state 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 val own_priority_node : t -> Clang_ast_t.stmt_info -> bool
(* Used by translation functions to handle potenatial cfg nodes. *) (* Used by translation functions to handle potenatial cfg nodes. *)

164
infer/tests/codetoanalyze/c/frontend/conditional_operator/cond2.c.dot
Unescape View File

@ -1,172 +1,176 @@
digraph iCFG { 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 ; 58 -> 42 ;
57 -> 42 ; 58 -> 43 ;
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"] 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 ; 57 -> 52 ;
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"] 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 ; 56 -> 52 ;
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"] 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 ; 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 ; 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 -> 58 ;
52 -> 54 ; 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 [label="51: + \n " ]
51 -> 57 ; 51 -> 39 ;
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"] 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 ; 50 -> 40 ;
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"] 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 ; 49 -> 40 ;
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"] 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 ; 48 -> 50 ;
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"] 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 ; 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 ; 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 -> 41 ;
45 -> 47 ; 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 [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"]
44 -> 40 ; 44 -> 41 ;
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"] 43 [label="43: Prune (false branch) \n PRUNE(((3 > 4) == 0), false); [line 24]\n " shape="invhouse"]
43 -> 40 ; 43 -> 45 ;
42 [label="42: Prune (false branch) \n PRUNE(((3 > 4) == 0), false); [line 24]\n " shape="invhouse"] 42 [label="42: Prune (true branch) \n PRUNE(((3 > 4) != 0), true); [line 24]\n " shape="invhouse"]
42 -> 44 ; 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 [label="40: + \n " ]
40 -> 45 ; 40 -> 51 ;
39 [label="39: + \n " ] 39 [label="39: Exit bar \n " color=yellow style=filled]
39 -> 50 ; 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]
38 [label="38: Exit bar \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 ; 37 -> 31 ;
36 [label="36: DeclStmt \n *&x:int =5 [line 12]\n " shape="box"] 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 -> 30 ;
36 -> 31 ; 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 [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 -> 29 ; 35 -> 30 ;
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"] 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 ; 34 -> 36 ;
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"] 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 ; 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 -> 33 ;
32 -> 34 ; 31 [label="31: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"]
31 [label="31: Prune (false branch) \n PRUNE(((3 < 4) == 0), false); [line 13]\n " shape="invhouse"]
31 -> 32 ; 31 -> 36 ;
30 [label="30: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 13]\n APPLY_ABSTRACTION; [line 13]\n " shape="invhouse"] 30 [label="30: + \n " ]
30 -> 35 ; 30 -> 29 ;
29 [label="29: + \n " ] 29 [label="29: DeclStmt \n *&y:int =19 [line 14]\n " shape="box"]
29 -> 28 ; 29 -> 21 ;
28 [label="28: DeclStmt \n *&y:int =19 [line 14]\n " shape="box"] 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 -> 10 ;
28 -> 21 ; 28 -> 11 ;
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"] 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 -> 20 ;
27 -> 11 ; 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 [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"]
26 -> 19 ; 26 -> 20 ;
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"] 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 ; 25 -> 27 ;
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"] 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 ; 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 ; 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 -> 23 ;
22 -> 24 ; 21 [label="21: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="invhouse"]
21 [label="21: Prune (false branch) \n PRUNE(((3 < 4) == 0), false); [line 15]\n " shape="invhouse"]
21 -> 22 ; 21 -> 26 ;
20 [label="20: Prune (true branch) \n PRUNE(((3 < 4) != 0), true); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="invhouse"] 20 [label="20: + \n " ]
20 -> 25 ; 20 -> 28 ;
19 [label="19: + \n " ] 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 ; 19 -> 4 ;
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 -> 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 -> 9 ;
18 -> 5 ;
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"] 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 ; 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"] 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 [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"] 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 [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 ;
} }

2
infer/tests/codetoanalyze/c/frontend/conditional_operator/conditional_operator.c.dot
Unescape View File

@ -7,7 +7,7 @@ digraph iCFG {
53 -> 49 ; 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 ; 52 -> 49 ;

2
infer/tests/codetoanalyze/c/frontend/conditional_operator/member_access.c.dot
Unescape View File

@ -7,7 +7,7 @@ digraph iCFG {
23 -> 19 ; 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 ; 22 -> 19 ;

12
infer/tests/codetoanalyze/objc/frontend/assertions/NSAssert_example.dot
Unescape View File

@ -8,7 +8,7 @@ digraph iCFG {
107 -> 101 ; 107 -> 101 ;
106 [label="106: Message Call: stringWithUTF8String: \n n$17=_fun_NSString_stringWithUTF8String:(\"<Unknown Function>\":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:(\"<Unknown Function>\":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 ; 106 -> 102 ;
@ -37,7 +37,7 @@ digraph iCFG {
100 -> 94 ; 100 -> 94 ;
99 [label="99: Message Call: stringWithUTF8String: \n n$11=_fun_NSString_stringWithUTF8String:(\"<Unknown File>\":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:(\"<Unknown File>\":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 ; 99 -> 95 ;
@ -128,7 +128,7 @@ digraph iCFG {
78 -> 72 ; 78 -> 72 ;
77 [label="77: Message Call: stringWithUTF8String: \n n$16=_fun_NSString_stringWithUTF8String:(\"<Unknown Function>\":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:(\"<Unknown Function>\":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 ; 77 -> 73 ;
@ -157,7 +157,7 @@ digraph iCFG {
71 -> 65 ; 71 -> 65 ;
70 [label="70: Message Call: stringWithUTF8String: \n n$10=_fun_NSString_stringWithUTF8String:(\"<Unknown File>\":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:(\"<Unknown File>\":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 ; 70 -> 66 ;
@ -263,7 +263,7 @@ digraph iCFG {
45 -> 39 ; 45 -> 39 ;
44 [label="44: Message Call: stringWithUTF8String: \n n$26=_fun_NSString_stringWithUTF8String:(\"<Unknown File>\":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:(\"<Unknown File>\":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 ; 44 -> 40 ;
@ -358,7 +358,7 @@ digraph iCFG {
22 -> 16 ; 22 -> 16 ;
21 [label="21: Message Call: stringWithUTF8String: \n n$11=_fun_NSString_stringWithUTF8String:(\"<Unknown File>\":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:(\"<Unknown File>\":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 ; 21 -> 17 ;

Write Preview
Loading…
Cancel
Save