On Wed, 9 Jan 2019, Evan Zhao wrote:
> 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?
free variables would be all metavariables referenced by a rule.
minus_free_vars would be the ones used in the matching part of the rule (-
annotated code or unannotated code).
nc means no constraint. One can put a constraint on a metavariable, for
example to say that one position should be different than a previously
identified position. The no constraint variables are the ones thatare
found directly on the matching code, and not in the constraints.
julia
>
> 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
