File tree Expand file tree Collapse file tree
Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -4174,6 +4174,19 @@ void CodeGenModule::EmitGlobal(GlobalDecl GD) {
41744174 if (Global->hasAttr <WeakRefAttr>())
41754175 return ;
41764176
4177+ // CppVerify: spec and proof functions are ghost — never emit IR for them.
4178+ // This must be checked before alias/ifunc/cpu_dispatch paths so that a
4179+ // ghost function carrying any of those attributes is still suppressed.
4180+ if (LangOpts.VerifyContracts ) {
4181+ if (const auto *FD = dyn_cast<FunctionDecl>(Global)) {
4182+ if (const FunctionContractInfo *CI =
4183+ getContext ().getFunctionContract (FD )) {
4184+ if (CI ->IsSpec || CI ->IsProof )
4185+ return ;
4186+ }
4187+ }
4188+ }
4189+
41774190 // If this is an alias definition (which otherwise looks like a declaration)
41784191 // emit it now.
41794192 if (Global->hasAttr <AliasAttr>()) {
@@ -4235,12 +4248,6 @@ void CodeGenModule::EmitGlobal(GlobalDecl GD) {
42354248
42364249 // Ignore declarations, they will be emitted on their first use.
42374250 if (const auto *FD = dyn_cast<FunctionDecl>(Global)) {
4238- // CppVerify: spec and proof functions are ghost — never emit IR for them.
4239- if (const FunctionContractInfo *CI = getContext ().getFunctionContract (FD )) {
4240- if (CI ->IsSpec || CI ->IsProof )
4241- return ;
4242- }
4243-
42444251 if (DeviceKernelAttr::isOpenCLSpelling (FD ->getAttr <DeviceKernelAttr>()) &&
42454252 FD ->doesThisDeclarationHaveABody ())
42464253 addDeferredDeclToEmit (GlobalDecl (FD , KernelReferenceKind::Stub));
You can’t perform that action at this time.
0 commit comments