Java: Consolidate Assertions.qll and Preconditions.qll.

This commit is contained in:
Anders Schack-Mulligen
2025-09-05 15:56:23 +02:00
parent edec76ae10
commit 3815503314
6 changed files with 168 additions and 109 deletions

View File

@@ -365,10 +365,10 @@ private module ControlFlowGraphImpl {
* Bind `t` to an unchecked exception that may occur in a precondition check or guard wrapper.
*/
private predicate uncheckedExceptionFromMethod(MethodCall ma, ThrowableType t) {
conditionCheckArgument(ma, _, _) and
(methodCallChecksArgument(ma) or methodCallUnconditionallyThrows(ma)) and
(t instanceof TypeError or t instanceof TypeRuntimeException)
or
methodMayThrow(ma.getMethod(), t)
methodMayThrow(ma.getMethod().getSourceDeclaration(), t)
}
/**
@@ -586,6 +586,7 @@ private module ControlFlowGraphImpl {
* Gets a `MethodCall` that always throws an exception or calls `exit`.
*/
private MethodCall nonReturningMethodCall() {
methodCallUnconditionallyThrows(result) or
result.getMethod().getSourceDeclaration() = nonReturningMethod() or
result = likelyNonReturningMethod().getAnAccess()
}