Re: [cocci] Checking evaluation of another SmPL script

On Sun, 24 May 2026, Markus Elfring wrote:

> > Loops require the use of the CTL operator AW, not AU.
>
> Further development considerations might become more interesting
> for desirable clarifications according to computation tree logic variants.
>
>
> @display@
> identifier i;
> expression e;
> @@
> *i = malloc(...);
>  ... when != i = e
> *free(i);
> *i->x = e
>
>
> Markus_Elfring@Sonne:/home/altes_Heim2/elfring/Projekte/Coccinelle/janitor> /usr/bin/spatch --show-ctl-text --no-loops show_UAF_3.cocci ../Probe/demo-UAF2.c
> …
> CTL =
>
> (!EX(EX(EX(Exit))) &,
>  (Ex_ i .
>   ((Ex _v . i = malloc(...);) &,
>    EX((Ex_ e .
>       E[(!After &
>          (!(i = malloc(...); v free(i);) & !(After v InnerAnd(i = e))))
>        U
>        ((Ex _v . free(i);) &,
>         EX(InnerAnd(((Ex_ _pos . (Ex _v . i->x = e)) v
>                     (Ex_ _pos .
>                      ((Ex_ _E2_0 . (Ex _v . i[_E2_0].x = e)) &
>                       !Uncheck(i->x = e)))))))])))))
>
> diff =
> …
> @@ -19,12 +19,9 @@ 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)
>
>
> Where is the mentioned CTL operator applied here?

Nowhere.  Loops are only an issue for the forall case, because we need to
ignore the path that goes around the loop infinitely.  You semantic patch
doesn't use any forall path operators, only exists.

julia