--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on June 2012 ---
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