@@ -55,32 +55,29 @@ private predicate oldHasCompleteTwin(@usertype c, @usertype d) {
5555}
5656
5757pragma [ noinline]
58- private @mangledname getTopLevelClassMangledName ( @usertype c ) {
58+ private @mangledname getClassMangledName ( @usertype c ) {
5959 isClass ( c ) and
60- mangled_name ( c , result ) and
61- not namespacembrs ( _, c ) and // not in a namespace
62- not member ( _, _, c ) and // not in some structure
63- not class_instantiation ( c , _) // not a template instantiation
60+ mangled_name ( c , result )
6461}
6562
6663/** Holds if `d` is a unique complete class named `name`. */
6764pragma [ noinline]
6865private predicate existsCompleteWithMangledName ( @mangledname name , @usertype d ) {
6966 is_complete ( d ) and
70- name = getTopLevelClassMangledName ( d ) and
67+ name = getClassMangledName ( d ) and
7168 onlyOneCompleteClassExistsWithMangledName ( name )
7269}
7370
7471pragma [ noinline]
7572private predicate onlyOneCompleteClassExistsWithMangledName ( @mangledname name ) {
76- strictcount ( @usertype c | is_complete ( c ) and getTopLevelClassMangledName ( c ) = name ) = 1
73+ strictcount ( @usertype c | is_complete ( c ) and getClassMangledName ( c ) = name ) = 1
7774}
7875
7976/** Holds if `c` is an incomplete class named `name`. */
8077pragma [ noinline]
8178private predicate existsIncompleteWithMangledName ( @mangledname name , @usertype c ) {
8279 not is_complete ( c ) and
83- name = getTopLevelClassMangledName ( c )
80+ name = getClassMangledName ( c )
8481}
8582
8683/**
0 commit comments