/**
 * @name whilestmt01
 * @description The statement following the while statement in normal is a successor of the condition.
 */

import cpp

from WhileStmt ws, int k, LabelStmt l
where
	ws.getEnclosingFunction().hasName("normal")
	and ws.getParentStmt().hasChild(ws, k)
	and ws.getParentStmt().hasChild(l, k + 1)
	and l = ws.getCondition().getASuccessor()
	and l = ws.getCondition().getAFalseSuccessor()
	and count(ws.getCondition().getAFalseSuccessor()) = 1
select ws.getCondition(), l.getName()