From 822ffc6f62142737fe3c6bc660277ef8d1898713 Mon Sep 17 00:00:00 2001 From: Daiva Naudziuniene Date: Mon, 11 Sep 2017 05:39:03 -0700 Subject: [PATCH] [frontend] Fix continue inside do while. Summary: The successor node of `continue` was not correct inside the `do while`. Reviewed By: sblackshear Differential Revision: D5769578 fbshipit-source-id: d7b0843 --- infer/src/clang/cTrans.ml | 8 ++- .../cpp/frontend/loops/do_while.cpp | 23 +++++++ .../cpp/frontend/loops/do_while.cpp.dot | 61 +++++++++++++++++++ 3 files changed, 89 insertions(+), 3 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp create mode 100644 infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp.dot diff --git a/infer/src/clang/cTrans.ml b/infer/src/clang/cTrans.ml index 82c478feb..6db70902c 100644 --- a/infer/src/clang/cTrans.ml +++ b/infer/src/clang/cTrans.ml @@ -1846,7 +1846,7 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s let sil_loc = CLocation.get_sil_location stmt_info context in let join_node = create_node Procdesc.Node.Join_node [] sil_loc context in let continuation = Some {break= succ_nodes; continue= [join_node]; return_temp= false} in - (* set the flat to inform that we are translating a condition of a if *) + (* set the flag to inform that we are translating a condition of a if *) let continuation_cond = mk_cond_continuation outer_continuation in let init_incr_nodes = match loop_kind with @@ -1887,8 +1887,10 @@ module CTrans_funct (F : CModule_type.CFrontend) : CModule_type.CTranslation = s -> res_trans_cond.root_nodes in let body_continuation = - match (continuation, init_incr_nodes) with - | Some c, Some (_, nodes_incr) + match (loop_kind, continuation, init_incr_nodes) with + | Loops.DoWhile _, Some c, _ + -> Some {c with continue= res_trans_cond.root_nodes} + | _, Some c, Some (_, nodes_incr) -> Some {c with continue= nodes_incr} | _ -> continuation diff --git a/infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp b/infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp new file mode 100644 index 000000000..0423d79da --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp @@ -0,0 +1,23 @@ +/* + * Copyright (c) 2016 - 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 test1(bool a, bool b) { + int x = 0; + do { + x = x + 1; + if (a) { + x = x + 2; + continue; + } else { + x = x + 3; + } + x = x + 4; + } while (b); + return x; +} diff --git a/infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp.dot b/infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp.dot new file mode 100644 index 000000000..afc7e2f9b --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/frontend/loops/do_while.cpp.dot @@ -0,0 +1,61 @@ +/* @generated */ +digraph iCFG { +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_1" [label="1: Start test1\nFormals: a:_Bool b:_Bool\nLocals: x:int \n DECLARE_LOCALS(&return,&x); [line 10]\n " color=yellow style=filled] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_1" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_14" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_2" [label="2: Exit test1 \n " color=yellow style=filled] + + +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_3" [label="3: Return Stmt \n n$0=*&x:int [line 22]\n *&return:int=n$0 [line 22]\n " shape="box"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_3" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_2" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_4" [label="4: + \n " ] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_4" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_13" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_5" [label="5: Prune (true branch) \n n$1=*&b:_Bool [line 21]\n PRUNE((n$1 != 0), true); [line 21]\n " shape="invhouse"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_5" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_4" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_6" [label="6: Prune (false branch) \n n$1=*&b:_Bool [line 21]\n PRUNE((n$1 == 0), false); [line 21]\n " shape="invhouse"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_6" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_3" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_7" [label="7: BinaryOperatorStmt: Assign \n n$2=*&x:int [line 20]\n *&x:int=(n$2 + 4) [line 20]\n " shape="box"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_7" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_5" ; + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_7" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_6" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_8" [label="8: + \n " ] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_8" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_7" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_9" [label="9: Prune (true branch) \n n$3=*&a:_Bool [line 14]\n PRUNE((n$3 != 0), true); [line 14]\n " shape="invhouse"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_9" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_11" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_10" [label="10: Prune (false branch) \n n$3=*&a:_Bool [line 14]\n PRUNE((n$3 == 0), false); [line 14]\n " shape="invhouse"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_10" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_12" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_11" [label="11: BinaryOperatorStmt: Assign \n n$4=*&x:int [line 15]\n *&x:int=(n$4 + 2) [line 15]\n " shape="box"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_11" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_5" ; + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_11" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_6" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_12" [label="12: BinaryOperatorStmt: Assign \n n$5=*&x:int [line 18]\n *&x:int=(n$5 + 3) [line 18]\n " shape="box"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_12" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_8" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_13" [label="13: BinaryOperatorStmt: Assign \n n$6=*&x:int [line 13]\n *&x:int=(n$6 + 1) [line 13]\n " shape="box"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_13" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_9" ; + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_13" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_10" ; +"test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_14" [label="14: DeclStmt \n *&x:int=0 [line 11]\n " shape="box"] + + + "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_14" -> "test1#_Z5test1bb.7b4b302df017dfac2074bf17bf65ca2c_4" ; +}