Java: Include non-null final fields in clearlyNotNull.

This commit is contained in:
Anders Schack-Mulligen
2020-01-03 16:24:54 +01:00
parent dc7863ce29
commit e74aa33f9d
5 changed files with 27 additions and 0 deletions

View File

@@ -101,6 +101,12 @@ predicate clearlyNotNull(SsaVariable v, Expr reason) {
v.(SsaImplicitInit).captures(captured) and
clearlyNotNull(captured, reason)
)
or
exists(Field f |
v.getSourceVariable().getVariable() = f and
f.isFinal() and
f.getInitializer() = clearlyNotNullExpr(reason)
)
}
/** Gets an expression that is provably not `null`. */