Merge pull request #3085 from jbj/inStaticInitializer-AggregateLiteral

C++: Manual magic in inStaticInitializer
This commit is contained in:
Robert Marsh
2020-03-18 13:23:04 -07:00
committed by GitHub

View File

@@ -397,16 +397,21 @@ class StaticStorageDurationVariable extends Variable {
*/
private predicate runtimeExprInStaticInitializer(Expr e) {
inStaticInitializer(e) and
if e instanceof AggregateLiteral
if e instanceof AggregateLiteral // in sync with the cast in `inStaticInitializer`
then runtimeExprInStaticInitializer(e.getAChild())
else not e.getFullyConverted().isConstant()
}
/** Holds if `e` is part of the initializer of a `StaticStorageDurationVariable`. */
/**
* Holds if `e` is the initializer of a `StaticStorageDurationVariable`, either
* directly or below some top-level `AggregateLiteral`s.
*/
private predicate inStaticInitializer(Expr e) {
exists(StaticStorageDurationVariable var | e = var.getInitializer().getExpr())
or
inStaticInitializer(e.getParent())
// The cast to `AggregateLiteral` ensures we only compute what'll later be
// needed by `runtimeExprInStaticInitializer`.
inStaticInitializer(e.getParent().(AggregateLiteral))
}
/**