Messages in this thread | | | Date | Thu, 4 Jun 2020 17:51:19 +0200 (CEST) | From | Julia Lawall <> | Subject | Re: [PATCH] coccinelle: api: add kzfree script |
| |
On Thu, 4 Jun 2020, Denis Efremov wrote:
> > > On 6/4/20 5:15 PM, Julia Lawall wrote: > > Did you try ... here but find that some subexpressions of E could be > > modified in between? > > Yes, I tried to use "... when != E = E1 when != &E" and results were bad. > Now, I've tried forall and when strict. Here are examples: > > // forall added > // Works well, suitable for v2. One additional catch in w1 driver. > @r depends on !patch && !(file in "lib/test_kasan.c") && !(file in "mm/slab_common.c") forall@ > expression *E; // pointer. Results are equal as if we use E. > position p; > @@ > > * memset(E, 0, ...); > ... when != E // Is it enough to match &E, E = E1?
Yes.
> * kfree(E)@p; > > //no forall, when strict > //results are bad, too many false positives > @r depends on !patch && !(file in "lib/test_kasan.c") && !(file in "mm/slab_common.c")@ > expression *E; > position p; > @@ > > * memset(E, 0, ...); > ... when != E // E is not enough here > when strict
OK, it's reassonable.
> * kfree(E)@p; > > I guess that the difference is that "forall" requires that whole pattern should occur on > every path, "when strict" states that kfree should be called on every path after memset. > This results in missed uses of E in loops and under conditions. How can I state in this > case that E should not occur at all (in all paths) in between memset, kfree even as a > subexpression? > > // Doesn't work well > ... when != E > when != if (...) { ... E ... } > when != for(...;...;...) { ... E ... }
Could you send an example of some C code on which the result is not suitable?
julia
| |