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? Thanks in advance. Best regards, Evan _______________________________________________ Cocci mailing list [email protected] https://systeme.lip6.fr/mailman/listinfo/cocci
