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] 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