--- layout: fc_discuss_archives title: Message 106 from Frama-C-discuss on February 2012 ---
[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