--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on June 2012 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Predicate application



Hello Boris,

2012/6/26 Boris Hollas <hollas at informatik.htw-dresden.de>:
> the constructor for predicate application Papp has a parameter of type
> logic_info * (logic_label * logic_label) list * term list.
> Was does the (logic_label * logic_label) list mean? If this has to do
> with label binders (eg Pre, Here, Post), shouldn't this be a logic_label
> list since a predicate can have an arbitrary positive number of labels,
> eg foo_pred{L1,L2,l3}(x :int) = x >= 0 ?

This is indeed use for label binders. More precisely, it is an
association list from label parameters (as appearing in the
declaration of the predicate) and the actual arguments.
e.g., if you have predicate foo_pred{L1,L2,L3}(integer x); and apply
it like foo_pred{Pre, Here, C_label}, the corresponding Papp
constructor will be of the form

Papp(_,[(L1, Pre); (L2,Old); (L3, C_label)],_)

The fact that we use an association list and not a plain list of
actual arguments is mainly historical.

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