Thank you for your quick response, I am a beginner for model checking. I having been reading your papers and implement code for a while, there are some more questions, will you please to answer them too?
there are three free vars type, free_vars, minus_free_vars, and minus_nc_free_vars. By reading your paper, I know that free vars are used to manage the metavariables, but what does those three do respectively? Thank you again. On Wed, Jan 9, 2019 at 4:09 PM Julia Lawall <[email protected]> wrote: > > > > 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
