From: John Levon <levon@movementarian.org>
To: smatch@vger.kernel.org, linux-sparse@vger.kernel.org
Cc: yuri.pankov@nexenta.com
Subject: Re: noreturn attribute doesn't work in smatch
Date: Thu, 15 Aug 2019 12:12:37 +0100 [thread overview]
Message-ID: <20190815111237.GA20100@movementarian.org> (raw)
In-Reply-To: <20190815005328.GA8004@movementarian.org>
I took another pass, and this works for me:
diff --git a/parse.c b/parse.c
index ca4726b8..44c59707 100644
--- a/parse.c
+++ b/parse.c
@@ -2859,6 +2859,7 @@ struct token *external_declaration(struct token
*token, struct symbol_list **lis
/* Parse declaration-specifiers, if any */
token = declaration_specifiers(token, &ctx);
mod = storage_modifiers(&ctx);
+ mod |= ctx.ctype.modifiers & MOD_NORETURN;
decl = alloc_symbol(token->pos, SYM_NODE);
/* Just a type declaration? */
if (match_op(token, ';')) {
(I suppose a proper fix would collate all function-level attributes
but...)
However, it seems like smatch is still not quite passing its knowledge
along: if I have:
extern void die() __attribute((__noreturn__));
void mydie()
{
die();
}
then the die() call is nullified, but smatch doesn't realise that means
all paths of mydie() are __noreturn__ too.
regards
john
next prev parent reply other threads:[~2019-08-15 11:12 UTC|newest]
Thread overview: 6+ messages / expand[flat|nested] mbox.gz Atom feed top
2019-08-15 0:53 noreturn attribute doesn't work in smatch John Levon
2019-08-15 11:12 ` John Levon [this message]
2019-08-22 13:30 ` Dan Carpenter
2019-08-22 13:46 ` John Levon
2019-08-22 15:05 ` Dan Carpenter
2019-08-22 15:29 ` John Levon
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20190815111237.GA20100@movementarian.org \
--to=levon@movementarian.org \
--cc=linux-sparse@vger.kernel.org \
--cc=smatch@vger.kernel.org \
--cc=yuri.pankov@nexenta.com \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox