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] multiple ACSL contracts/declarations for one function definition

  • Subject: [Frama-c-discuss] multiple ACSL contracts/declarations for one function definition
  • From: David.COK at cea.fr (COK David)
  • Date: Wed, 27 Feb 2019 14:16:27 +0000
The ACSL manual says
"A C function can be defined only once but declared several times. It is allowed to annotate each of these functions with contracts. These contracts are seen as a single contract with the union of the requires clauses and behaviors."

This seems problematic. Different contracts might be used in different places. If the same contract is present multiple times, at minimum ones gets repetition of identical clauses, and one is faced with combining lists of behaviors, some of which might have identical names. This can arise if a declaration in a .h has a contract and the .h is included multiple times.

It seems better to follow the spirit of the ODR: If multiple declarations each have ACSL contracts, those contracts must be token-identical. Tools can pick one to use; as in the ODR, tools may not be obligated to report violations of this rule.

Comments?
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20190227/5dc6a88c/attachment.html>