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

Handle variable declaration inside condition expression correctly

Browse Source 
Summary: public
C++ allows to have one variable declared+initialized as a condition statement.
Handle these cases properly for `if` and `while` statements.

Reviewed By: dulmarod

Differential Revision: D2625774

fb-gh-sync-id: bac95b8
master
Andrzej Kotulski 9 years ago committed by facebook-github-bot-1
parent 0db83eb5dd
commit db35afef1e
11 changed files with 765 additions and 22 deletions
Show Stats Download Patch File Download Diff File

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

@ -1053,6 +1053,15 @@ struct
cond_trans trans_state s
| _ -> no_short_circuit_cond ()
and declStmt_in_condition_trans trans_state decl_stmt res_trans_cond =
match decl_stmt with
| Clang_ast_t.DeclStmt(stmt_info, stmt_list, decl_list) ->
let trans_state_decl = { trans_state with
succ_nodes = res_trans_cond.root_nodes
} in
declStmt_trans trans_state_decl decl_list stmt_info
| _ -> res_trans_cond
and ifStmt_trans trans_state stmt_info stmt_list =
let context = trans_state.context in
let pln = trans_state.parent_line_number in
@ -1073,15 +1082,26 @@ struct
IList.iter (fun n -> Cfg.Node.set_succs_exn n nodes_branch []) prune_nodes';
res_trans_b.ids in
(match stmt_list with
| [null_stmt; cond; stmt1; stmt2] -> (* Note: for the moment we don't do anything with the null_stmt/decl*)
| [decl_stmt; cond; stmt1; stmt2] ->
(* set the flat to inform that we are translating a condition of a if *)
let continuation' = mk_cond_continuation trans_state.continuation in
let trans_state'' = { trans_state with continuation = continuation'; succ_nodes = []; parent_line_number = line_number } in
let trans_state'' = { trans_state with
continuation = continuation';
succ_nodes = [];
parent_line_number = line_number
} in
let res_trans_cond = cond_trans trans_state'' cond in
let res_trans_decl = declStmt_in_condition_trans trans_state decl_stmt res_trans_cond in
(* Note: by contruction prune nodes are leafs_nodes_cond *)
let ids_t = do_branch true stmt1 res_trans_cond.leaf_nodes in
let ids_f = do_branch false stmt2 res_trans_cond.leaf_nodes in
{ root_nodes = res_trans_cond.root_nodes; leaf_nodes =[join_node]; ids = res_trans_cond.ids@ids_t@ids_f; instrs =[]; exps =[] }
{
root_nodes = res_trans_decl.root_nodes;
leaf_nodes = [join_node];
ids = res_trans_decl.ids @ res_trans_cond.ids @ ids_t @ ids_f;
instrs = [];
exps = []
}
| _ -> assert false)
(* Assumption: the CompoundStmt can be made of different stmts, not just CaseStmts *)
@ -1240,7 +1260,7 @@ struct
let continuation_cond = mk_cond_continuation outer_continuation in
let init_incr_nodes =
match loop_kind with
| Loops.For (init, cond, incr, body) ->
| Loops.For (init, decl_stmt, cond, incr, body) ->
let trans_state' = {
trans_state with
succ_nodes = [join_node];
@ -1260,6 +1280,13 @@ struct
succ_nodes = [];
} in
let res_trans_cond = cond_trans trans_state_cond cond_stmt in
let decl_stmt_opt = match loop_kind with
| Loops.For (_, decl_stmt, _, _, _) -> Some decl_stmt
| 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
| _ -> res_trans_cond in
let body_succ_nodes =
match loop_kind with
| Loops.For _ -> (match init_incr_nodes with
@ -1280,7 +1307,7 @@ struct
instruction trans_state_body (Loops.get_body loop_kind) in
let join_succ_nodes =
match loop_kind with
| Loops.For _ | Loops.While _ -> res_trans_cond.root_nodes
| Loops.For _ | Loops.While _ -> res_trans_decl.root_nodes
| Loops.DoWhile _ -> res_trans_body.root_nodes in
(* Note: prune nodes are by contruction the res_trans_cond.leaf_nodes *)
let prune_nodes_t, prune_nodes_f = IList.partition is_true_prune_node res_trans_cond.leaf_nodes in
@ -1298,12 +1325,12 @@ struct
| Loops.While _ | Loops.DoWhile _ -> [join_node] in
{ empty_res_trans with root_nodes = root_nodes; leaf_nodes = prune_nodes_f }
and forStmt_trans trans_state init cond incr body stmt_info =
let for_kind = Loops.For (init, cond, incr, body) in
and forStmt_trans trans_state init decl_stmt cond incr body stmt_info =
let for_kind = Loops.For (init, decl_stmt, cond, incr, body) in
loop_instruction trans_state for_kind stmt_info
and whileStmt_trans trans_state cond body stmt_info =
let while_kind = Loops.While (cond, body) in
and whileStmt_trans trans_state decl_stmt cond body stmt_info =
let while_kind = Loops.While (Some decl_stmt, cond, body) in
loop_instruction trans_state while_kind stmt_info
and doStmt_trans trans_state stmt_info cond body =
@ -1315,7 +1342,7 @@ struct
(* Here we do ast transformation, so we don't need the value of the translation of the *)
(* variable item but we still need to add the variable to the locals *)
let bin_op = Ast_expressions.make_next_object_exp stmt_info item items in
let while_kind = Loops.While (bin_op, body) in
let while_kind = Loops.While (None, bin_op, body) in
loop_instruction trans_state while_kind stmt_info
(* Assumption: We expect precisely 2 stmt corresponding to the 2 operands. *)
@ -1941,12 +1968,12 @@ struct
| StmtExpr(stmt_info, stmt_list, expr_info) ->
stmtExpr_trans trans_state stmt_info stmt_list expr_info
| ForStmt(stmt_info, [init; null_stmt; cond; incr; body]) ->
| ForStmt(stmt_info, [init; decl_stmt; cond; incr; body]) ->
(* Note: we ignore null_stmt at the moment.*)
forStmt_trans trans_state init cond incr body stmt_info
forStmt_trans trans_state init decl_stmt cond incr body stmt_info
| WhileStmt(stmt_info, [_; cond; body]) -> (* Note: we ignore null_stmt at the moment.*)
whileStmt_trans trans_state cond body stmt_info
| WhileStmt(stmt_info, [decl_stmt; cond; body]) ->
whileStmt_trans trans_state decl_stmt cond body stmt_info
| DoStmt(stmt_info, [body; cond]) ->
doStmt_trans trans_state stmt_info cond body

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

@ -250,9 +250,10 @@ module Loops =
struct
type loop_kind =
| For of Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt
(* init, condition, increment and body *)
| While of Clang_ast_t.stmt * Clang_ast_t.stmt (* condition and body *)
| For of Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt
(* init, decl_stmt, condition, increment and body *)
| While of Clang_ast_t.stmt option * Clang_ast_t.stmt * Clang_ast_t.stmt
(* decl_stmt, condition and body *)
| DoWhile of Clang_ast_t.stmt * Clang_ast_t.stmt (* condition and body *)
let loop_kind_to_if_kind loop_kind =
@ -263,11 +264,11 @@ struct
let get_body loop_kind =
match loop_kind with
| For (_, _, _, body) | While (_, body) | DoWhile (_, body) -> body
| For (_, _, _, _, body) | While (_, _, body) | DoWhile (_, body) -> body
let get_cond loop_kind =
match loop_kind with
| For (_, cond, _, _) | While (cond, _) | DoWhile (cond, _) -> cond
| For (_, _, cond, _, _) | While (_, cond, _) | DoWhile (cond, _) -> cond
end
(** This function handles ObjC new/alloc and C++ new calls *)

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

@ -183,9 +183,10 @@ end
module Loops :
sig
type loop_kind =
| For of Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt
(* init, condition, increment and body *)
| While of Clang_ast_t.stmt * Clang_ast_t.stmt (* condition and body *)
| For of Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt * Clang_ast_t.stmt
(* init, decl_stmt, condition, increment and body *)
| While of Clang_ast_t.stmt option * Clang_ast_t.stmt * Clang_ast_t.stmt
(* decl_stmt, condition and body *)
| DoWhile of Clang_ast_t.stmt * Clang_ast_t.stmt (* condition and body *)
val loop_kind_to_if_kind : loop_kind -> Sil.if_kind

22
infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_for.cpp
Unescape View File

@ -0,0 +1,22 @@
/*
* Copyright (c) 2015 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
int simple_init() {
int result = 0;
for (int i = 0; int x = 2; i++) {
result += x;
}
}
int init_with_scoped_var() {
int result = 0;
for (int i = 10; int x = i; i--) {
result += x;
}
}

82
infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_for.cpp.dot
Unescape View File

@ -0,0 +1,82 @@
digraph iCFG {
20 [label="20: DeclStmt \n *&result:int =0 [line 18]\n " shape="box"]
20 -> 14 ;
19 [label="19: ComppoundAssignStmt \n n$3=*&x:int [line 20]\n n$4=*&result:int [line 20]\n *&result:int =(n$4 + n$3) [line 20]\n REMOVE_TEMPS(n$3,n$4); [line 20]\n NULLIFY(&x,false); [line 20]\n " shape="box"]
19 -> 15 ;
18 [label="18: DeclStmt \n n$2=*&i:int [line 19]\n *&x:int =n$2 [line 19]\n REMOVE_TEMPS(n$2); [line 19]\n " shape="box"]
18 -> 16 ;
18 -> 17 ;
17 [label="17: Prune (false branch) \n n$1=*&x:int [line 19]\n PRUNE((n$1 == 0), false); [line 19]\n REMOVE_TEMPS(n$1); [line 19]\n NULLIFY(&i,false); [line 19]\n NULLIFY(&result,false); [line 19]\n NULLIFY(&x,false); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="invhouse"]
17 -> 12 ;
16 [label="16: Prune (true branch) \n n$1=*&x:int [line 19]\n PRUNE((n$1 != 0), true); [line 19]\n REMOVE_TEMPS(n$1); [line 19]\n " shape="invhouse"]
16 -> 19 ;
15 [label="15: UnaryOperator \n n$0=*&i:int [line 19]\n *&i:int =(n$0 - 1) [line 19]\n REMOVE_TEMPS(n$0); [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"]
15 -> 13 ;
14 [label="14: DeclStmt \n *&i:int =10 [line 19]\n APPLY_ABSTRACTION; [line 19]\n " shape="box"]
14 -> 13 ;
13 [label="13: + \n " ]
13 -> 18 ;
12 [label="12: Exit init_with_scoped_var \n " color=yellow style=filled]
11 [label="11: Start init_with_scoped_var\nFormals: \nLocals: i:int x:int result:int \n DECLARE_LOCALS(&return,&i,&x,&result); [line 17]\n NULLIFY(&i,false); [line 17]\n NULLIFY(&result,false); [line 17]\n NULLIFY(&x,false); [line 17]\n " color=yellow style=filled]
11 -> 20 ;
10 [label="10: DeclStmt \n *&result:int =0 [line 11]\n " shape="box"]
10 -> 4 ;
9 [label="9: ComppoundAssignStmt \n n$2=*&x:int [line 13]\n n$3=*&result:int [line 13]\n *&result:int =(n$3 + n$2) [line 13]\n REMOVE_TEMPS(n$2,n$3); [line 13]\n NULLIFY(&x,false); [line 13]\n " shape="box"]
9 -> 5 ;
8 [label="8: DeclStmt \n *&x:int =2 [line 12]\n " shape="box"]
8 -> 6 ;
8 -> 7 ;
7 [label="7: Prune (false branch) \n n$1=*&x:int [line 12]\n PRUNE((n$1 == 0), false); [line 12]\n REMOVE_TEMPS(n$1); [line 12]\n NULLIFY(&i,false); [line 12]\n NULLIFY(&result,false); [line 12]\n NULLIFY(&x,false); [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="invhouse"]
7 -> 2 ;
6 [label="6: Prune (true branch) \n n$1=*&x:int [line 12]\n PRUNE((n$1 != 0), true); [line 12]\n REMOVE_TEMPS(n$1); [line 12]\n " shape="invhouse"]
6 -> 9 ;
5 [label="5: UnaryOperator \n n$0=*&i:int [line 12]\n *&i:int =(n$0 + 1) [line 12]\n REMOVE_TEMPS(n$0); [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"]
5 -> 3 ;
4 [label="4: DeclStmt \n *&i:int =0 [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"]
4 -> 3 ;
3 [label="3: + \n " ]
3 -> 8 ;
2 [label="2: Exit simple_init \n " color=yellow style=filled]
1 [label="1: Start simple_init\nFormals: \nLocals: i:int x:int result:int \n DECLARE_LOCALS(&return,&i,&x,&result); [line 10]\n NULLIFY(&i,false); [line 10]\n NULLIFY(&result,false); [line 10]\n NULLIFY(&x,false); [line 10]\n " color=yellow style=filled]
1 -> 10 ;
}

64
infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_if.cpp
Unescape View File

@ -0,0 +1,64 @@
/*
* Copyright (c) 2015 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
int simple_init_div1() {
if (int a = 1) {
return 1/a;
}
}
int simple_init_div0() {
if (int a = 0) {
return a;
} else {
return 1/a;
}
}
int simple_inif_elseif_div0() {
if (int a = 0) {
return 1;
} else if (int b = 0) {
return 1;
} else {
return 1 / (a + b);
}
}
int get1() {
return 1;
}
int function_call_init_div0() {
if (int a = get1()) {
return 1 / (a - 1);
}
}
int conditional_init_div0() {
if (int a = 1 ? 1 : 0) {
return 1 / (a - 1);
}
}
int reference_init_div0() {
int r = 1;
if (int& a = r) {
a = 0;
}
return 1/r;
}
int simple_init_null_deref() {
if (int *p = nullptr) {
return 1;
} else {
return *p;
}
}

271
infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_if.cpp.dot
Unescape View File

@ -0,0 +1,271 @@
digraph iCFG {
67 [label="67: Return Stmt \n n$1=*&p:int * [line 62]\n n$2=*n$1:int [line 62]\n *&return:int =n$2 [line 62]\n REMOVE_TEMPS(n$1,n$2); [line 62]\n NULLIFY(&p,false); [line 62]\n APPLY_ABSTRACTION; [line 62]\n " shape="box"]
67 -> 61 ;
66 [label="66: Return Stmt \n NULLIFY(&p,false); [line 60]\n *&return:int =1 [line 60]\n APPLY_ABSTRACTION; [line 60]\n " shape="box"]
66 -> 61 ;
65 [label="65: DeclStmt \n *&p:int *=null [line 59]\n " shape="box"]
65 -> 63 ;
65 -> 64 ;
64 [label="64: Prune (false branch) \n n$0=*&p:int * [line 59]\n PRUNE((n$0 == 0), false); [line 59]\n REMOVE_TEMPS(n$0); [line 59]\n " shape="invhouse"]
64 -> 67 ;
63 [label="63: Prune (true branch) \n n$0=*&p:int * [line 59]\n PRUNE((n$0 != 0), true); [line 59]\n REMOVE_TEMPS(n$0); [line 59]\n " shape="invhouse"]
63 -> 66 ;
62 [label="62: + \n NULLIFY(&p,false); [line 59]\n " ]
62 -> 61 ;
61 [label="61: Exit simple_init_null_deref \n " color=yellow style=filled]
60 [label="60: Start simple_init_null_deref\nFormals: \nLocals: p:int * \n DECLARE_LOCALS(&return,&p); [line 58]\n NULLIFY(&p,false); [line 58]\n " color=yellow style=filled]
60 -> 65 ;
59 [label="59: DeclStmt \n *&r:int =1 [line 51]\n " shape="box"]
59 -> 57 ;
58 [label="58: BinaryOperatorStmt: Assign \n n$3=*&a:int & [line 53]\n *n$3:int =0 [line 53]\n REMOVE_TEMPS(n$3); [line 53]\n NULLIFY(&a,false); [line 53]\n APPLY_ABSTRACTION; [line 53]\n " shape="box"]
58 -> 54 ;
57 [label="57: DeclStmt \n *&a:int &=&r [line 52]\n " shape="box"]
57 -> 55 ;
57 -> 56 ;
56 [label="56: Prune (false branch) \n n$1=*&a:int & [line 52]\n n$2=*n$1:int [line 52]\n PRUNE((n$2 == 0), false); [line 52]\n REMOVE_TEMPS(n$1,n$2); [line 52]\n APPLY_ABSTRACTION; [line 52]\n " shape="invhouse"]
56 -> 54 ;
55 [label="55: Prune (true branch) \n n$1=*&a:int & [line 52]\n n$2=*n$1:int [line 52]\n PRUNE((n$2 != 0), true); [line 52]\n REMOVE_TEMPS(n$1,n$2); [line 52]\n " shape="invhouse"]
55 -> 58 ;
54 [label="54: + \n " ]
54 -> 53 ;
53 [label="53: Return Stmt \n NULLIFY(&a,false); [line 55]\n n$0=*&r:int [line 55]\n *&return:int =(1 / n$0) [line 55]\n REMOVE_TEMPS(n$0); [line 55]\n NULLIFY(&r,false); [line 55]\n APPLY_ABSTRACTION; [line 55]\n " shape="box"]
53 -> 52 ;
52 [label="52: Exit reference_init_div0 \n " color=yellow style=filled]
51 [label="51: Start reference_init_div0\nFormals: \nLocals: a:int & r:int \n DECLARE_LOCALS(&return,&a,&r); [line 50]\n NULLIFY(&a,false); [line 50]\n " color=yellow style=filled]
51 -> 59 ;
50 [label="50: Return Stmt \n n$2=*&a:int [line 46]\n *&return:int =(1 / (n$2 - 1)) [line 46]\n REMOVE_TEMPS(n$2); [line 46]\n NULLIFY(&a,false); [line 46]\n APPLY_ABSTRACTION; [line 46]\n " shape="box"]
50 -> 40 ;
49 [label="49: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___45); [line 45]\n *&SIL_temp_conditional___45:int =0 [line 45]\n APPLY_ABSTRACTION; [line 45]\n " shape="box"]
49 -> 45 ;
48 [label="48: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___45); [line 45]\n *&SIL_temp_conditional___45:int =1 [line 45]\n APPLY_ABSTRACTION; [line 45]\n " shape="box"]
48 -> 45 ;
47 [label="47: Prune (false branch) \n PRUNE((1 == 0), false); [line 45]\n " shape="invhouse"]
47 -> 49 ;
46 [label="46: Prune (true branch) \n PRUNE((1 != 0), true); [line 45]\n " shape="invhouse"]
46 -> 48 ;
45 [label="45: + \n " ]
45 -> 44 ;
44 [label="44: DeclStmt \n n$1=*&SIL_temp_conditional___45:int [line 45]\n NULLIFY(&SIL_temp_conditional___45,true); [line 45]\n *&a:int =n$1 [line 45]\n REMOVE_TEMPS(n$1); [line 45]\n " shape="box"]
44 -> 42 ;
44 -> 43 ;
43 [label="43: Prune (false branch) \n n$0=*&a:int [line 45]\n PRUNE((n$0 == 0), false); [line 45]\n REMOVE_TEMPS(n$0); [line 45]\n " shape="invhouse"]
43 -> 41 ;
42 [label="42: Prune (true branch) \n n$0=*&a:int [line 45]\n PRUNE((n$0 != 0), true); [line 45]\n REMOVE_TEMPS(n$0); [line 45]\n " shape="invhouse"]
42 -> 50 ;
41 [label="41: + \n NULLIFY(&a,false); [line 45]\n " ]
41 -> 40 ;
40 [label="40: Exit conditional_init_div0 \n " color=yellow style=filled]
39 [label="39: Start conditional_init_div0\nFormals: \nLocals: a:int \n DECLARE_LOCALS(&return,&a); [line 44]\n NULLIFY(&a,false); [line 44]\n " color=yellow style=filled]
39 -> 46 ;
39 -> 47 ;
38 [label="38: Return Stmt \n n$2=*&a:int [line 40]\n *&return:int =(1 / (n$2 - 1)) [line 40]\n REMOVE_TEMPS(n$2); [line 40]\n NULLIFY(&a,false); [line 40]\n APPLY_ABSTRACTION; [line 40]\n " shape="box"]
38 -> 33 ;
37 [label="37: DeclStmt \n n$1=_fun_get1() [line 39]\n *&a:int =n$1 [line 39]\n REMOVE_TEMPS(n$1); [line 39]\n " shape="box"]
37 -> 35 ;
37 -> 36 ;
36 [label="36: Prune (false branch) \n n$0=*&a:int [line 39]\n PRUNE((n$0 == 0), false); [line 39]\n REMOVE_TEMPS(n$0); [line 39]\n " shape="invhouse"]
36 -> 34 ;
35 [label="35: Prune (true branch) \n n$0=*&a:int [line 39]\n PRUNE((n$0 != 0), true); [line 39]\n REMOVE_TEMPS(n$0); [line 39]\n " shape="invhouse"]
35 -> 38 ;
34 [label="34: + \n NULLIFY(&a,false); [line 39]\n " ]
34 -> 33 ;
33 [label="33: Exit function_call_init_div0 \n " color=yellow style=filled]
32 [label="32: Start function_call_init_div0\nFormals: \nLocals: a:int \n DECLARE_LOCALS(&return,&a); [line 38]\n NULLIFY(&a,false); [line 38]\n " color=yellow style=filled]
32 -> 37 ;
31 [label="31: Return Stmt \n *&return:int =1 [line 35]\n APPLY_ABSTRACTION; [line 35]\n " shape="box"]
31 -> 30 ;
30 [label="30: Exit get1 \n " color=yellow style=filled]
29 [label="29: Start get1\nFormals: \nLocals: \n DECLARE_LOCALS(&return); [line 34]\n " color=yellow style=filled]
29 -> 31 ;
28 [label="28: Return Stmt \n n$2=*&a:int [line 30]\n n$3=*&b:int [line 30]\n *&return:int =(1 / (n$2 + n$3)) [line 30]\n REMOVE_TEMPS(n$2,n$3); [line 30]\n NULLIFY(&a,false); [line 30]\n NULLIFY(&b,false); [line 30]\n APPLY_ABSTRACTION; [line 30]\n " shape="box"]
28 -> 17 ;
27 [label="27: Return Stmt \n NULLIFY(&a,false); [line 28]\n NULLIFY(&b,false); [line 28]\n *&return:int =1 [line 28]\n APPLY_ABSTRACTION; [line 28]\n " shape="box"]
27 -> 17 ;
26 [label="26: DeclStmt \n *&b:int =0 [line 27]\n " shape="box"]
26 -> 24 ;
26 -> 25 ;
25 [label="25: Prune (false branch) \n n$1=*&b:int [line 27]\n PRUNE((n$1 == 0), false); [line 27]\n REMOVE_TEMPS(n$1); [line 27]\n " shape="invhouse"]
25 -> 28 ;
24 [label="24: Prune (true branch) \n n$1=*&b:int [line 27]\n PRUNE((n$1 != 0), true); [line 27]\n REMOVE_TEMPS(n$1); [line 27]\n " shape="invhouse"]
24 -> 27 ;
23 [label="23: + \n " ]
23 -> 18 ;
22 [label="22: Return Stmt \n NULLIFY(&a,false); [line 26]\n *&return:int =1 [line 26]\n APPLY_ABSTRACTION; [line 26]\n " shape="box"]
22 -> 17 ;
21 [label="21: DeclStmt \n *&a:int =0 [line 25]\n " shape="box"]
21 -> 19 ;
21 -> 20 ;
20 [label="20: Prune (false branch) \n n$0=*&a:int [line 25]\n PRUNE((n$0 == 0), false); [line 25]\n REMOVE_TEMPS(n$0); [line 25]\n " shape="invhouse"]
20 -> 26 ;
19 [label="19: Prune (true branch) \n n$0=*&a:int [line 25]\n PRUNE((n$0 != 0), true); [line 25]\n REMOVE_TEMPS(n$0); [line 25]\n " shape="invhouse"]
19 -> 22 ;
18 [label="18: + \n NULLIFY(&a,false); [line 25]\n NULLIFY(&b,false); [line 25]\n " ]
18 -> 17 ;
17 [label="17: Exit simple_inif_elseif_div0 \n " color=yellow style=filled]
16 [label="16: Start simple_inif_elseif_div0\nFormals: \nLocals: a:int b:int \n DECLARE_LOCALS(&return,&a,&b); [line 24]\n NULLIFY(&a,false); [line 24]\n NULLIFY(&b,false); [line 24]\n " color=yellow style=filled]
16 -> 21 ;
15 [label="15: Return Stmt \n n$2=*&a:int [line 20]\n *&return:int =(1 / n$2) [line 20]\n REMOVE_TEMPS(n$2); [line 20]\n NULLIFY(&a,false); [line 20]\n APPLY_ABSTRACTION; [line 20]\n " shape="box"]
15 -> 9 ;
14 [label="14: Return Stmt \n n$1=*&a:int [line 18]\n *&return:int =n$1 [line 18]\n REMOVE_TEMPS(n$1); [line 18]\n NULLIFY(&a,false); [line 18]\n APPLY_ABSTRACTION; [line 18]\n " shape="box"]
14 -> 9 ;
13 [label="13: DeclStmt \n *&a:int =0 [line 17]\n " shape="box"]
13 -> 11 ;
13 -> 12 ;
12 [label="12: Prune (false branch) \n n$0=*&a:int [line 17]\n PRUNE((n$0 == 0), false); [line 17]\n REMOVE_TEMPS(n$0); [line 17]\n " shape="invhouse"]
12 -> 15 ;
11 [label="11: Prune (true branch) \n n$0=*&a:int [line 17]\n PRUNE((n$0 != 0), true); [line 17]\n REMOVE_TEMPS(n$0); [line 17]\n " shape="invhouse"]
11 -> 14 ;
10 [label="10: + \n NULLIFY(&a,false); [line 17]\n " ]
10 -> 9 ;
9 [label="9: Exit simple_init_div0 \n " color=yellow style=filled]
8 [label="8: Start simple_init_div0\nFormals: \nLocals: a:int \n DECLARE_LOCALS(&return,&a); [line 16]\n NULLIFY(&a,false); [line 16]\n " color=yellow style=filled]
8 -> 13 ;
7 [label="7: Return Stmt \n n$1=*&a:int [line 12]\n *&return:int =(1 / n$1) [line 12]\n REMOVE_TEMPS(n$1); [line 12]\n NULLIFY(&a,false); [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"]
7 -> 2 ;
6 [label="6: DeclStmt \n *&a:int =1 [line 11]\n " shape="box"]
6 -> 4 ;
6 -> 5 ;
5 [label="5: Prune (false branch) \n n$0=*&a:int [line 11]\n PRUNE((n$0 == 0), false); [line 11]\n REMOVE_TEMPS(n$0); [line 11]\n " shape="invhouse"]
5 -> 3 ;
4 [label="4: Prune (true branch) \n n$0=*&a:int [line 11]\n PRUNE((n$0 != 0), true); [line 11]\n REMOVE_TEMPS(n$0); [line 11]\n " shape="invhouse"]
4 -> 7 ;
3 [label="3: + \n NULLIFY(&a,false); [line 11]\n " ]
3 -> 2 ;
2 [label="2: Exit simple_init_div1 \n " color=yellow style=filled]
1 [label="1: Start simple_init_div1\nFormals: \nLocals: a:int \n DECLARE_LOCALS(&return,&a); [line 10]\n NULLIFY(&a,false); [line 10]\n " color=yellow style=filled]
1 -> 6 ;
}

28
infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_while.cpp
Unescape View File

@ -0,0 +1,28 @@
/*
* Copyright (c) 2015 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
int simple_assignment() {
int x = 10;
int result = 0;
while(int a = x) {
result += a;
x -= 1;
}
return 0;
}
int conditional_assignment() {
int x = 10;
int result = 0;
while(int a = x > 0 ? x : 0) {
result += a;
x -= 1;
}
return 0;
}

115
infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_while.cpp.dot
Unescape View File

@ -0,0 +1,115 @@
digraph iCFG {
28 [label="28: DeclStmt \n *&x:int =10 [line 21]\n " shape="box"]
28 -> 27 ;
27 [label="27: DeclStmt \n *&result:int =0 [line 22]\n APPLY_ABSTRACTION; [line 22]\n " shape="box"]
27 -> 15 ;
26 [label="26: ComppoundAssignStmt \n n$5=*&a:int [line 24]\n n$6=*&result:int [line 24]\n *&result:int =(n$6 + n$5) [line 24]\n REMOVE_TEMPS(n$5,n$6); [line 24]\n NULLIFY(&a,false); [line 24]\n " shape="box"]
26 -> 25 ;
25 [label="25: ComppoundAssignStmt \n n$4=*&x:int [line 25]\n *&x:int =(n$4 - 1) [line 25]\n REMOVE_TEMPS(n$4); [line 25]\n APPLY_ABSTRACTION; [line 25]\n " shape="box"]
25 -> 15 ;
24 [label="24: ConditinalStmt Branch \n DECLARE_LOCALS(&SIL_temp_conditional___19); [line 23]\n *&SIL_temp_conditional___19:int =0 [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"]
24 -> 19 ;
23 [label="23: ConditinalStmt Branch \n n$2=*&x:int [line 23]\n DECLARE_LOCALS(&SIL_temp_conditional___19); [line 23]\n *&SIL_temp_conditional___19:int =n$2 [line 23]\n REMOVE_TEMPS(n$2); [line 23]\n APPLY_ABSTRACTION; [line 23]\n " shape="box"]
23 -> 19 ;
22 [label="22: Prune (false branch) \n PRUNE(((n$1 > 0) == 0), false); [line 23]\n REMOVE_TEMPS(n$1); [line 23]\n " shape="invhouse"]
22 -> 24 ;
21 [label="21: Prune (true branch) \n PRUNE(((n$1 > 0) != 0), true); [line 23]\n REMOVE_TEMPS(n$1); [line 23]\n " shape="invhouse"]
21 -> 23 ;
20 [label="20: BinaryOperatorStmt: GT \n n$1=*&x:int [line 23]\n " shape="box"]
20 -> 21 ;
20 -> 22 ;
19 [label="19: + \n " ]
19 -> 18 ;
18 [label="18: DeclStmt \n n$3=*&SIL_temp_conditional___19:int [line 23]\n NULLIFY(&SIL_temp_conditional___19,true); [line 23]\n *&a:int =n$3 [line 23]\n REMOVE_TEMPS(n$3); [line 23]\n " shape="box"]
18 -> 16 ;
18 -> 17 ;
17 [label="17: Prune (false branch) \n n$0=*&a:int [line 23]\n PRUNE((n$0 == 0), false); [line 23]\n REMOVE_TEMPS(n$0); [line 23]\n " shape="invhouse"]
17 -> 14 ;
16 [label="16: Prune (true branch) \n n$0=*&a:int [line 23]\n PRUNE((n$0 != 0), true); [line 23]\n REMOVE_TEMPS(n$0); [line 23]\n " shape="invhouse"]
16 -> 26 ;
15 [label="15: + \n " ]
15 -> 20 ;
14 [label="14: Return Stmt \n NULLIFY(&a,false); [line 27]\n NULLIFY(&result,false); [line 27]\n NULLIFY(&x,false); [line 27]\n *&return:int =0 [line 27]\n APPLY_ABSTRACTION; [line 27]\n " shape="box"]
14 -> 13 ;
13 [label="13: Exit conditional_assignment \n " color=yellow style=filled]
12 [label="12: Start conditional_assignment\nFormals: \nLocals: a:int result:int x:int \n DECLARE_LOCALS(&return,&a,&result,&x); [line 20]\n NULLIFY(&a,false); [line 20]\n NULLIFY(&result,false); [line 20]\n NULLIFY(&x,false); [line 20]\n " color=yellow style=filled]
12 -> 28 ;
11 [label="11: DeclStmt \n *&x:int =10 [line 11]\n " shape="box"]
11 -> 10 ;
10 [label="10: DeclStmt \n *&result:int =0 [line 12]\n APPLY_ABSTRACTION; [line 12]\n " shape="box"]
10 -> 4 ;
9 [label="9: ComppoundAssignStmt \n n$3=*&a:int [line 14]\n n$4=*&result:int [line 14]\n *&result:int =(n$4 + n$3) [line 14]\n REMOVE_TEMPS(n$3,n$4); [line 14]\n NULLIFY(&a,false); [line 14]\n " shape="box"]
9 -> 8 ;
8 [label="8: ComppoundAssignStmt \n n$2=*&x:int [line 15]\n *&x:int =(n$2 - 1) [line 15]\n REMOVE_TEMPS(n$2); [line 15]\n APPLY_ABSTRACTION; [line 15]\n " shape="box"]
8 -> 4 ;
7 [label="7: DeclStmt \n n$1=*&x:int [line 13]\n *&a:int =n$1 [line 13]\n REMOVE_TEMPS(n$1); [line 13]\n " shape="box"]
7 -> 5 ;
7 -> 6 ;
6 [label="6: Prune (false branch) \n n$0=*&a:int [line 13]\n PRUNE((n$0 == 0), false); [line 13]\n REMOVE_TEMPS(n$0); [line 13]\n " shape="invhouse"]
6 -> 3 ;
5 [label="5: Prune (true branch) \n n$0=*&a:int [line 13]\n PRUNE((n$0 != 0), true); [line 13]\n REMOVE_TEMPS(n$0); [line 13]\n " shape="invhouse"]
5 -> 9 ;
4 [label="4: + \n " ]
4 -> 7 ;
3 [label="3: Return Stmt \n NULLIFY(&a,false); [line 17]\n NULLIFY(&result,false); [line 17]\n NULLIFY(&x,false); [line 17]\n *&return:int =0 [line 17]\n APPLY_ABSTRACTION; [line 17]\n " shape="box"]
3 -> 2 ;
2 [label="2: Exit simple_assignment \n " color=yellow style=filled]
1 [label="1: Start simple_assignment\nFormals: \nLocals: a:int result:int x:int \n DECLARE_LOCALS(&return,&a,&result,&x); [line 10]\n NULLIFY(&a,false); [line 10]\n NULLIFY(&result,false); [line 10]\n NULLIFY(&x,false); [line 10]\n " color=yellow style=filled]
1 -> 11 ;
}

81
infer/tests/endtoend/cpp/NestedCPPOperatorsTest.java
Unescape View File

@ -0,0 +1,81 @@
/*
* Copyright (c) 2015 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
package endtoend.cpp;
import static org.hamcrest.MatcherAssert.assertThat;
import static utils.matchers.ResultContainsErrorInMethod.contains;
import static utils.matchers.ResultContainsNoErrorInMethod.doesNotContain;
import com.google.common.collect.ImmutableList;
import org.junit.BeforeClass;
import org.junit.ClassRule;
import org.junit.Test;
import java.io.IOException;
import utils.DebuggableTemporaryFolder;
import utils.InferException;
import utils.InferResults;
import utils.InferRunner;
public class NestedCPPOperatorsTest {
public static final String FILE =
"infer/tests/codetoanalyze/cpp/frontend/nestedoperators/var_decl_inside_if.cpp";
private static ImmutableList<String> inferCmd;
public static final String DIVIDE_BY_ZERO = "DIVIDE_BY_ZERO";
public static final String NULL_DEREFERENCE = "NULL_DEREFERENCE";
@ClassRule
public static DebuggableTemporaryFolder folder =
new DebuggableTemporaryFolder();
@BeforeClass
public static void runInfer() throws InterruptedException, IOException {
inferCmd = InferRunner.createCPPInferCommand(folder, FILE);
}
@Test
public void whenInferRunsOnDiv0MethodsErrorIsFound()
throws InterruptedException, IOException, InferException {
InferResults inferResults = InferRunner.runInferCPP(inferCmd);
String[] proceduresWithDiv0 = {
"simple_init_div0",
"simple_inif_elseif_div0",
"function_call_init_div0",
"conditional_init_div0",
"reference_init_div0",
};
for (String procedure : proceduresWithDiv0) {
assertThat(
"Results should contain the expected divide by zero",
inferResults,
contains(
DIVIDE_BY_ZERO,
FILE,
procedure
)
);
}
/* null dereference */
assertThat(
"Results should contain the expected null dereference",
inferResults,
contains(
NULL_DEREFERENCE,
FILE,
"simple_init_null_deref"
)
);
}
}

51
infer/tests/frontend/cpp/NestedCPPOperatorsTest.java
Unescape View File

@ -0,0 +1,51 @@
/*
* Copyright (c) 2013 - present Facebook, Inc.
* All rights reserved.
*
* This source code is licensed under the BSD style license found in the
* LICENSE file in the root directory of this source tree. An additional grant
* of patent rights can be found in the PATENTS file in the same directory.
*/
package frontend.cpp;
import org.junit.Rule;
import org.junit.Test;
import java.io.IOException;
import utils.DebuggableTemporaryFolder;
import utils.InferException;
import utils.ClangFrontendUtils;
public class NestedCPPOperatorsTest {
String nestedOperatorsBasePath = "infer/tests/codetoanalyze/cpp/frontend/nestedoperators/";
@Rule
public DebuggableTemporaryFolder folder = new DebuggableTemporaryFolder();
void frontendTest(String fileRelative) throws InterruptedException, IOException, InferException {
ClangFrontendUtils.createAndCompareCppDotFiles(folder, nestedOperatorsBasePath + fileRelative);
}
@Test
public void testVarDeclInsideIfDotFilesMatch()
throws InterruptedException, IOException, InferException {
frontendTest("var_decl_inside_if.cpp");
}
@Test
public void testVarDeclInsideWhileDotFilesMatch()
throws InterruptedException, IOException, InferException {
frontendTest("var_decl_inside_while.cpp");
}
@Test
public void testVarDeclInsideForDotFilesMatch()
throws InterruptedException, IOException, InferException {
frontendTest("var_decl_inside_for.cpp");
}
}
Write Preview
Loading…
Cancel
Save