--- layout: fc_discuss_archives title: Message 15 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,

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 ?
-- 
Best regards,
Boris