On Wed, 9 Jan 2019, Evan Zhao wrote:
> Hi there,
>
> I am looking at a CTL formula generated by spatch with "--show-ctl-text",
>
> for example, for a cocci file like
> @@
> expression e,e1,e2;
> @@
>
> if (e)
> - GOTO(e1);
> -else GOTO(e2);
> + e1;
> +else e2;
>
> it corresponding CTL formula is:
>
> CTL =
> Let _r_0 = (EX^((TrueBranch v InLoop)) v EX^(EX^(FalseBranch))) in
> ((_r_0 &
> (Ex e1 .
> ((Ex_ e . (Ex _v . if (e) )) &,
> ((EX(FalseBranch) &, EX(After)) &,
> ((EX((TrueBranch &, AX((Ex _v . GOTO(e1);)))) &,
> EX((FalseBranch &,
> AX(((Ex _v . else ) &, AX((Ex e2 . (Ex _v . GOTO(e2);))))))))
> &, EX((After &, EX((Ex _v . _S1)))))))))
> v
> (!_r_0 &
> (Ex e1 .
> ((Ex_ e . if (e) ) &,
> (EX(FalseBranch) &,
> ((EX((TrueBranch &, AX((Ex _v . GOTO(e1);)))) &,
> EX((FalseBranch &,
> AX(((Ex _v . else ) &, AX((Ex e2 . (Ex _v . GOTO(e2);))))))))
> &, EX(After)))))))
>
> and I noticed that
> Let _r_0 = (EX^((TrueBranch v InLoop)) v EX^(EX^(FalseBranch))) in
> is a fixed pattern, and I can track it at somewhere around the function of
> do_between_dots in the module Asttoctl2, but I don't what it stands for.
>
> Cloud someone tell me what purpose it serves for?
I think it is checking whether the added code is in an if branch in which
case it wants to add {}. I think that in your semantic patch it is not
detecting that the then is just a replacement. If this is what led you to
look at the CTL in the first place, you may get a better result with
if (e)
- GOTO(
e1
- )
;
else
- GOTO(
e2
- )
;
Then it should be able to see that the changes are just inside the
existing branches, and so no {} adjustment is needed.
julia
_______________________________________________
Cocci mailing list
[email protected]
https://systeme.lip6.fr/mailman/listinfo/cocci
