Re: [cocci] Checking evaluation of another SmPL script

On Sun, 24 May 2026, Markus Elfring wrote:

> >>> For the case of --no-loops, backward jumps are detected as loops for other pruposes.
> >>
> >> Which purposes do you imagine here?
> >
> > Loops require the use of the CTL operator AW, not AU.
>
> Thanks for such background information on computation tree logic.
>
>
> >>> --no-loops for for, while etc loops does consider a subset of meaningful paths.
> >> How will software design approaches evolve accordingly?
> >
> > As I said, I don't know what is the best thing to do.  If you have an
> > actual proposal., propose it.  If you don't have a proposal, plase stop
> > the discussion, because nothing is going to change.
> Will another clarification approach become helpful?
>
> Do you find it easier to clarify a reduced test case?
>
> Source file example:
> // See also:
> // * CWE-416: Use After Free
> //   https://cwe.mitre.org/data/definitions/416.html
> //
> // * MEM30-C: Do not access freed memory
> //   https://cmu-sei.github.io/secure-coding-standards/sei-cert-c-coding-standard/rules/memory-management-mem/mem30-c/
>
> #include <stdlib.h>
>
> struct my_point
> {
>  int x, y;
> };
>
> void my_test(void)
> {
>  // A few variables
>  size_t s = 0;
>  struct my_point * mp;
>
> allocation:
>  mp = malloc(sizeof(*mp));
>  if (mp)
>  {
>   free(mp);
>   // Demonstration of a programming mistake
>   mp->x = 2;
>
>   // Trigger a repetition eventually
>   if (++s < 5)
>     goto allocation;
>  }
> }
>
>
> SmPL script:
> @display@
> identifier i;
> expression e;
> @@
> *i = malloc(...);
>  ... when != i = e
> *i->x = e
>
>
> Questionable test result:
> Markus_Elfring@Sonne:…/Projekte/Coccinelle/janitor> time /usr/bin/spatch --no-loops show_UAF_2.cocci ../Probe/demo-UAF2.c
> …
> @@ -19,12 +19,10 @@ void my_test(void)
>   struct my_point * mp;
>
>  allocation:
> - mp = malloc(sizeof(*mp));
>   if (mp)
>   {
>    free(mp);
>    // Demonstration of a programming mistake
> -  mp->x = 2;
>
>    // Trigger a repetition eventually
>    if (++s < 5)
>
> real    0m0,078s
> user    0m0,053s
> sys     0m0,022s
>
>
>
> How will development ideas evolve accordingly?

I don't know what the above is supposed to do.  The semantic patch looks
completely wrong to detect a use after free.  One would expect thta a
detection of use after free would mention free somewhere.  But the
obtained result looks completely correct for the provided semantic patch
(as well as a hypothetical semantic patch that would check for use after
free).

julia