--- layout: fc_discuss_archives title: Message 104 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 Fri, 2012-02-24 at 15:47 +0100, Virgile Prevosto wrote:
> Hello Boris,
> 
> 2012/2/24 Boris Hollas <hollas at informatik.htw-dresden.de>:
> > I want to perform a substitution in a Cil_types.predicate, for example
> > x->a in (0 <= x <= n). Is there a function in the Frama-C API to do so?
> 
> There's nothing built-in, but a tiny copy visitor should do the trick.

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?

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?

-- 
Best regards,
Boris