From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <smatch-owner@vger.kernel.org>
Received: from aserp2120.oracle.com ([141.146.126.78]:54080 "EHLO
        aserp2120.oracle.com" rhost-flags-OK-OK-OK-OK) by vger.kernel.org
        with ESMTP id S1726262AbfHVNcw (ORCPT
        <rfc822;smatch@vger.kernel.org>); Thu, 22 Aug 2019 09:32:52 -0400
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=oracle.com; h=date : from : to : cc
 : subject : message-id : references : mime-version : content-type :
 in-reply-to; s=corp-2019-08-05;
 bh=C1Wv3tdAVw2xDUAYsEtzApTXudLtXKogSkiT0+24GLw=;
 b=ZjEeX8MOsIbG688D+jm2Qn8bvZ1uoJaq68iyoY0lY2mNLEXlkvx63YN2PbTsqZQV6SsT
 qk7uukyJrIqRJn0unXF5gCgxe2DcjnkfujjKYJPDj937P4Q1OqcOXP6a6Tkx/9TN0jed
 TL/yAuezZl3To+RzCJgnus1hW+Je1+X5cGPkJek3pXq41/bEyOuuTeBI7+6Ie8oPLGPj
 St4xQMxZCS8uGp3d1QwcQXgJ7vY1GmcT4D5FvQ/6ESVOs7ApAGWxVfoFANhvNSQpPUk/
 B67iOZSxqMfIHBliHXZenQ5h2qBN2Fd0WPmj6muSIkIQjhBaNBAZp2arNMGvZqXH3MGI Fg== 
Date: Thu, 22 Aug 2019 16:30:34 +0300
From: Dan Carpenter <dan.carpenter@oracle.com>
Subject: Re: noreturn attribute doesn't work in smatch
Message-ID: <20190822132800.GJ4451@kadam>
References: <20190815005328.GA8004@movementarian.org>
 <20190815111237.GA20100@movementarian.org>
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Content-Disposition: inline
In-Reply-To: <20190815111237.GA20100@movementarian.org>
Sender: smatch-owner@vger.kernel.org
List-ID: <smatch.vger.kernel.org>
To: John Levon <levon@movementarian.org>
Cc: smatch@vger.kernel.org, linux-sparse@vger.kernel.org, yuri.pankov@nexenta.com

On Thu, Aug 15, 2019 at 12:12:37PM +0100, John Levon wrote:
> 
> 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...)
> 

This patch seems like a hack, but I will apply it...

> 
> 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.

The code to handle that is really ancient.  You need to do:
    ./smatch --info test.c | tee warns.txt
    grep no_return_funcs warns.txt || echo FAIL
    ./smatch_scripts/gen_no_return_funcs.sh warns.txt -p=levon
    mv levon.no_return_funcs smatch_data/

Then pass -p=levon to smatch on the next run.

regards,
dan carpenter