From: Dan Carpenter <dan.carpenter@oracle.com>
To: Norbert Manthey <nmanthey@amazon.de>
Cc: dwmw@amazon.co.uk, smatch@vger.kernel.org
Subject: Re: [xen 1/6] math: increase bounds and buffers
Date: Fri, 17 Aug 2018 14:42:25 +0300 [thread overview]
Message-ID: <20180817114225.lplk535x4h6ig3ba@mwanda> (raw)
In-Reply-To: <35c88062-8846-83f7-b447-c126bb67335d@amazon.de>
On Fri, Aug 17, 2018 at 09:25:48AM +0200, Norbert Manthey wrote:
> Dear Dan,
>
> rather than fixing a single limit as in this case, I'd be interested in
> adding another command line parameter that controls all the limits at
> once, and would allow them to be increased based on users demand. This
> could be useful for runs where I'm interested in more results and do not
> care about run time (e.g. because I run over night or the weekend).
>
> Is there a simple way to spot all the used limits, or can you point the
> relevant places so that I can adapt the tool appropriately? Thanks!
No, there isn't really...
There are a bunch of limits. Some of them are subtle. All of them come
from real world testing on the kernel where it just didn't complete the
build. One example of a subtle limit, is that if you're passing a list
of values like parameter X can be "1,4,6,...", then when the string gets
too long, Smatch just says ok it goes up to type_max. This is a kind of
hacky way to deal with recursive calls, because otherwise if a function
does:
void frob(int x)
{
frob(x + 2);
}
Then the list of potential values of x just keeps getting longer. A
bunch of the limits just solve recursion in one form or another.
I don't think boosting the limits really gains you very much. One of
the most common limits to hit is that "this function is taking too long
to parse so let's stop calculating implications of how variables are
related to each other". But this just means that you get more warnings
and they're mostly false positives...
What I would like to do is sort of say "parse all the function calls
for this file as if they were inline". Say you have code like:
out:
free_whatever(foo);
return ret;
Maybe there are 5 "goto out;" lines, it would be useful to parse the
free_whatever(foo); 5 times. Even if it took an hour to parse one file,
that would be fine if you were really interested in that file.
regards,
dan carpenter
prev parent reply other threads:[~2018-08-17 14:45 UTC|newest]
Thread overview: 14+ messages / expand[flat|nested] mbox.gz Atom feed top
2018-08-14 15:00 [xen 1/6] math: increase bounds and buffers Norbert Manthey
2018-08-14 15:00 ` [xen 2/6] user_data: add ends_with method Norbert Manthey
2018-08-14 15:00 ` [xen 3/6] user_data: match some Xen hypercalls Norbert Manthey
2018-08-14 15:00 ` [xen 4/6] user_data: match Xen copy_from_guest Norbert Manthey
2018-08-14 17:27 ` Dan Carpenter
2018-08-14 18:10 ` Norbert Manthey
2018-08-14 15:00 ` [xen 5/6] user_data: add register read function Norbert Manthey
2018-08-14 17:08 ` Dan Carpenter
2018-08-14 18:07 ` Norbert Manthey
2018-08-14 18:38 ` Dan Carpenter
2018-08-14 15:00 ` [xen 6/6] user_data: add hypercall sub calls Norbert Manthey
2018-08-14 16:35 ` [xen 1/6] math: increase bounds and buffers Dan Carpenter
[not found] ` <f1a66ee7-209c-aaee-0e51-fc4fc7b5b3cf@amazon.de>
2018-08-17 7:25 ` Norbert Manthey
2018-08-17 11:42 ` Dan Carpenter [this message]
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=20180817114225.lplk535x4h6ig3ba@mwanda \
--to=dan.carpenter@oracle.com \
--cc=dwmw@amazon.co.uk \
--cc=nmanthey@amazon.de \
--cc=smatch@vger.kernel.org \
/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;
as well as URLs for read-only IMAP folder(s) and NNTP newsgroup(s).