WIP 15-3

Author: s-samadi

c/misra/src/rules/RULE-15-3/GotoLabelBlockCondition.ql

@@ -1,6 +1,6 @@
 /**
  * @id c/misra/goto-label-block-condition
- * @name RULE-15-3: The goto statement and any of its label shall be declared or enclosed in the same block. 
+ * @name RULE-15-3: The goto statement and any of its label shall be declared or enclosed in the same block.
  * @description Any label referenced by a goto statement shall be declared in the same block, or in
  *              any block enclosing the goto statement
  * @kind problem
@@ -15,33 +15,67 @@
 import cpp
 import codingstandards.c.misra
 
+predicate isPartOfSwitch(Stmt goto) {
+  exists(SwitchStmt switch | switch.getStmt() = goto.getParent())
+}
+
+Stmt getNextStmt(ControlFlowNode node) {
+  node.getASuccessor() = result
+  or
+  exists(ControlFlowNode other |
+    node.getASuccessor() = other and other != result and result = getNextStmt(other)
+  )
+}
+
+Stmt getPreviousStmt(Stmt s) { s = getNextStmt(result) }
+
+SwitchCase getSwitchCase(Stmt stmt) {
+  exists(int index, SwitchStmt switch |
+    getStmtInSwitch(switch, stmt, index) and getStmtInSwitch(switch, result, index - 1)
+  )
+  or
+  exists(int index, SwitchStmt switch, Stmt other |
+    getStmtInSwitch(switch, stmt, index) and
+    getStmtInSwitch(switch, other, index - 1) and
+    not other instanceof SwitchCase and
+    result = getSwitchCase(other)
+  )
+}
+
+predicate getStmtInSwitch(SwitchStmt switch, Stmt s, int index) {
+  switch.getStmt().(BlockStmt).getStmt(index) = s
+}
+
 int statementDepth(Stmt statement) {
   statement.getParent() = statement.getEnclosingFunction().getBlock() and result = 1
   or
   statementDepth(statement.getParent()) + 1 = result
 }
 
 predicate test(GotoStmt goto, Stmt target, int m, int n) {
-  statementDepth(goto) = m and target = goto.getTarget() and statementDepth(target) = n
+  statementDepth(goto) = m and
+  target = goto.getTarget() and
+  statementDepth(target) = n and
+  isPartOfSwitch(goto) and
+  getSwitchCase(goto) = getSwitchCase(target) and
+  m = n
 }
 
-from GotoStmt goto
+from GotoStmt goto, Stmt target, int gotoDepth, int targetDepth
 where
   not isExcluded(goto, Statements2Package::gotoLabelBlockConditionQuery()) and
-  not goto.getEnclosingBlock+() = goto.getTarget().getEnclosingBlock()
-  or
-  exists(SwitchStmt switch, int caseLocation, int nextCaseLocation |
-    switch.getAChild*() = goto and
-    switch.getASwitchCase().getLocation().getStartLine() = caseLocation and
-    switch.getASwitchCase().getNextSwitchCase().getLocation().getStartLine() = nextCaseLocation and
-    goto.getLocation().getStartLine() > caseLocation and
-    goto.getLocation().getStartLine() < nextCaseLocation and
+  goto.getTarget() = target and
+  gotoDepth = statementDepth(goto) and
+  targetDepth = statementDepth(target) and
+  targetDepth >= gotoDepth and
+  (
+    targetDepth = gotoDepth
+    implies
     (
-      goto.getTarget().getLocation().getStartLine() < caseLocation
+      not isPartOfSwitch(goto) and not goto.getParent() = target.getParent()
       or
-      goto.getTarget().getLocation().getStartLine() > nextCaseLocation
-    ) and
-    goto.getTarget().getLocation().getStartLine() > switch.getLocation().getStartLine()
+      isPartOfSwitch(goto) and not getSwitchCase(goto) = getSwitchCase(target)
+    )
   )
 select goto, "The $@ statement and its $@ are not declared or enclosed in the same block. test",
-  goto, "goto", goto.getTarget(), "label"
+  goto, "goto", target, "label"

c/misra/test/rules/RULE-15-3/test.c

@@ -66,4 +66,17 @@ void f7(int p) {
   default:
     break;
   }
-}
+}
+
+void f8(int p) {
+
+  switch (p) {
+  case 0:
+    goto L1;
+    ;
+  L1:; // COMPLIANT
+    break;
+  default:
+    break;
+  }
+}