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

Hello,

2012/2/27 Boris Hollas <hollas at informatik.htw-dresden.de>:
> This works in a small example:
>
> method vterm t =
> ?begin match t.term_node with
> ? ?| TLval(TVar lv, offs) when Logic_utils.is_same_var lv lv_old ->
> ? ? ?let t_new = Logic_const.term (TLval(TVar lv_new, offs))
> t.term_type in
> ? ? ?Cil.ChangeDoChildrenPost (t, fun _ -> t_new)
>
> However, I use the term_offset of t in t_new. Is this correct in
> general?

No. As soon as offs is non-trivial, you end up with some sharing
across new and old node.
You should either visit the offset manually
(let offs_new = Visitor.visitFramacTermOffset self offs in
 let t_new = Logic_const.term (Logic_const.tvar lv_new,offs_new) t.term_type in
Cil.ChangeTo t_new)
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
The latter can only be used for performing var-to-var substitution.
For more complex substitutions, you'll have to operate at
the vterm_lval or vterm level.

By the way, Logic_utils.is_same_logic_var is based purely on
variable's name (not taking into account possible captures). Depending
on the intended usage, you might want to rely on
Cil_datatype.Logic_variable.equal instead, which is based on the
lv_id.

>
> With ChangeDoChildrenPost, it want to replace t with t_new. In 5.14.3.,
> the meaning of ChangeDoChildrenPost is explained as follows:
> "ChangeDoChildrenPost(v,f) the old node is replaced by v, the visit goes
> on with the children of v, and when it is finished, f is applied to the
> result."
> - does "old node" mean the original node?
> - what does the "result" refer to? If it is the result of the visit,
> what is this?

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.

Best regards,
-- 
E tutto per oggi, a la prossima volta
Virgile