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

  • Subject: [Frama-c-discuss] Predicate application
  • From: hollas at informatik.htw-dresden.de (Boris Hollas)
  • Date: Tue, 26 Jun 2012 08:40:00 +0200
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