CPP: Avoid CP with edgekind in non-returning analysis

This commit is contained in:
Alex Eyers-Taylor
2023-09-08 16:55:06 +01:00
parent e208a7aed6
commit 5fe44b65b7
2 changed files with 2 additions and 2 deletions

View File

@@ -11,7 +11,7 @@ predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
instr.getSuccessor(kind) instanceof UnreachedInstruction and
kind instanceof GotoEdge
or
isCallToNonReturningFunction(instr)
isCallToNonReturningFunction(instr) and exists(instr.getSuccessor(kind))
}
/**

View File

@@ -11,7 +11,7 @@ predicate isInfeasibleInstructionSuccessor(Instruction instr, EdgeKind kind) {
instr.getSuccessor(kind) instanceof UnreachedInstruction and
kind instanceof GotoEdge
or
isCallToNonReturningFunction(instr)
isCallToNonReturningFunction(instr) and exists(instr.getSuccessor(kind))
}
/**