Re: noreturn attribute doesn't work in smatch

[Dan Carpenter <dan.carpenter@oracle.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