Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Substitution in Cil_types.predicate

On Mon, 2012-02-27 at 11:05 +0100, Virgile Prevosto wrote:
> No. As soon as offs is non-trivial, you end up with some sharing
> across new and old node.

Ok. I suspected I can't be that easy :)

> or overload vlogic_var_use instead of vterm:
> method vlogic_var_use lv =
>   if Logic_utils.is_same_var lv lv_old then Cil.ChangeTo lv_new else DoChildren

but wouldn't this just replace the lv without substituting the
corresponding offset?

> The latter can only be used for performing var-to-var substitution.

if I want to substitute s->t in s.a and both s,t are vars of compatible
type, is this a var-to-var substitution? 

> Yes, old node means the original one, and the result is the result of
> visiting v. The result is whatever the visitor wants to do with the
> children of v.

So the result is a visitAction? But fun _ -> t_new is applied on a term,
not on a visitAction. Or is the result the node of the corresponding
type after having been visited?

-- 
Best regards,
Boris